-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : IsPretransitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
a : α
ha : a ∈ sᶜ ∩ (g • s)ᶜ
ha' : a ∈ (s ∩ g • s)ᶜ
x : α
hx_1 :
  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α) (ofFixingSubgroup M (s ∩ g • s)) x
hx : x ∉ g • s
hg'x : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • x)
hg'a : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) (g⁻¹ • a)
k : M
hk : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
hkax_1 :
  Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk •
      Subtype.mk (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • a)
        hg'a =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • x) hg'x
hkax :
  (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk •
          Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) (g⁻¹ • a)
            hg'a) :
      α) =
    g⁻¹ • x
h :
  ∀
    (hkax :
      Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k hk •
          (↑(Subtype.mk (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x)
                (g⁻¹ • a) hg'a) :
            α) =
        g⁻¹ • x),
    (↑(HSMul.hSMul (α := ↥(fixingSubgroup M (s ∩ g • s)))
            (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∩ g • s)) x)
              (g * k * g⁻¹) ⋯)
            (Subtype.mk (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
                (ofFixingSubgroup M (s ∩ g • s)) x)
              a ha')) :
        α) =
      x
h₁ :
  ∀
    (hkax :
      k •
          (↑(Subtype.mk (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x)
                (g⁻¹ • a) hg'a) :
            α) =
        g⁻¹ • x),
    (↑(HSMul.hSMul (α := ↥(fixingSubgroup M (s ∩ g • s)))
            (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∩ g • s)) x)
              (g * k * g⁻¹) ⋯)
            (Subtype.mk (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
                (ofFixingSubgroup M (s ∩ g • s)) x)
              a ha')) :
        α) =
      x
h₂ :
  ∀
    (hkax :
      g •
          k •
            (↑(Subtype.mk (p := fun (x : α) ↦
                  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x)
                  (g⁻¹ • a) hg'a) :
              α) =
        x),
    (↑(HSMul.hSMul (α := ↥(fixingSubgroup M (s ∩ g • s)))
            (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∩ g • s)) x)
              (g * k * g⁻¹) ⋯)
            (Subtype.mk (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
                (ofFixingSubgroup M (s ∩ g • s)) x)
              a ha')) :
        α) =
      x
h₃ :
  ∀
    (hkax :
      (g * k) •
          (↑(Subtype.mk (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x)
                (g⁻¹ • a) hg'a) :
            α) =
        x),
    (↑(HSMul.hSMul (α := ↥(fixingSubgroup M (s ∩ g • s)))
            (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∩ g • s)) x)
              (g * k * g⁻¹) ⋯)
            (Subtype.mk (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
                (ofFixingSubgroup M (s ∩ g • s)) x)
              a ha')) :
        α) =
      x
h₄ h₅ h₆ h₇ :
  ∀ (hkax : (g * k * g⁻¹) • a = x),
    (↑(HSMul.hSMul (α := ↥(fixingSubgroup M (s ∩ g • s)))
            (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∩ g • s)) x)
              (g * k * g⁻¹) ⋯)
            (Subtype.mk (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
                (ofFixingSubgroup M (s ∩ g • s)) x)
              a ha')) :
        α) =
      x
⊢ (↑(HSMul.hSMul (α := ↥(fixingSubgroup M (s ∩ g • s)))
          (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∩ g • s)) x)
            (g * k * g⁻¹) ⋯)
          (Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∩ g • s))) α)
              (ofFixingSubgroup M (s ∩ g • s)) x)
            a ha')) :
      α) =
    x

Tactic:
rwa [SetLike.val_smul, Subgroup.mk_smul, eq_inv_smul_iff, smul_smul, smul_smul] at hkax

Premises used: smul_smul, SetLike.val_smul, Subgroup.mk_smul, eq_inv_smul_iff