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>

Author: robertylewis

src/analysis/hofer.lean

@@ -63,7 +63,7 @@ begin
   { intro n,
     induction n using nat.case_strong_induction_on with n IH,
     { specialize hu 0,
-      simpa [hu0, mul_nonneg_iff, zero_le_one, ε_pos.le] using hu },
+      simpa [hu0, mul_nonneg_iff, zero_le_one, ε_pos.le, le_refl] using hu },
     have A : d (u (n+1)) x ≤ 2 * ε,
     { rw [dist_comm],
       let r := range (n+1), -- range (n+1) = {0, ..., n}

src/analysis/normed_space/inner_product.lean

@@ -766,7 +766,7 @@ begin
   rw orthonormal_iff_ite at ⊢ hv,
   intros i j,
   convert hv (f i) (f j) using 1,
-  simp [hf]
+  simp [hf.eq_iff]
 end
 
 /-- A linear combination of some subset of an orthonormal set is orthogonal to other members of the

src/combinatorics/colex.lean

@@ -107,7 +107,7 @@ begin
   simp only [colex.lt_def, not_exists, mem_image, exists_prop, not_and],
   split,
   { rintro ⟨k, z, q, k', _, rfl⟩,
-    exact ⟨k', λ x hx, by simpa [h₁.injective] using z (h₁ hx), λ t, q _ t rfl, ‹k' ∈ B›⟩ },
+    exact ⟨k', λ x hx, by simpa [h₁.injective.eq_iff] using z (h₁ hx), λ t, q _ t rfl, ‹k' ∈ B›⟩ },
   rintro ⟨k, z, ka, _⟩,
   refine ⟨f k, λ x hx, _, _, k, ‹k ∈ B›, rfl⟩,
   { split,

src/combinatorics/hall.lean

@@ -125,7 +125,7 @@ begin
       specialize hfr x,
       rw ←h at hfr,
       simpa using hfr, },
-    by_cases h₁ : z₁ = x; by_cases h₂ : z₂ = x; simp [h₁, h₂, hfinj, key, key.symm], },
+    by_cases h₁ : z₁ = x; by_cases h₂ : z₂ = x; simp [h₁, h₂, hfinj.eq_iff, key, key.symm], },
   { intro z,
     split_ifs with hz,
     { rwa hz },

src/data/equiv/basic.lean

@@ -1634,7 +1634,7 @@ lemma image_symm_preimage {α β} {f : α → β} (hf : injective f) (u s : set
 begin
   ext ⟨b, a, has, rfl⟩,
   have : ∀(h : ∃a', a' ∈ s ∧ a' = a), classical.some h = a := λ h, (classical.some_spec h).2,
-  simp [equiv.set.image, equiv.set.image_of_inj_on, hf, this],
+  simp [equiv.set.image, equiv.set.image_of_inj_on, hf.eq_iff, this],
 end
 
 /-- If `f : α → β` is an injective function, then `α` is equivalent to the range of `f`. -/

src/linear_algebra/basis.lean

@@ -179,7 +179,7 @@ begin
   { intro i,
     ext j,
     haveI : nontrivial R := ⟨⟨0, 1, H⟩⟩,
-    simp [hv.range_repr_self, finsupp.single_apply, hv.injective] }
+    simp [hv.range_repr_self, finsupp.single_apply, hv.injective.eq_iff] }
 end
 
 /-- Construct a linear map given the value at the basis. -/

src/logic/basic.lean

@@ -219,7 +219,7 @@ iff_def.trans and.comm
 theorem imp_true_iff {α : Sort*} : (α → true) ↔ true :=
 iff_true_intro $ λ_, trivial
 
-@[simp] theorem imp_iff_right (ha : a) : (a → b) ↔ b :=
+theorem imp_iff_right (ha : a) : (a → b) ↔ b :=
 ⟨λf, f ha, imp_intro⟩
 
 /-! ### Declarations about `not` -/

src/logic/function/basic.lean

@@ -56,7 +56,7 @@ iff.intro (assume h a, h ▸ rfl) funext
 protected lemma bijective.injective {f : α → β} (hf : bijective f) : injective f := hf.1
 protected lemma bijective.surjective {f : α → β} (hf : bijective f) : surjective f := hf.2
 
-@[simp] theorem injective.eq_iff (I : injective f) {a b : α} :
+theorem injective.eq_iff (I : injective f) {a b : α} :
   f a = f b ↔ a = b :=
 ⟨@I _ _, congr_arg f⟩
 

src/order/rel_iso.lean

@@ -282,7 +282,7 @@ end
 def order_embedding_of_lt_embedding [partial_order α] [partial_order β]
   (f : ((<) : α → α → Prop) ↪r ((<) : β → β → Prop)) :
   α ↪o β :=
-{ map_rel_iff' := by { intros, simp [le_iff_lt_or_eq,f.map_rel_iff, f.injective] }, .. f }
+{ map_rel_iff' := by { intros, simp [le_iff_lt_or_eq,f.map_rel_iff, f.injective.eq_iff] }, .. f }
 
 @[simp]
 lemma order_embedding_of_lt_embedding_apply [partial_order α] [partial_order β]