From e6d72e3b82b7b7bffce72f965103f80c7fd8b4c9 Mon Sep 17 00:00:00 2001
From: mehbark <terezi@pyrope.net>
Date: Tue, 8 Apr 2025 22:19:21 -0400
Subject: [PATCH] not_f_eq_imp_eq

---
 SimpleCounterexamples/NotFEqImpEq.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)
 create mode 100644 SimpleCounterexamples/NotFEqImpEq.lean

diff --git a/SimpleCounterexamples/NotFEqImpEq.lean b/SimpleCounterexamples/NotFEqImpEq.lean
new file mode 100644
index 0000000..430e7a9
--- /dev/null
+++ b/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]