no goals
G : Type u_2
inst✝² : Group G
H : Subgroup G
A : Type u_1
inst✝¹ : CommGroup A
ϕ : { x // x ∈ H } →* A
R S T : ↑(leftTransversals ↑H)
inst✝ : FiniteIndex H
q : G ⧸ H
x✝ : q ∈ univ
⊢ {
        val :=
          (↑(↑(MemLeftTransversals.toEquiv (_ : ↑R ∈ leftTransversals ↑H)) q))⁻¹ *
            ↑(↑(MemLeftTransversals.toEquiv (_ : ↑S ∈ leftTransversals ↑H)) q),
        property :=
          (_ :
            (↑(↑(MemLeftTransversals.toEquiv (_ : ↑R ∈ leftTransversals ↑H)) q))⁻¹ *
                ↑(↑(MemLeftTransversals.toEquiv (_ : ↑S ∈ leftTransversals ↑H)) q) ∈
              H) } *
      {
        val :=
          (↑(↑(MemLeftTransversals.toEquiv (_ : ↑S ∈ leftTransversals ↑H)) q))⁻¹ *
            ↑(↑(MemLeftTransversals.toEquiv (_ : ↑T ∈ leftTransversals ↑H)) q),
        property :=
          (_ :
            (↑(↑(MemLeftTransversals.toEquiv (_ : ↑S ∈ leftTransversals ↑H)) q))⁻¹ *
                ↑(↑(MemLeftTransversals.toEquiv (_ : ↑T ∈ leftTransversals ↑H)) q) ∈
              H) } =
    {
      val :=
        (↑(↑(MemLeftTransversals.toEquiv (_ : ↑R ∈ leftTransversals ↑H)) q))⁻¹ *
          ↑(↑(MemLeftTransversals.toEquiv (_ : ↑T ∈ leftTransversals ↑H)) q),
      property :=
        (_ :
          (↑(↑(MemLeftTransversals.toEquiv (_ : ↑R ∈ leftTransversals ↑H)) q))⁻¹ *
              ↑(↑(MemLeftTransversals.toEquiv (_ : ↑T ∈ leftTransversals ↑H)) q) ∈
            H) }
simp_rw [Subtype.ext_iff, coe_mul, coe_mk, mul_assoc, mul_inv_cancel_left]