awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
x : ↥(fixingSubgroup M s)
g : M
hg : ∀ y ∈ s, g • y = y
y : β
hy : y ∈ t
suffices : ∃ x ∈ s, y = (f : (a : α) → β) x
⊢ φ g • y = y

Tactic:
suffices ∃ x ∈ s, y = f x by
        obtain ⟨x, hx, rfl⟩ := this
        rwa [← map_smulₛₗ, hg]
-- 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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
x : ↥(fixingSubgroup M s)
g : M
hg : ∀ y ∈ s, g • y = y
y : β
hy : y ∈ t
obtain :
  ∀ (x : α) (hy : Membership.mem (α := β) t ((f : (a : α) → β) x : β)),
    ∃ x_1 ∈ s, Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) x_1 : β)
⊢ ∃ x ∈ s, y = (f : (a : α) → β) x

Tactic:
obtain ⟨x, rfl⟩ := hf.surjective y

Premises used: Function.Bijective.surjective, rfl
-- 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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
x_1 : ↥(fixingSubgroup M s)
g : M
hg : ∀ y ∈ s, g • y = y
x : α
hy : Membership.mem (α := β) t ((f : (a : α) → β) x : β)
⊢ ∃ x_2 ∈ s, Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) x_2 : β)

Tactic:
simpa only [Set.mem_image, t, eq_comm] using hy

Premises used: Set.mem_image, eq_comm
-- 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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
x : ↥(ofFixingSubgroup M s)
simp : (↑x : α) ∉ s
⊢ Membership.mem (α := β) (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t)
    ((f : (a : α) → β) (↑x : α) : β)

Tactic:
simp only [mem_ofFixingSubgroup_iff, Set.mem_image, hf.injective.eq_iff, exists_eq_right, t]

Premises used: Function.Injective.eq_iff, Set.mem_image, exists_eq_right, Function.Bijective.injective, SubMulAction.mem_ofFixingSubgroup_iff
-- 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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
x : ↥(ofFixingSubgroup M s)
⊢ (↑x : α) ∉ s

Tactic:
x.prop

Premises used: Set.Mem, setOf, Subtype.prop, Not
-- 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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
x : ↥(ofFixingSubgroup M s)
⊢ (↑x : α) ∉ s

Tactic:
exact x.prop

Premises used: Subtype.prop
-- 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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
m : ↥(fixingSubgroup M s)
x : ↥(ofFixingSubgroup M s)
⊢ Subtype.mk (p := fun (x : β) ↦
      Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
      ((f : (a : α) → β) (↑(m • x) : α)) ⋯ =
    HSMul.hSMul (β := ↥(ofFixingSubgroup N t)) (ψ m)
      (Subtype.mk (p := fun (x : β) ↦
          Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
          ((f : (a : α) → β) (↑x : α)) ⋯ :
        ↥(ofFixingSubgroup N t))

Tactic:
simp [subgroup_smul_def, map_smulₛₗ, ψ]

Premises used: MulActionSemiHomClass.map_smulₛₗ, MulAction.subgroup_smul_def
-- 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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
right : IsPreprimitive.{u_3, u_4} ↥(fixingSubgroup N t) ↥(ofFixingSubgroup N t)
right₁ : Function.Surjective ψ
right₂ :
  Function.Bijective.{u_2 + 1, u_4 + 1} (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup N t))
    (⇑g : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t))
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)

Tactic:
rw [isPreprimitive_congr (f := g)]

Premises used: MulAction.isPreprimitive_congr
-- 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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
right : t.encard + 1 = (↑n : ℕ∞)
⊢ IsPreprimitive.{u_3, u_4} ↥(fixingSubgroup N t) ↥(ofFixingSubgroup N t)

Tactic:
apply H.isPreprimitive_ofFixingSubgroup

Premises used: MulAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup
-- 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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
⊢ t.encard + 1 = (↑n : ℕ∞)

Tactic:
simp [← hs, t, hf.injective.injOn.encard_image]

