not_f_eq_imp_eq

SimpleCounterexamples/NotFEqImpEq.lean

@@ -0,0 +1,11 @@
+theorem not_f_eq_imp_eq
+    : ¬∀{α β: Type} (f : α → β) a b, f a = f b → a = b := by
+  intro h
+  have : 1 = 2 := h (fun _ => 0) 1 2 rfl
+  contradiction
+
+-- Counter-counterexample? (This is trivial.)
+theorem eq_imp_f_eq (f : α → β) (a b : α)
+    : a = b → f a = f b := by
+  intro h
+  rw [h]