-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
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) :
          α)
        ⋯)
      ⋯ =
    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) :
            α)
          ⋯)
        ⋯)
have 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) :
                α)
              sorry)
            sorry) :
        ↥(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)
                sorry)
              sorry)
            (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) :
                  α)
                sorry)
              sorry)) :
        ↥(ofFixingSubgroup M s)) :
    α)
Tactic: rw [← SetLike.coe_eq_coe, ← SetLike.coe_eq_coe]