-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s_1 s t : Set α
x_1 : ↥(fixingSubgroup M (s ∪ t))
x_2 : ↥(ofFixingSubgroup M (s ∪ t))
m : M
hm : Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∪ t)) m
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∪ t))) α) (ofFixingSubgroup M (s ∪ t)) x
⊢ (↑(↑(Subtype.mk (p := fun (x : ↥(ofFixingSubgroup M s)) ↦
              Membership.mem (γ :=
                SubMulAction.{u_1, u_2}
                  ↥(fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(ofFixingSubgroup M s))
                      (Subtype.val (p := fun (x : α) ↦
                          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s)
                            x) ⁻¹'
                        t))
                  ↥(ofFixingSubgroup M s))
                (ofFixingSubgroup (↥(fixingSubgroup M s))
                  (Subtype.val (p := fun (x : α) ↦
                      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s)
                        x) ⁻¹'
                    t))
                x)
              (Subtype.mk (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x)
                (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∪ t)) x) m hm •
                      Subtype.mk (p := fun (x : α) ↦
                        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∪ t))) α)
                          (ofFixingSubgroup M (s ∪ t)) x)
                        x hx) :
                  α)
                ⋯)
              ⋯) :
          ↥(ofFixingSubgroup M s)) :
      α) =
    (↑(↑(HSMul.hSMul (β :=
              ↥(ofFixingSubgroup (↥(fixingSubgroup M s))
                  (Subtype.val (p := fun (x : α) ↦
                      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s)
                        x) ⁻¹'
                    t)))
              (Subtype.mk (p := fun (x : ↥(fixingSubgroup M s)) ↦
                Membership.mem (γ := Subgroup ↥(fixingSubgroup M s))
                  (fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(ofFixingSubgroup M s))
                    (Subtype.val (p := fun (x : α) ↦
                        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s)
                          x) ⁻¹'
                      t))
                  x)
                (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x)
                  (↑(Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M (s ∪ t)) x) m
                        hm) :
                    M)
                  ⋯)
                ⋯)
              (Subtype.mk (p := fun (x : ↥(ofFixingSubgroup M s)) ↦
                Membership.mem (γ :=
                  SubMulAction.{u_1, u_2}
                    ↥(fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(ofFixingSubgroup M s))
                        (Subtype.val (p := fun (x : α) ↦
                            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α)
                              (ofFixingSubgroup M s) x) ⁻¹'
                          t))
                    ↥(ofFixingSubgroup M s))
                  (ofFixingSubgroup (↥(fixingSubgroup M s))
                    (Subtype.val (p := fun (x : α) ↦
                        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s)
                          x) ⁻¹'
                      t))
                  x)
                (Subtype.mk (p := fun (x : α) ↦
                  Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x)
                  (↑(Subtype.mk (p := fun (x : α) ↦
                        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M (s ∪ t))) α)
                          (ofFixingSubgroup M (s ∪ t)) x)
                        x hx) :
                    α)
                  ⋯)
                ⋯)) :
          ↥(ofFixingSubgroup M s)) :
      α)

Tactic:
exact subgroup_smul_def ⟨m, hm⟩ x

Premises used: Subtype.mk, MulAction.subgroup_smul_def