[Merged by Bors] - fix(logic/{function}/basic): remove simp lemmas function.injective.eq_iff and imp_iff_right

[robertylewis]

• 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.

---

[eric-wieser]

Are any lemmas with statement injective f currently tagged simp? I guess those could be resolved by changing the relevant fs to embeddings, although that doesn't work for already-bundled fs

[robertylewis]

[list.reverse_injective, list.length_injective, list.cons_injective] seem to be the only ones.

But I think I'm missing something, what's being resolved with this change? It's fine to leave those as simp lemmas.

[eric-wieser]

I ask only because removing [simp] from injective.eq_iff means that list.reverse_injective.eq_iff, list.length_injective.eq_iff, and list.cons_injective.eq_iff will no longer be applied by simp. I think we have aliases for those statements tagged simp anyway though, so it shouldn't matter.

[gebner]

Right, the aliases are reverse_inj and cons_inj. I'm not sure how useful length_inj would be.

bors r+

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Build failed (retrying...):

• Build mathlib

[sgouezel]

bors r-
Two builds have failed with this one.

[bors]

Canceled.

[robertylewis]

I just learned that simp calls refl to try to discharge hypotheses to conditional simp lemmas, even with the default discharger failed:

constant R : ℕ → ℕ → Prop 

@[refl] -- removing this cases the example to fail
lemma R_refl (a : ℕ) : R a a := sorry

@[simp]
lemma r_simp (a : ℕ) (ha : R a a) : id a = 0 := sorry 

example : id 3 = 0 := by simp

So my claim

• imp_iff_right is a conditional simp lemma that matches a lot and should never successfully rewrite.

is false, it can successfully rewrite. I still think it should go.

[bryangingechen]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests

[gebner]

I just learned that simp calls refl to try to discharge hypotheses to conditional simp lemmas, even with the default discharger failed:

If the discharger tactic fails, simp calls simp to discharge hypotheses in conditional simp lemmas.