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 : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n > 0
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
m : ℕ
hm : n = Nat.succ 0 + m
inr : IsMultiplyPretransitive.{u_1, u_2} (↥(fixingSubgroup M s)) (↥(ofFixingSubgroup M s)) 2
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)

Tactic:
apply isPreprimitive_of_is_two_pretransitive

Premises used: MulAction.isPreprimitive_of_is_two_pretransitive
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
n : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n > 0
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
m : ℕ
hm : n = Nat.succ 0 + m
⊢ s.encard + 1 = (↑(m + 1) : ℕ∞)

Tactic:
simp only [hm, Nat.succ_eq_add_one, zero_add, add_comm 1] at hs

Premises used: Nat.succ_eq_add_one, zero_add, add_comm, OfNat.ofNat
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
n : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n > 0
s : Set α
m : ℕ
hm : n = Nat.succ 0 + m
hs : s.encard + 1 = (↑(m + 1) : ℕ∞)
⊢ s.encard = (↑m : ℕ∞)

Tactic:
ENat.add_left_injective_of_ne_top ENat.one_ne_top hs

Premises used: ENat.one_ne_top, ENat.add_left_injective_of_ne_top
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
n : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n > 0
s : Set α
m : ℕ
hm : n = Nat.succ 0 + m
hs : s.encard + 1 = (↑(m + 1) : ℕ∞)
⊢ s.encard = (↑m : ℕ∞)

Tactic:
exact ENat.add_left_injective_of_ne_top ENat.one_ne_top hs

Premises used: ENat.one_ne_top, ENat.add_left_injective_of_ne_top
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
n : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n > 0
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
m : ℕ
hm : n = Nat.succ 0 + m
⊢ s.encard = (↑m : ℕ∞)

Tactic:
have hs' : s.encard = m := by
      simp only [hm, Nat.succ_eq_add_one, zero_add, add_comm 1] at hs
      exact ENat.add_left_injective_of_ne_top ENat.one_ne_top hs
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
n : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n > 0
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
m : ℕ
hm : n = Nat.succ 0 + m
hs' : s.encard = (↑m : ℕ∞)
⊢ Finite.{u_2 + 1} (↑s : Type u_2)

Tactic:
have : Finite s := Set.finite_of_encard_eq_coe hs'
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
n : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n > 0
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
m : ℕ
hm : n = Nat.succ 0 + m
hs' : s.encard = (↑m : ℕ∞)
this : Finite.{u_2 + 1} (↑s : Type u_2)
inr : s.ncard + 2 = n.succ
⊢ IsMultiplyPretransitive.{u_1, u_2} (↥(fixingSubgroup M s)) (↥(ofFixingSubgroup M s)) 2

Tactic:
apply ofFixingSubgroup.isMultiplyPretransitive (G := M) s (n := n.succ)

Premises used: SubMulAction.ofFixingSubgroup.isMultiplyPretransitive
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
n : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n > 0
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
m : ℕ
hm : n = Nat.succ 0 + m
hs' : s.encard = (↑m : ℕ∞)
this : Finite.{u_2 + 1} (↑s : Type u_2)
⊢ s.ncard + 2 = n.succ

