-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
N : Type u_3
β : Type u_4
inst_2 : Group N
inst_3 : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
h : IsMultiplyPreprimitive M α n
t : Set β
ht : t.encard + 1 = (↑n : ℕ∞)
s : Set α := (⇑f : (a : α) → β) ⁻¹' t
hs' : (⇑f : (a : α) → β) '' s = t
φ' : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨m, hm⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ m) ⋯
x_1 : ↥(fixingSubgroup M s)
x_2 : ↥(ofFixingSubgroup M s)
m : M
hm : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) m
x : α
hx : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x
rw :
  (↑(match (motive := ↥(ofFixingSubgroup M s) → ↥(ofFixingSubgroup N t))
          Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) m hm •
            Subtype.mk (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x
              hx with
        | ⟨x, hx⟩ =>
          Subtype.mk (p := fun (x : β) ↦
            Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
            (f.toFun x) ⋯) :
      β) =
    (↑(HSMul.hSMul (β := ↥(ofFixingSubgroup N t))
          (φ' (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) m hm))
          (match (motive := ↥(ofFixingSubgroup M s) → ↥(ofFixingSubgroup N t))
              Subtype.mk (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x
                hx with
            | ⟨x, hx⟩ =>
              Subtype.mk (p := fun (x : β) ↦
                Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
                (f.toFun x) ⋯ :
            ↥(ofFixingSubgroup N t))) :
      β)
⊢ (match (motive := ↥(ofFixingSubgroup M s) → ↥(ofFixingSubgroup N t))
      Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) m hm •
        Subtype.mk (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx with
    | ⟨x, hx⟩ =>
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x) (f.toFun x)
        ⋯) =
    HSMul.hSMul (β := ↥(ofFixingSubgroup N t))
      (φ' (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) m hm))
      (match (motive := ↥(ofFixingSubgroup M s) → ↥(ofFixingSubgroup N t))
          Subtype.mk (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) x hx with
        | ⟨x, hx⟩ =>
          Subtype.mk (p := fun (x : β) ↦
            Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
            (f.toFun x) ⋯ :
        ↥(ofFixingSubgroup N t))

Tactic:
rw [← SetLike.coe_eq_coe]

Premises used: SetLike.coe_eq_coe