feat(logic/basic): eq_iff_eq_cancel (#1447)

* feat(logic/basic): eq_iff_eq_cancel

These lemmas or not meant for `rw` but to be applied, as a sort of congruence lemma.

* State lemmas as iff

* Make'm simp

src/logic/basic.lean

@@ -81,6 +81,14 @@ attribute [symm] ne.symm
 
 lemma ne_comm {α} {a b : α} : a ≠ b ↔ b ≠ a := ⟨ne.symm, ne.symm⟩
 
+@[simp] lemma eq_iff_eq_cancel_left {b c : α} :
+  (∀ {a}, a = b ↔ a = c) ↔ (b = c) :=
+⟨λ h, by rw [← h], λ h a, by rw h⟩
+
+@[simp] lemma eq_iff_eq_cancel_right {a b : α} :
+  (∀ {c}, a = c ↔ b = c) ↔ (a = b) :=
+⟨λ h, by rw h, λ h a, by rw h⟩
+
 end miscellany
 
 /-