Premises used: Function.Injective.injOn, Function.Bijective.injective, Set.InjOn.encard_image
-- 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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
k : N
hk : Membership.mem (γ := Subgroup N) (fixingSubgroup N t) k
right :
  ∀ (k : M) (hk : Membership.mem (γ := Subgroup N) (fixingSubgroup N t) (φ k)),
    ∃ (a : ↥(fixingSubgroup M s)),
      ψ a = Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ k) hk
⊢ ∃ (a : ↥(fixingSubgroup M s)),
    ψ a = Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) k hk

Tactic:
obtain ⟨k, rfl⟩ := hφ k

Premises used: rfl
-- 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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
k : M
hk : Membership.mem (γ := Subgroup N) (fixingSubgroup N t) (φ k)
this : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
w : ↥(fixingSubgroup M s)
h :
  ψ (Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) k this) =
    Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ k) hk
⊢ ∃ (a : ↥(fixingSubgroup M s)),
    ψ a = Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ k) hk

Tactic:
use ⟨k, this⟩
-- 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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
k : M
hk : Membership.mem (γ := Subgroup N) (fixingSubgroup N t) (φ k)
right : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k
⊢ ∃ (a : ↥(fixingSubgroup M s)),
    ψ a = Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ k) hk

Tactic:
suffices k ∈ fixingSubgroup M s by
        use ⟨k, this⟩
-- 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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
k : M
hk : Membership.mem (γ := Subgroup N) (fixingSubgroup N t) (φ k)
right : ∀ (hk : ∀ (y : β), Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) y → φ k • y = y), ∀ y ∈ s, k • y = y
⊢ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) k

Tactic:
simp only [mem_fixingSubgroup_iff, t] at hk ⊢

Premises used: mem_fixingSubgroup_iff
-- 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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
k : M
hk : ∀ (y : β), Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) y → φ k • y = y
y : α
hy : y ∈ s
right : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (k • y) : β) ((f : (a : α) → β) y : β)
⊢ k • y = y

Tactic:
apply hf.injective

Premises used: Function.Bijective.injective
-- 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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
k : M
hk : ∀ (y : β), Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) y → φ k • y = y
y : α
hy : y ∈ s
right : Membership.mem.{u_4, u_4} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' s) ((f : (a : α) → β) y : β)
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (k • y) : β) ((f : (a : α) → β) y : β)

Tactic:
rw [map_smulₛₗ, hk]

Premises used: MulActionSemiHomClass.map_smulₛₗ
-- 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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
k : M
hk : ∀ (y : β), Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) y → φ k • y = y
y : α
hy : y ∈ s
⊢ Membership.mem.{u_4, u_4} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' s) ((f : (a : α) → β) y : β)

Tactic:
Set.mem_image_of_mem (⇑f) hy

Premises used: Set.Mem, Set.mem_image_of_mem, DFunLike.coe
-- 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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
k : M
hk : ∀ (y : β), Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) y → φ k • y = y
y : α
hy : y ∈ s
⊢ Membership.mem.{u_4, u_4} (α := β) (γ := Set β) ((⇑f : (a : α) → β) '' s) ((f : (a : α) → β) y : β)

Tactic:
exact Set.mem_image_of_mem (⇑f) hy

Premises used: Set.mem_image_of_mem, DFunLike.coe
-- 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
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective.{u_2 + 1, u_4 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
t : Set β := (⇑f : (a : α) → β) '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun (x : ↥(fixingSubgroup M s)) ↦
    match (motive := ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t)) x with
    | ⟨g, hg⟩ => Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Subgroup N) (fixingSubgroup N t) x) (φ g) ⋯
g : MulActionHom.{u_1, u_3, u_2, u_4} ψ ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x)
        ((f : (a : α) → β) (↑x : α)) ⋯,
    map_smul' := ⋯ }
right :
  Function.Injective.{u_2 + 1, u_4 + 1} (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup N t))
    (⇑g : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t))
right₁ :
  Function.Surjective.{u_2 + 1, u_4 + 1} (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup N t))
    (⇑g : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t))
⊢ Function.Bijective.{u_2 + 1, u_4 + 1} (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup N t))
    (⇑g : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t))

Tactic:
constructor