Tactic:
simp [Set.ncard, hs', hm, add_comm 1]

Premises used: add_comm, Set.ncard, OfNat.ofNat
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m : ℕ
hn : IsMultiplyPreprimitive M α 0
hmn : m ≤ 0
hα : (↑0 : ℕ∞) ≤ ENat.card α
zero : IsMultiplyPreprimitive M α 0
⊢ IsMultiplyPreprimitive M α m

Tactic:
rw [Nat.eq_zero_of_le_zero hmn]

Premises used: Nat.eq_zero_of_le_zero
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m : ℕ
hn : IsMultiplyPreprimitive M α 0
hmn : m ≤ 0
hα : (↑0 : ℕ∞) ≤ ENat.card α
⊢ IsMultiplyPreprimitive M α 0

Tactic:
hn
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m : ℕ
hn : IsMultiplyPreprimitive M α 0
hmn : m ≤ 0
hα : (↑0 : ℕ∞) ≤ ENat.card α
⊢ IsMultiplyPreprimitive M α 0

Tactic:
exact hn
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m n : ℕ
hrec : ∀ (hn : IsMultiplyPreprimitive M α n) (hmn : m ≤ n) (hα : (↑n : ℕ∞) ≤ ENat.card α), IsMultiplyPreprimitive M α m
hn : IsMultiplyPreprimitive M α (n + 1)
hmn : m ≤ n + 1
hα : (↑(n + 1) : ℕ∞) ≤ ENat.card α
succ : ∀ (hmn : m = n + 1), IsMultiplyPreprimitive M α m
succ₁ : ∀ (hmn' : m < n + 1), IsMultiplyPreprimitive M α m
⊢ IsMultiplyPreprimitive M α m

Tactic:
rcases Nat.eq_or_lt_of_le hmn with hmn | hmn'

Premises used: Nat.eq_or_lt_of_le
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m n : ℕ
hrec : ∀ (hn : IsMultiplyPreprimitive M α n) (hmn : m ≤ n) (hα : (↑n : ℕ∞) ≤ ENat.card α), IsMultiplyPreprimitive M α m
hn : IsMultiplyPreprimitive M α (n + 1)
hmn_1 : m ≤ n + 1
hα : (↑(n + 1) : ℕ∞) ≤ ENat.card α
hmn : m = n + 1
succ : IsMultiplyPreprimitive M α (n + 1)
⊢ IsMultiplyPreprimitive M α m

Tactic:
rw [hmn]
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m n : ℕ
hrec : ∀ (hn : IsMultiplyPreprimitive M α n) (hmn : m ≤ n) (hα : (↑n : ℕ∞) ≤ ENat.card α), IsMultiplyPreprimitive M α m
hn : IsMultiplyPreprimitive M α (n + 1)
hmn_1 : m ≤ n + 1
hα : (↑(n + 1) : ℕ∞) ≤ ENat.card α
hmn : m = n + 1
⊢ IsMultiplyPreprimitive M α (n + 1)

Tactic:
hn
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m n : ℕ
hrec : ∀ (hn : IsMultiplyPreprimitive M α n) (hmn : m ≤ n) (hα : (↑n : ℕ∞) ≤ ENat.card α), IsMultiplyPreprimitive M α m
hn : IsMultiplyPreprimitive M α (n + 1)
hmn_1 : m ≤ n + 1
hα : (↑(n + 1) : ℕ∞) ≤ ENat.card α
hmn : m = n + 1
⊢ IsMultiplyPreprimitive M α (n + 1)

Tactic:
exact hn
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m n : ℕ
hrec : ∀ (hn : IsMultiplyPreprimitive M α n) (hmn : m ≤ n) (hα : (↑n : ℕ∞) ≤ ENat.card α), IsMultiplyPreprimitive M α m
hn : IsMultiplyPreprimitive M α (n + 1)
hmn : m ≤ n + 1
hα : (↑(n + 1) : ℕ∞) ≤ ENat.card α
hmn' : m < n + 1
succ : (↑n : ℕ∞) ≤ ENat.card α
⊢ IsMultiplyPreprimitive M α m

Tactic:
apply hrec
        (isMultiplyPreprimitive_of_isMultiplyPretransitive_succ M α hα)
        (Nat.lt_succ_iff.mp hmn')

Premises used: MulAction.isMultiplyPreprimitive_of_isMultiplyPretransitive_succ, Nat.lt_succ_iff, Iff.mp
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m n : ℕ
hrec : ∀ (hn : IsMultiplyPreprimitive M α n) (hmn : m ≤ n) (hα : (↑n : ℕ∞) ≤ ENat.card α), IsMultiplyPreprimitive M α m
hn : IsMultiplyPreprimitive M α (n + 1)
hmn : m ≤ n + 1
hα : (↑(n + 1) : ℕ∞) ≤ ENat.card α
hmn' : m < n + 1
⊢ (↑n : ℕ∞) ≤ ENat.card α

Tactic:
le_trans ?_ hα

Premises used: le_trans
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m n : ℕ
hrec : ∀ (hn : IsMultiplyPreprimitive M α n) (hmn : m ≤ n) (hα : (↑n : ℕ∞) ≤ ENat.card α), IsMultiplyPreprimitive M α m
hn : IsMultiplyPreprimitive M α (n + 1)
hmn : m ≤ n + 1
hα : (↑(n + 1) : ℕ∞) ≤ ENat.card α
hmn' : m < n + 1
succ : LE.le (α := ℕ∞) (↑n : ℕ∞) (↑(n + 1) : ℕ∞)
⊢ (↑n : ℕ∞) ≤ ENat.card α

Tactic:
refine le_trans ?_ hα

Premises used: le_trans
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m n : ℕ
hrec : ∀ (hn : IsMultiplyPreprimitive M α n) (hmn : m ≤ n) (hα : (↑n : ℕ∞) ≤ ENat.card α), IsMultiplyPreprimitive M α m
hn : IsMultiplyPreprimitive M α (n + 1)
hmn : m ≤ n + 1
hα : (↑(n + 1) : ℕ∞) ≤ ENat.card α
hmn' : m < n + 1
succ : n ≤ n + 1
⊢ LE.le (α := ℕ∞) (↑n : ℕ∞) (↑(n + 1) : ℕ∞)

Tactic:
rw [ENat.coe_le_coe]

Premises used: ENat.coe_le_coe
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m n : ℕ
hrec : ∀ (hn : IsMultiplyPreprimitive M α n) (hmn : m ≤ n) (hα : (↑n : ℕ∞) ≤ ENat.card α), IsMultiplyPreprimitive M α m
hn : IsMultiplyPreprimitive M α (n + 1)
hmn : m ≤ n + 1
hα : (↑(n + 1) : ℕ∞) ≤ ENat.card α
hmn' : m < n + 1
⊢ n ≤ n + 1

Tactic:
Nat.le_succ n

Premises used: Nat.le_succ
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m n : ℕ
hrec : ∀ (hn : IsMultiplyPreprimitive M α n) (hmn : m ≤ n) (hα : (↑n : ℕ∞) ≤ ENat.card α), IsMultiplyPreprimitive M α m
hn : IsMultiplyPreprimitive M α (n + 1)
hmn : m ≤ n + 1
hα : (↑(n + 1) : ℕ∞) ≤ ENat.card α
hmn' : m < n + 1
⊢ n ≤ n + 1

Tactic:
exact Nat.le_succ n

Premises used: Nat.le_succ
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
n : ℕ
hn : IsMultiplyPreprimitive M α n
m : ℕ
hmn : m ≤ n
hα : (↑n : ℕ∞) ≤ ENat.card α
zero : ∀ (hn : IsMultiplyPreprimitive M α 0) (hmn : m ≤ 0) (hα : (↑0 : ℕ∞) ≤ ENat.card α), IsMultiplyPreprimitive M α m
succ :
  ∀ (n : ℕ)
    (hrec :
      ∀ (hn : IsMultiplyPreprimitive M α n) (hmn : m ≤ n) (hα : (↑n : ℕ∞) ≤ ENat.card α), IsMultiplyPreprimitive M α m)
    (hn : IsMultiplyPreprimitive M α (n + 1)) (hmn : m ≤ n + 1) (hα : (↑(n + 1) : ℕ∞) ≤ ENat.card α),
    IsMultiplyPreprimitive M α m
⊢ IsMultiplyPreprimitive M α m

Tactic:
induction n with
  | zero => rw [Nat.eq_zero_of_le_zero hmn]; exact hn
  | succ n hrec =>
    rcases Nat.eq_or_lt_of_le hmn with hmn | hmn'
    · rw [hmn]; exact hn
    · apply hrec
        (isMultiplyPreprimitive_of_isMultiplyPretransitive_succ M α hα)
        (Nat.lt_succ_iff.mp hmn')
      · refine le_trans ?_ hα; rw [ENat.coe_le_coe]; exact Nat.le_succ n

Premises used: Nat.le_succ, ENat.coe_le_coe, Nat.eq_or_lt_of_le, Nat.eq_zero_of_le_zero, le_trans
-- 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
⊢ (⇑f : (a : α) → β) '' s = t

Tactic:
have hs' : f '' s = t := Set.image_preimage_eq t hf.surjective
-- 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
x : ↥(fixingSubgroup M s)
m : M
hm : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) m
x_1 : (↑t : Type u_4)
y : β
hy : y ∈ t
⊢ ∃ x ∈ s, (f : (a : α) → β) x = y

Tactic:
rw [← hs', Set.mem_image] at hy

Premises used: Set.mem_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
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
x : ↥(fixingSubgroup M s)
m : M
hm : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) m
x_1 : (↑t : Type u_4)
y : β
hy_1 : y ∈ t
hy : ∃ x ∈ s, (f : (a : α) → β) x = y
obtain :
  ∀ (x : α) (hx : x ∈ s) (hx' : (f : (a : α) → β) x = y),
    φ m • (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ t) y hy_1) : β) = (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ t) y hy_1) : β)
