mathlib

5fbebf67 - fix(logic/{function}/basic): remove simp lemmas `function.injective.eq_iff` and `imp_iff_right` (#6402)

fix(logic/{function}/basic): remove simp lemmas `function.injective.eq_iff` and `imp_iff_right` (#6402) * `imp_iff_right` is a conditional simp lemma that matches a lot and should never successfully rewrite. * `function.injective.eq_iff` is a conditional simp lemma that matches a lot and is rarely used. Since you almost always need to give the proof `hf : function.injective f` as an argument to `simp`, you can replace it with `hf.eq_iff`. Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>