Commit 2021-02-26 04:07 5fbebf67

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.