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
g : G
x✝² : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex H
x✝¹ : G ⧸ H
x✝ : x✝¹ ∈ univ
⊢ {
      val :=
        (↑(↑(MemLeftTransversals.toEquiv (_ : ↑(g • S) ∈ leftTransversals ↑H)) x✝¹))⁻¹ *
          ↑(↑(MemLeftTransversals.toEquiv (_ : ↑(g • T) ∈ leftTransversals ↑H)) x✝¹),
      property :=
        (_ :
          (↑(↑(MemLeftTransversals.toEquiv (_ : ↑(g • S) ∈ leftTransversals ↑H)) x✝¹))⁻¹ *
              ↑(↑(MemLeftTransversals.toEquiv (_ : ↑(g • T) ∈ leftTransversals ↑H)) x✝¹) ∈
            H) } =
    {
      val :=
        (↑(↑(MemLeftTransversals.toEquiv (_ : ↑S ∈ leftTransversals ↑H)) ((fun q x => g⁻¹ • q) x✝¹ x✝)))⁻¹ *
          ↑(↑(MemLeftTransversals.toEquiv (_ : ↑T ∈ leftTransversals ↑H)) ((fun q x => g⁻¹ • q) x✝¹ x✝)),
      property :=
        (_ :
          (↑(↑(MemLeftTransversals.toEquiv (_ : ↑S ∈ leftTransversals ↑H)) ((fun q x => g⁻¹ • q) x✝¹ x✝)))⁻¹ *
              ↑(↑(MemLeftTransversals.toEquiv (_ : ↑T ∈ leftTransversals ↑H)) ((fun q x => g⁻¹ • q) x✝¹ x✝)) ∈
            H) }
simp_rw [coe_mk, smul_apply_eq_smul_apply_inv_smul, smul_eq_mul, mul_inv_rev, mul_assoc,
  inv_mul_cancel_left]