⊢ φ m • (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ t) y hy_1) : β) = (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ t) y hy_1) : β)

Tactic:
obtain ⟨x, hx, hx'⟩ := hy
-- 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
x_1 : ↥(fixingSubgroup M s)
m : M
hm : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) m
x_2 : (↑t : Type u_4)
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : (f : (a : α) → β) x = y
simp : φ m • y = y
⊢ φ m • (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ t) y hy) : β) = (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ t) y hy) : β)

Tactic:
simp only
-- 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
x_1 : ↥(fixingSubgroup M s)
m : M
hm : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) m
x_2 : (↑t : Type u_4)
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : (f : (a : α) → β) x = y
rw : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (m • x) : β) ((f : (a : α) → β) x : β)
⊢ φ m • y = y

Tactic:
rw [← hx', ← map_smulₛₗ]

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
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
x_1 : ↥(fixingSubgroup M s)
m : M
hm : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) m
x_2 : (↑t : Type u_4)
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : (f : (a : α) → β) x = y
h₁ : m • x = x
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (m • x) : β) ((f : (a : α) → β) x : β)

Tactic:
apply congr_arg

Premises used: congr_arg
-- 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
x_1 : ↥(fixingSubgroup M s)
m : M
hm : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) m
x_2 : (↑t : Type u_4)
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : (f : (a : α) → β) x = y
h₁ :
  ∀ (hm : ∀ y ∈ s, m • y = y) (x : (↑t : Type u_4)) (y : β) (hy : y ∈ t) (x : α) (hx : x ∈ s)
    (hx' : (f : (a : α) → β) x = y), m • x = x
⊢ m • x = x

Tactic:
rw [mem_fixingSubgroup_iff] at hm

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
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
x_1 : ↥(fixingSubgroup M s)
m : M
hm : ∀ y ∈ s, m • y = y
x_2 : (↑t : Type u_4)
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : (f : (a : α) → β) x = y
⊢ m • x = x

Tactic:
hm x hx
-- 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
x_1 : ↥(fixingSubgroup M s)
m : M
hm : ∀ y ∈ s, m • y = y
x_2 : (↑t : Type u_4)
y : β
hy : y ∈ t
x : α
hx : x ∈ s
hx' : (f : (a : α) → β) x = y
⊢ m • x = x

Tactic:
exact hm x hx
-- 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
⊢ (↑(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:
f.map_smul' m x

Premises used: MulActionHom.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
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))) :
      β)

Tactic:
exact f.map_smul' m x

Premises used: MulActionHom.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
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) ⋯
f' : MulActionHom.{u_1, u_3, u_2, u_4} φ' ↥(ofFixingSubgroup M s) ↥(ofFixingSubgroup N t) :=
  {
    toFun := fun (x : ↥(ofFixingSubgroup M s)) ↦
      match (motive := ↥(ofFixingSubgroup M s) → ↥(ofFixingSubgroup N t)) x 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)
          ⋯,
    map_smul' := ⋯ }
y : β
hy : Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) y
obtain :
  ∀ (x : α) (hx : (f : (a : α) → β) x = y),
    ∃ (a : ↥(ofFixingSubgroup M s)),
      (f' : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t)) a =
        Subtype.mk (p := fun (x : β) ↦
          Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x) y hy
⊢ ∃ (a : ↥(ofFixingSubgroup M s)),
    (f' : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t)) a =
      Subtype.mk (p := fun (x : β) ↦
        Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x) y hy

Tactic:
obtain ⟨x, hx⟩ := hf.right y

Premises used: And.right