no goals
α : Type u_1
β : Type u_2
γ : Sort ?u.1513
f : α → β
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
I : Injective f
a b : α
⊢ (f a == f b) = (a == b)
by_cases h : a == b <;> simp [h] <;> simpa [I.eq_iff] using h