-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultiplePrimitivity (goal)
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
⊢ (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))
have 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)
          sorry) :
    β) =
  (↑(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) sorry :
          ↥(ofFixingSubgroup N t))) :
    β)
Tactic: rw [← SetLike.coe_eq_coe]