-- Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
a : α
s : Set ↥(ofStabilizer M a)
x : α
hx :
  Membership.mem (γ :=
    SubMulAction.{u_1, u_2}
      (↥(fixingSubgroup M
          (insert a
            (Subtype.val (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
              s))))
      α)
    (ofFixingSubgroup M
      (insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          s)))
    x
y : α
hy :
  Membership.mem (γ :=
    SubMulAction.{u_1, u_2}
      (↥(fixingSubgroup M
          (insert a
            (Subtype.val (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
              s))))
      α)
    (ofFixingSubgroup M
      (insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          s)))
    y
h :
  Eq (α := ↥(ofFixingSubgroup (↥(stabilizer M a)) s))
    ((ofFixingSubgroup_insert_map a s :
          (a_1 : ↥(ofFixingSubgroup M (insert a (Subtype.val '' s)))) → ↥(ofFixingSubgroup (↥(stabilizer M a)) s))
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ :=
            SubMulAction.{u_1, u_2}
              (↥(fixingSubgroup M
                  (insert a
                    (Subtype.val (p := fun (x : α) ↦
                        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
                      s))))
              α)
            (ofFixingSubgroup M
              (insert a
                (Subtype.val (p := fun (x : α) ↦
                    Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
                  s)))
            x)
          x hx) :
      ↥(ofFixingSubgroup (↥(stabilizer M a)) s))
    ((ofFixingSubgroup_insert_map a s :
          (a_1 : ↥(ofFixingSubgroup M (insert a (Subtype.val '' s)))) → ↥(ofFixingSubgroup (↥(stabilizer M a)) s))
        (Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ :=
            SubMulAction.{u_1, u_2}
              (↥(fixingSubgroup M
                  (insert a
                    (Subtype.val (p := fun (x : α) ↦
                        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
                      s))))
              α)
            (ofFixingSubgroup M
              (insert a
                (Subtype.val (p := fun (x : α) ↦
                    Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
                  s)))
            x)
          y hy) :
      ↥(ofFixingSubgroup (↥(stabilizer M a)) s))
⊢ Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ :=
        SubMulAction.{u_1, u_2}
          (↥(fixingSubgroup M
              (insert a
                (Subtype.val (p := fun (x : α) ↦
                    Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
                  s))))
          α)
        (ofFixingSubgroup M
          (insert a
            (Subtype.val (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
              s)))
        x)
      x hx =
    Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ :=
        SubMulAction.{u_1, u_2}
          (↥(fixingSubgroup M
              (insert a
                (Subtype.val (p := fun (x : α) ↦
                    Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
                  s))))
          α)
        (ofFixingSubgroup M
          (insert a
            (Subtype.val (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
              s)))
        x)
      y hy

Tactic:
simpa only [← Subtype.coe_inj, ofFixingSubgroup_insert_map_apply] using h

Premises used: SubMulAction.ofFixingSubgroup_insert_map_apply, Subtype.coe_inj