chore(data/equiv/*): rename trans_symm and symm_trans to `self_tr…

…ans_symm` and `symm_trans_self`. (#10309)

This frees up `symm_trans` to state `(a.trans b).symm = a.symm.trans b.symm`.

These names are consistent with `self_comp_symm` and `symm_comp_self`.

src/analysis/normed_space/affine_isometry.lean

@@ -356,8 +356,8 @@ omit V V₂ V₃
 
 @[simp] lemma trans_refl : e.trans (refl 𝕜 P₂) = e := ext $ λ x, rfl
 @[simp] lemma refl_trans : (refl 𝕜 P).trans e = e := ext $ λ x, rfl
-@[simp] lemma trans_symm : e.trans e.symm = refl 𝕜 P := ext e.symm_apply_apply
-@[simp] lemma symm_trans : e.symm.trans e = refl 𝕜 P₂ := ext e.apply_symm_apply
+@[simp] lemma self_trans_symm : e.trans e.symm = refl 𝕜 P := ext e.symm_apply_apply
+@[simp] lemma symm_trans_self : e.symm.trans e = refl 𝕜 P₂ := ext e.apply_symm_apply
 
 include V V₂ V₃
 @[simp] lemma coe_symm_trans (e₁ : P ≃ᵃⁱ[𝕜] P₂) (e₂ : P₂ ≃ᵃⁱ[𝕜] P₃) :
@@ -378,7 +378,7 @@ instance : group (P ≃ᵃⁱ[𝕜] P) :=
   one_mul := trans_refl,
   mul_one := refl_trans,
   mul_assoc := λ _ _ _, trans_assoc _ _ _,
-  mul_left_inv := trans_symm }
+  mul_left_inv := self_trans_symm }
 
 @[simp] lemma coe_one : ⇑(1 : P ≃ᵃⁱ[𝕜] P) = id := rfl
 @[simp] lemma coe_mul (e e' : P ≃ᵃⁱ[𝕜] P) : ⇑(e * e') = e ∘ e' := rfl

src/analysis/normed_space/linear_isometry.lean

@@ -305,8 +305,8 @@ omit σ₁₃ σ₂₁ σ₃₁ σ₃₂
 
 @[simp] lemma trans_refl : e.trans (refl R₂ E₂) = e := ext $ λ x, rfl
 @[simp] lemma refl_trans : (refl R E).trans e = e := ext $ λ x, rfl
-@[simp] lemma trans_symm : e.trans e.symm = refl R E := ext e.symm_apply_apply
-@[simp] lemma symm_trans : e.symm.trans e = refl R₂ E₂ := ext e.apply_symm_apply
+@[simp] lemma self_trans_symm : e.trans e.symm = refl R E := ext e.symm_apply_apply
+@[simp] lemma symm_trans_self : e.symm.trans e = refl R₂ E₂ := ext e.apply_symm_apply
 
 include σ₁₃ σ₂₁ σ₃₂ σ₃₁
 @[simp] lemma coe_symm_trans (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
@@ -326,7 +326,7 @@ instance : group (E ≃ₗᵢ[R] E) :=
   one_mul := trans_refl,
   mul_one := refl_trans,
   mul_assoc := λ _ _ _, trans_assoc _ _ _,
-  mul_left_inv := trans_symm }
+  mul_left_inv := self_trans_symm }
 
 @[simp] lemma coe_one : ⇑(1 : E ≃ₗᵢ[R] E) = id := rfl
 @[simp] lemma coe_mul (e e' : E ≃ₗᵢ[R] E) : ⇑(e * e') = e ∘ e' := rfl

src/data/equiv/basic.lean

@@ -273,9 +273,9 @@ lemma eq_symm_apply {α β} (e : α ≃ β) {x y} : y = e.symm x ↔ e y = x :=
 
 @[simp] theorem refl_trans (e : α ≃ β) : (equiv.refl α).trans e = e := by { cases e, refl }
 
-@[simp] theorem symm_trans (e : α ≃ β) : e.symm.trans e = equiv.refl β := ext (by simp)
+@[simp] theorem symm_trans_self (e : α ≃ β) : e.symm.trans e = equiv.refl β := ext (by simp)
 
-@[simp] theorem trans_symm (e : α ≃ β) : e.trans e.symm = equiv.refl α := ext (by simp)
+@[simp] theorem self_trans_symm (e : α ≃ β) : e.trans e.symm = equiv.refl α := ext (by simp)
 
 lemma trans_assoc {δ} (ab : α ≃ β) (bc : β ≃ γ) (cd : γ ≃ δ) :
   (ab.trans bc).trans cd = ab.trans (bc.trans cd) :=

src/data/equiv/module.lean

@@ -233,11 +233,11 @@ omit σ'
 
 @[simp] lemma refl_symm [module R M] : (refl R M).symm = linear_equiv.refl R M := rfl
 
-@[simp] lemma trans_symm [module R M] [module R M₂] (f : M ≃ₗ[R] M₂) :
+@[simp] lemma self_trans_symm [module R M] [module R M₂] (f : M ≃ₗ[R] M₂) :
   f.trans f.symm = linear_equiv.refl R M :=
 by { ext x, simp }
 
-@[simp] lemma symm_trans [module R M] [module R M₂] (f : M ≃ₗ[R] M₂) :
+@[simp] lemma symm_trans_self [module R M] [module R M₂] (f : M ≃ₗ[R] M₂) :
   f.symm.trans f = linear_equiv.refl R M₂ :=
 by { ext x, simp }
 

src/data/equiv/ring.lean

@@ -427,8 +427,8 @@ namespace ring_equiv
 
 variables [has_add R] [has_add S] [has_mul R] [has_mul S]
 
-@[simp] theorem trans_symm (e : R ≃+* S) : e.trans e.symm = ring_equiv.refl R := ext e.3
-@[simp] theorem symm_trans (e : R ≃+* S) : e.symm.trans e = ring_equiv.refl S := ext e.4
+@[simp] theorem self_trans_symm (e : R ≃+* S) : e.trans e.symm = ring_equiv.refl R := ext e.3
+@[simp] theorem symm_trans_self (e : R ≃+* S) : e.symm.trans e = ring_equiv.refl S := ext e.4
 
 /-- If two rings are isomorphic, and the second is a domain, then so is the first. -/
 protected lemma is_domain

src/data/finsupp/basic.lean

@@ -2450,12 +2450,12 @@ protected def dom_congr [add_comm_monoid M] (e : α ≃ β) : (α →₀ M) ≃+
 { to_fun := equiv_map_domain e,
   inv_fun := equiv_map_domain e.symm,
   left_inv := λ v, begin
-    simp only [← equiv_map_domain_trans, equiv.trans_symm],
+    simp only [← equiv_map_domain_trans, equiv.self_trans_symm],
     exact equiv_map_domain_refl _
   end,
   right_inv := begin
     assume v,
-    simp only [← equiv_map_domain_trans, equiv.symm_trans],
+    simp only [← equiv_map_domain_trans, equiv.symm_trans_self],
     exact equiv_map_domain_refl _
   end,
   map_add' := λ a b, by simp only [equiv_map_domain_eq_map_domain]; exact map_domain_add }

src/data/pequiv.lean

@@ -208,7 +208,7 @@ end of_set
 
 lemma symm_trans_rev (f : α ≃. β) (g : β ≃. γ) : (f.trans g).symm = g.symm.trans f.symm := rfl
 
-lemma trans_symm (f : α ≃. β) : f.trans f.symm = of_set {a | (f a).is_some} :=
+lemma self_trans_symm (f : α ≃. β) : f.trans f.symm = of_set {a | (f a).is_some} :=
 begin
   ext,
   dsimp [pequiv.trans],
@@ -220,12 +220,12 @@ begin
   { simp {contextual := tt} }
 end
 
-lemma symm_trans (f : α ≃. β) : f.symm.trans f = of_set {b | (f.symm b).is_some} :=
-symm_injective $ by simp [symm_trans_rev, trans_symm, -symm_symm]
+lemma symm_trans_self (f : α ≃. β) : f.symm.trans f = of_set {b | (f.symm b).is_some} :=
+symm_injective $ by simp [symm_trans_rev, self_trans_symm, -symm_symm]
 
 lemma trans_symm_eq_iff_forall_is_some {f : α ≃. β} :
   f.trans f.symm = pequiv.refl α ↔ ∀ a, is_some (f a) :=
-by rw [trans_symm, of_set_eq_refl, set.eq_univ_iff_forall]; refl
+by rw [self_trans_symm, of_set_eq_refl, set.eq_univ_iff_forall]; refl
 
 instance : has_bot (α ≃. β) :=
 ⟨{ to_fun := λ _, none,

src/field_theory/splitting_field.lean

@@ -740,7 +740,7 @@ theorem splits_iff (f : polynomial K) [is_splitting_field K L f] :
     let ⟨x, hxs, hxy⟩ := finset.mem_image.1 (by rwa multiset.to_finset_map at hy) in
     hxy ▸ set_like.mem_coe.2 $ subalgebra.algebra_map_mem _ _),
  λ h, @ring_equiv.to_ring_hom_refl K _ ▸
-  ring_equiv.trans_symm (ring_equiv.of_bijective _ $ algebra.bijective_algebra_map_iff.2 h) ▸
+  ring_equiv.self_trans_symm (ring_equiv.of_bijective _ $ algebra.bijective_algebra_map_iff.2 h) ▸
   by { rw ring_equiv.to_ring_hom_trans, exact splits_comp_of_splits _ _ (splits L f) }⟩
 
 theorem mul (f g : polynomial F) (hf : f ≠ 0) (hg : g ≠ 0) [is_splitting_field F K f]

src/geometry/manifold/diffeomorph.lean

@@ -163,9 +163,9 @@ h.to_equiv.symm_apply_apply x
 
 @[simp] lemma symm_refl : (diffeomorph.refl I M n).symm = diffeomorph.refl I M n :=
 ext $ λ _, rfl
-@[simp] lemma trans_symm (h : M ≃ₘ^n⟮I, J⟯ N) : h.trans h.symm = diffeomorph.refl I M n :=
+@[simp] lemma self_trans_symm (h : M ≃ₘ^n⟮I, J⟯ N) : h.trans h.symm = diffeomorph.refl I M n :=
 ext h.symm_apply_apply
-@[simp] lemma symm_trans (h : M ≃ₘ^n⟮I, J⟯ N) : h.symm.trans h = diffeomorph.refl J N n :=
+@[simp] lemma symm_trans_self (h : M ≃ₘ^n⟮I, J⟯ N) : h.symm.trans h = diffeomorph.refl J N n :=
 ext h.apply_symm_apply
 @[simp] lemma symm_trans' (h₁ : M ≃ₘ^n⟮I, I'⟯ M') (h₂ : M' ≃ₘ^n⟮I', J⟯ N) :
   (h₁.trans h₂).symm = h₂.symm.trans h₁.symm := rfl

src/group_theory/perm/basic.lean

@@ -26,7 +26,7 @@ instance perm_group : group (perm α) :=
   mul_assoc := λ f g h, (trans_assoc _ _ _).symm,
   one_mul := trans_refl,
   mul_one := refl_trans,
-  mul_left_inv := trans_symm }
+  mul_left_inv := self_trans_symm }
 
 theorem mul_apply (f g : perm α) (x) : (f * g) x = f (g x) :=
 equiv.trans_apply _ _ _
@@ -74,13 +74,13 @@ equiv.refl_trans e
 
 @[simp] lemma refl_mul (e : perm α) : equiv.refl α * e = e := equiv.refl_trans e
 
-@[simp] lemma inv_trans (e : perm α) : e⁻¹.trans e = 1 := equiv.symm_trans e
+@[simp] lemma inv_trans_self (e : perm α) : e⁻¹.trans e = 1 := equiv.symm_trans_self e
 
-@[simp] lemma mul_symm (e : perm α) : e * e.symm = 1 := equiv.symm_trans e
+@[simp] lemma mul_symm (e : perm α) : e * e.symm = 1 := equiv.symm_trans_self e
 
-@[simp] lemma trans_inv (e : perm α) : e.trans e⁻¹ = 1 := equiv.trans_symm e
+@[simp] lemma self_trans_inv (e : perm α) : e.trans e⁻¹ = 1 := equiv.self_trans_symm e
 
-@[simp] lemma symm_mul (e : perm α) : e.symm * e = 1 := equiv.trans_symm e
+@[simp] lemma symm_mul (e : perm α) : e.symm * e = 1 := equiv.self_trans_symm e
 
 /-! Lemmas about `equiv.perm.sum_congr` re-expressed via the group structure. -/
 

src/group_theory/perm/sign.lean

@@ -405,7 +405,7 @@ lemma sign_aux_eq_sign_aux2 {n : ℕ} : ∀ (l : list α) (f : perm α) (e : α
   (h : ∀ x, f x ≠ x → x ∈ l), sign_aux ((e.symm.trans f).trans e) = sign_aux2 l f
 | []     f e h := have f = 1, from equiv.ext $
   λ y, not_not.1 (mt (h y) (list.not_mem_nil _)),
-by rw [this, one_def, equiv.trans_refl, equiv.symm_trans, ← one_def,
+by rw [this, one_def, equiv.trans_refl, equiv.symm_trans_self, ← one_def,
   sign_aux_one, sign_aux2]
 | (x::l) f e h := begin
   rw sign_aux2,

src/linear_algebra/affine_space/affine_equiv.lean

@@ -211,10 +211,10 @@ ext $ λ _, rfl
 @[simp] lemma refl_trans (e : P₁ ≃ᵃ[k] P₂) : (refl k P₁).trans e = e :=
 ext $ λ _, rfl
 
-@[simp] lemma trans_symm (e : P₁ ≃ᵃ[k] P₂) : e.trans e.symm = refl k P₁ :=
+@[simp] lemma self_trans_symm (e : P₁ ≃ᵃ[k] P₂) : e.trans e.symm = refl k P₁ :=
 ext e.symm_apply_apply
 
-@[simp] lemma symm_trans (e : P₁ ≃ᵃ[k] P₂) : e.symm.trans e = refl k P₂ :=
+@[simp] lemma symm_trans_self (e : P₁ ≃ᵃ[k] P₂) : e.symm.trans e = refl k P₂ :=
 ext e.apply_symm_apply
 
 @[simp] lemma apply_line_map (e : P₁ ≃ᵃ[k] P₂) (a b : P₁) (c : k) :
@@ -230,7 +230,7 @@ instance : group (P₁ ≃ᵃ[k] P₁) :=
   mul_assoc := λ e₁ e₂ e₃, trans_assoc _ _ _,
   one_mul := trans_refl,
   mul_one := refl_trans,
-  mul_left_inv := trans_symm }
+  mul_left_inv := self_trans_symm }
 
 lemma one_def : (1 : P₁ ≃ᵃ[k] P₁) = refl k P₁ := rfl
 

src/linear_algebra/determinant.lean

@@ -258,9 +258,9 @@ begin
   { rcases H with ⟨s, ⟨b⟩⟩,
     rw [← det_to_matrix b f, ← det_to_matrix (b.map e), to_matrix_comp (b.map e) b (b.map e),
         to_matrix_comp (b.map e) b b, ← matrix.mul_assoc, matrix.det_conj],
-    { rw [← to_matrix_comp, linear_equiv.comp_coe, e.symm_trans,
+    { rw [← to_matrix_comp, linear_equiv.comp_coe, e.symm_trans_self,
           linear_equiv.refl_to_linear_map, to_matrix_id] },
-    { rw [← to_matrix_comp, linear_equiv.comp_coe, e.trans_symm,
+    { rw [← to_matrix_comp, linear_equiv.comp_coe, e.self_trans_symm,
           linear_equiv.refl_to_linear_map, to_matrix_id] } },
   { have H' : ¬ (∃ (t : finset N), nonempty (basis t A N)),
     { contrapose! H,