chore(*/equiv): add simp to refl_apply and trans_apply where missing (#…

…13760)




Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/algebra/basic.lean

@@ -942,7 +942,7 @@ def trans (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) : A₁ ≃
 @[simp] lemma coe_trans (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) :
   ⇑(e₁.trans e₂) = e₂ ∘ e₁ := rfl
 
-lemma trans_apply (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) (x : A₁) :
+@[simp] lemma trans_apply (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) (x : A₁) :
   (e₁.trans e₂) x = e₂ (e₁ x) := rfl
 
 @[simp] lemma comp_symm (e : A₁ ≃ₐ[R] A₂) :

src/algebra/hom/equiv.lean

@@ -258,13 +258,13 @@ theorem self_comp_symm (e : M ≃* N) : e ∘ e.symm = id := funext e.apply_symm
 @[simp, to_additive]
 theorem coe_refl : ⇑(refl M) = id := rfl
 
-@[to_additive]
+@[simp, to_additive]
 theorem refl_apply (m : M) : refl M m = m := rfl
 
 @[simp, to_additive]
 theorem coe_trans (e₁ : M ≃* N) (e₂ : N ≃* P) : ⇑(e₁.trans e₂) = e₂ ∘ e₁ := rfl
 
-@[to_additive]
+@[simp, to_additive]
 theorem trans_apply (e₁ : M ≃* N) (e₂ : N ≃* P) (m : M) : e₁.trans e₂ m = e₂ (e₁ m) := rfl
 
 @[simp, to_additive] theorem symm_trans_apply (e₁ : M ≃* N) (e₂ : N ≃* P) (p : P) :

src/linear_algebra/affine_space/affine_equiv.lean

@@ -74,7 +74,7 @@ omit V₂
 
 @[simp] lemma coe_refl : ⇑(refl k P₁) = id := rfl
 
-lemma refl_apply (x : P₁) : refl k P₁ x = x := rfl
+@[simp] lemma refl_apply (x : P₁) : refl k P₁ x = x := rfl
 
 @[simp] lemma to_equiv_refl : (refl k P₁).to_equiv = equiv.refl P₁ := rfl
 
@@ -207,6 +207,7 @@ include V₂ V₃
 
 @[simp] lemma coe_trans (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) : ⇑(e.trans e') = e' ∘ e := rfl
 
+@[simp]
 lemma trans_apply (e : P₁ ≃ᵃ[k] P₂) (e' : P₂ ≃ᵃ[k] P₃) (p : P₁) : e.trans e' p = e' (e p) := rfl
 
 include V₄

src/order/hom/basic.lean

@@ -508,7 +508,7 @@ def refl (α : Type*) [has_le α] : α ≃o α := rel_iso.refl (≤)
 
 @[simp] lemma coe_refl : ⇑(refl α) = id := rfl
 
-lemma refl_apply (x : α) : refl α x = x := rfl
+@[simp] lemma refl_apply (x : α) : refl α x = x := rfl
 
 @[simp] lemma refl_to_equiv : (refl α).to_equiv = equiv.refl α := rfl
 
@@ -562,7 +562,7 @@ e.to_equiv.preimage_image s
 
 @[simp] lemma coe_trans (e : α ≃o β) (e' : β ≃o γ) : ⇑(e.trans e') = e' ∘ e := rfl
 
-lemma trans_apply (e : α ≃o β) (e' : β ≃o γ) (x : α) : e.trans e' x = e' (e x) := rfl
+@[simp] lemma trans_apply (e : α ≃o β) (e' : β ≃o γ) (x : α) : e.trans e' x = e' (e x) := rfl
 
 @[simp] lemma refl_trans (e : α ≃o β) : (refl α).trans e = e := by { ext x, refl }