-- Lean 4 proof step from Mathlib.GroupTheory.Transfer (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
A : Type u_2
inst_1 : CommGroup A
ϕ : MonoidHom.{u_1, u_2} (↥H) A
R S T : H.LeftTransversal
inst_2 : H.FiniteIndex
q : G ⧸ H
h : Membership.mem (γ := Finset (G ⧸ H)) univ q
simp_rw :
  (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H)
            (HMul.hMul (α := G)
              (↑((⋯.leftQuotientEquiv (S := (↑R : Set G)) : (a : G ⧸ H) → (↑(↑R : Set G) : Type u_1)) q) : G)⁻¹
              (↑((⋯.leftQuotientEquiv (S := (↑S : Set G)) : (a : G ⧸ H) → (↑(↑S : Set G) : Type u_1)) q) : G))
            ⋯ *
          Subtype.mk (p := fun (x : G) ↦ x ∈ H)
            (HMul.hMul (α := G)
              (↑((⋯.leftQuotientEquiv (S := (↑S : Set G)) : (a : G ⧸ H) → (↑(↑S : Set G) : Type u_1)) q) : G)⁻¹
              (↑((⋯.leftQuotientEquiv (S := (↑T : Set G)) : (a : G ⧸ H) → (↑(↑T : Set G) : Type u_1)) q) : G))
            ⋯) :
      G) =
    HMul.hMul (α := G) (↑((⋯.leftQuotientEquiv (S := (↑R : Set G)) : (a : G ⧸ H) → (↑(↑R : Set G) : Type u_1)) q) : G)⁻¹
      (↑((⋯.leftQuotientEquiv (S := (↑T : Set G)) : (a : G ⧸ H) → (↑(↑T : Set G) : Type u_1)) q) : G)
simp_rw₁ :
  HMul.hMul (α := G) (↑((⋯.leftQuotientEquiv (S := (↑R : Set G)) : (a : G ⧸ H) → (↑(↑R : Set G) : Type u_1)) q) : G)⁻¹
        (↑((⋯.leftQuotientEquiv (S := (↑S : Set G)) : (a : G ⧸ H) → (↑(↑S : Set G) : Type u_1)) q) : G) *
      HMul.hMul (α := G)
        (↑((⋯.leftQuotientEquiv (S := (↑S : Set G)) : (a : G ⧸ H) → (↑(↑S : Set G) : Type u_1)) q) : G)⁻¹
        (↑((⋯.leftQuotientEquiv (S := (↑T : Set G)) : (a : G ⧸ H) → (↑(↑T : Set G) : Type u_1)) q) : G) =
    HMul.hMul (α := G) (↑((⋯.leftQuotientEquiv (S := (↑R : Set G)) : (a : G ⧸ H) → (↑(↑R : Set G) : Type u_1)) q) : G)⁻¹
      (↑((⋯.leftQuotientEquiv (S := (↑T : Set G)) : (a : G ⧸ H) → (↑(↑T : Set G) : Type u_1)) q) : G)
⊢ Subtype.mk (p := fun (x : G) ↦ x ∈ H)
        (HMul.hMul (α := G)
          (↑((⋯.leftQuotientEquiv (S := (↑R : Set G)) : (a : G ⧸ H) → (↑(↑R : Set G) : Type u_1)) q) : G)⁻¹
          (↑((⋯.leftQuotientEquiv (S := (↑S : Set G)) : (a : G ⧸ H) → (↑(↑S : Set G) : Type u_1)) q) : G))
        ⋯ *
      Subtype.mk (p := fun (x : G) ↦ x ∈ H)
        (HMul.hMul (α := G)
          (↑((⋯.leftQuotientEquiv (S := (↑S : Set G)) : (a : G ⧸ H) → (↑(↑S : Set G) : Type u_1)) q) : G)⁻¹
          (↑((⋯.leftQuotientEquiv (S := (↑T : Set G)) : (a : G ⧸ H) → (↑(↑T : Set G) : Type u_1)) q) : G))
        ⋯ =
    Subtype.mk (p := fun (x : G) ↦ x ∈ H)
      (HMul.hMul (α := G)
        (↑((⋯.leftQuotientEquiv (S := (↑R : Set G)) : (a : G ⧸ H) → (↑(↑R : Set G) : Type u_1)) q) : G)⁻¹
        (↑((⋯.leftQuotientEquiv (S := (↑T : Set G)) : (a : G ⧸ H) → (↑(↑T : Set G) : Type u_1)) q) : G))
      ⋯
have simp_rw₂ : (↑((sorry.leftQuotientEquiv (S := (↑R : Set G)) : (a : G ⧸ H) → (↑(↑R : Set G) : Type u_1)) q) : G)⁻¹ *
    ((↑((sorry.leftQuotientEquiv (S := (↑S : Set G)) : (a : G ⧸ H) → (↑(↑S : Set G) : Type u_1)) q) : G) *
      HMul.hMul (α := G)
        (↑((sorry.leftQuotientEquiv (S := (↑S : Set G)) : (a : G ⧸ H) → (↑(↑S : Set G) : Type u_1)) q) : G)⁻¹
        (↑((sorry.leftQuotientEquiv (S := (↑T : Set G)) : (a : G ⧸ H) → (↑(↑T : Set G) : Type u_1)) q) : G)) =
  HMul.hMul (α := G) (↑((sorry.leftQuotientEquiv (S := (↑R : Set G)) : (a : G ⧸ H) → (↑(↑R : Set G) : Type u_1)) q) : G)⁻¹
    (↑((sorry.leftQuotientEquiv (S := (↑T : Set G)) : (a : G ⧸ H) → (↑(↑T : Set G) : Type u_1)) q) : G)
Tactic: simp_rw [Subtype.ext_iff, coe_mul, mul_assoc, mul_inv_cancel_left]