-- 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
rw :
  (↑(↑(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)) :
      α)
⊢ 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) :
          α)
        ⋯)
      ⋯ =
    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) :
            α)
          ⋯)
        ⋯)

Tactic:
rw [← SetLike.coe_eq_coe, ← SetLike.coe_eq_coe]

Premises used: SetLike.coe_eq_coe