Commit 2025-06-12 08:08 d9571603

feat: make sure that the simp normal form of equiv-like classes pushes symm and trans to the right (#25604) This follows the usual convention for coercions. See discussion at #mathlib4 > simp normal form for symm and coercions @ 💬 For each equiv class, after the PR we should have lemmas like

@[simp]
lemma coe_toEquiv (e : G ≃+c[a, b] H) : ⇑e.toEquiv = e := rfl
@[simp]
lemma coe_symm_toEquiv (e : G ≃+c[a, b] H) : ⇑e.toEquiv.symm = e.symm := rfl
@[simp]
lemma toEquiv_symm (e : G ≃+c[a, b] H) : e.symm.toEquiv = e.toEquiv.symm := rfl
@[simp]
lemma toEquiv_trans (e₁ : G ≃+c[a, b] H) (e₂ : H ≃+c[b, c] K) :
    (e₁.trans e₂).toEquiv = e₁.toEquiv.trans e₂.toEquiv := rfl

The PR does not complete this task, because it would require killing the coercion from EquivLike classes to Equivs (which I am planning to do in a subsequent PR), but it is a significant first step in this direction.