-- Lean 4 proof step from Mathlib.GroupTheory.Complement (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
α : Type u_2
inst_1 : MulAction G α
a : α
h2 : ∀ (g : G), ∃ (h : ↥H), h • g • a = a
h : ↥H
h' : (↑(↑H : Set G) : Type u_1)
g : G
hg : g • a = a
hh :
  h •
      ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)) •
        a =
    a
hh' :
  ((↑h : G) *
        ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
          (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G))) •
      a =
    a
h1 : h * h' = 1
rwa :
  ∀ (h1 : (↑(h * h') : G) = (↑1 : G)),
    (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G) =
      (↑(h⁻¹,
              Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G))
                ((↑h : G) *
                  ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
                    (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)))
                hh').2 :
        G)
rwa₁ :
  ∀ (h1 : (↑(h * h') : G) = 1),
    (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G) =
      (↑(h⁻¹,
              Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G))
                ((↑h : G) *
                  ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
                    (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)))
                hh').2 :
        G)
rwa₂ :
  ∀ (h1 : (↑h : G) * (↑h' : G) = 1),
    (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G) =
      (↑(h⁻¹,
              Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G))
                ((↑h : G) *
                  ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
                    (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)))
                hh').2 :
        G)
rwa₃ :
  ∀ (h1 : (↑h : G) * (↑h' : G) = 1) (h1 : g = (↑h : G) * (↑h' : G) * g),
    (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G) =
      (↑(h⁻¹,
              Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G))
                ((↑h : G) *
                  ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
                    (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)))
                hh').2 :
        G)
⊢ (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G) =
    (↑(h⁻¹,
            Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G))
              ((↑h : G) *
                ((↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).1 : G) *
                  (↑(h', Subtype.mk (p := fun (x : G) ↦ x ∈ (↑(MulAction.stabilizer G a) : Set G)) g hg).2 : G)))
              hh').2 :
      G)
have rwa₄ : (h1 : (↑h : G) * (↑h' : G) = 1) → G
Tactic: rwa [Subtype.ext_iff, coe_one, coe_mul, ← right_eq_mul, mul_assoc (↑h) (↑h') g] at h1
Cleared hypotheses: h1