awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultiplePrimitivity (hypothesis)
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
⊢ IsMultiplyPretransitive.{u_1, u_2} (↥(fixingSubgroup M s)) (↥(ofFixingSubgroup M s)) 2
have hs' : 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
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultiplePrimitivity (hypothesis)
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 : ℕ∞)
⊢ IsMultiplyPretransitive.{u_1, u_2} (↥(fixingSubgroup M s)) (↥(ofFixingSubgroup M s)) 2
have this : Finite.{u_2 + 1} (↑s : Type u_2)
Tactic: have : Finite s := Set.finite_of_encard_eq_coe hs'
-- 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 : ℕ
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)
⊢ IsMultiplyPretransitive.{u_1, u_2} (↥(fixingSubgroup M s)) (↥(ofFixingSubgroup M s)) 2
have inr : s.ncard + 2 = n.succ
Tactic: apply ofFixingSubgroup.isMultiplyPretransitive (G := M) s (n := n.succ)
-- 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 α
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 α
⊢ IsMultiplyPreprimitive M α m
have succ : ∀ (hmn : m = n + 1), IsMultiplyPreprimitive M α m
Tactic: rcases Nat.eq_or_lt_of_le hmn with hmn | hmn'
-- 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 α
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
⊢ IsMultiplyPreprimitive M α m
have succ₁ : ∀ (hmn' : m < n + 1), IsMultiplyPreprimitive M α m
Tactic: rcases Nat.eq_or_lt_of_le hmn with hmn | hmn'
-- 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 α
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
⊢ IsMultiplyPreprimitive M α m
have succ : (↑n : ℕ∞) ≤ ENat.card α
Tactic: apply hrec
        (isMultiplyPreprimitive_of_isMultiplyPretransitive_succ M α hα)
        (Nat.lt_succ_iff.mp hmn')
-- 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 α
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 α
have succ : LE.le (α := ℕ∞) (↑n : ℕ∞) (↑(n + 1) : ℕ∞)
Tactic: refine le_trans ?_ hα
-- 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 α
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
⊢ LE.le (α := ℕ∞) (↑n : ℕ∞) (↑(n + 1) : ℕ∞)
have succ : n ≤ n + 1
Tactic: rw [ENat.coe_le_coe]
-- 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 : ℕ
hn : IsMultiplyPreprimitive M α n
m : ℕ
hmn : m ≤ n
hα : (↑n : ℕ∞) ≤ ENat.card α
⊢ IsMultiplyPreprimitive M α m
have zero : ∀ (hn : IsMultiplyPreprimitive M α 0) (hmn : m ≤ 0) (hα : (↑0 : ℕ∞) ≤ ENat.card α), 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
Cleared hypotheses: n, hn, hmn, hα
-- 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 : ℕ
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
⊢ IsMultiplyPreprimitive M α m
have 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
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
Cleared hypotheses: n, hn, hmn, hα
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultiplePrimitivity (hypothesis)
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
⊢ IsPreprimitive.{u_3, u_4} ↥(fixingSubgroup N t) ↥(ofFixingSubgroup N t)
have hs' : (⇑f : (a : α) → β) '' s = t
Tactic: have hs' : f '' s = t := Set.image_preimage_eq t hf.surjective
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultiplePrimitivity (hypothesis)
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
⊢ φ m • (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ t) y hy) : β) = (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ t) y hy) : β)
have hy₁ : ∃ x ∈ s, (f : (a : α) → β) x = y
Tactic: rw [← hs', Set.mem_image] at hy
-- 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
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
⊢ φ m • (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ t) y hy_1) : β) = (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ t) y hy_1) : β)
have 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) : β)
Tactic: obtain ⟨x, hx, hx'⟩ := hy
Cleared hypotheses: hy
-- 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
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
⊢ φ m • (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ t) y hy) : β) = (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ t) y hy) : β)
have simp : φ m • y = y
Tactic: simp only
-- 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
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
⊢ φ m • y = y
have rw : Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (m • x) : β) ((f : (a : α) → β) x : β)
Tactic: rw [← hx', ← map_smulₛₗ]
-- 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
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
⊢ Eq.{u_4 + 1} (α := β) ((f : (a : α) → β) (m • x) : β) ((f : (a : α) → β) x : β)
have h₁ : m • x = x
Tactic: apply congr_arg
-- 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
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
⊢ m • x = x
have 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
Tactic: rw [mem_fixingSubgroup_iff] at hm
Cleared hypotheses: hm, x_2, y, hy, x, hx, hx'
-- 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) ⋯
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨x, hx⟩ := hf.right y
-- 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) ⋯
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
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
have h₁ : (f' : (a : ↥(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 sorry) =
  Subtype.mk (p := fun (x : β) ↦
    Membership.mem (γ := SubMulAction.{u_3, u_4} (↥(fixingSubgroup N t)) β) (ofFixingSubgroup N t) x) y hy
Tactic: use ⟨x, ?_⟩
-- 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) ⋯
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
x : α
hx : (f : (a : α) → β) x = y
h₁ :
  (f' : (a : ↥(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 ⋯) =
    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
have w : Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x
Tactic: use ⟨x, ?_⟩
-- 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_1 : 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
x : α
hx : (f : (a : α) → β) x = y
h : x ∈ s
⊢ False
have w : y ∈ t
Tactic: apply hy
-- 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_1 : 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
x : α
hx : (f : (a : α) → β) x = y
h : x ∈ s
⊢ y ∈ t
have w : Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' s) y
Tactic: rw [← hs']
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.MultiplePrimitivity (hypothesis)
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' := ⋯ }
⊢ IsPreprimitive.{u_3, u_4} ↥(fixingSubgroup N t) ↥(ofFixingSubgroup N t)
have hf' : Function.Surjective.{u_2 + 1, u_4 + 1} (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup N t))
  (⇑f' : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t))
Tactic: have hf' : Function.Surjective f' := by
      rintro ⟨y, hy⟩
      obtain ⟨x, hx⟩ := hf.right y
      use ⟨x, ?_⟩
      · simpa only [f', ← Subtype.coe_inj] using hx
      · intro h
        apply hy
        rw [← hs']
        exact ⟨x, h, hx⟩
-- 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) ⋯
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' := ⋯ }
hf' :
  Function.Surjective.{u_2 + 1, u_4 + 1} (α := ↥(ofFixingSubgroup M s)) (β := ↥(ofFixingSubgroup N t))
    (⇑f' : (a : ↥(ofFixingSubgroup M s)) → ↥(ofFixingSubgroup N t))
⊢ s.encard + 1 = (↑n : ℕ∞)
have rw : s.encard + 1 = t.encard + 1
Tactic: rw [← ht, ← hs', hf.injective.encard_image]