awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
inl : ∀ (hα4 : Nat.card α < 4), alternatingGroup α ≤ G
inr inr₁ : ∀ (hα4 : Nat.card α ≥ 4), alternatingGroup α ≤ G
inr₂ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), alternatingGroup α ≤ G
inr₃ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
inr₄ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), IsMultiplyPreprimitive (↥G) α (Nat.card α - 2)
inr₅ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), IsMultiplyPreprimitive (↥G) α (n + 2)
inr₆ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), (↑g.support : Set α)ᶜ.ncard = n + 1
inr₇ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), n + 2 < Nat.card α
⊢ alternatingGroup α ≤ G
have inr₈ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4),
  IsPreprimitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
Tactic: classical
  rcases Nat.lt_or_ge (Nat.card α) 4 with hα4 | hα4
  · -- trivial case : Fintype.card α ≤ 3
    rw [Nat.lt_succ_iff] at hα4
    apply alternatingGroup_le_of_index_le_two
    rw [← Nat.mul_le_mul_right_iff (k := Nat.card G) (Nat.card_pos),
      Subgroup.index_mul_card, Nat.card_perm]
    apply le_trans (Nat.factorial_le hα4)
    rw [show Nat.factorial 3 = 2 * 3 by simp [Nat.factorial]]
    simp only [mul_le_mul_iff_right₀, Nat.succ_pos]
    apply Nat.le_of_dvd Nat.card_pos
    suffices 3 = orderOf (⟨g, hg⟩ : G) by
      rw [this, Nat.card_eq_fintype_card]
      exact orderOf_dvd_card
    simp only [orderOf_mk, h3g.orderOf]
    -- important case : Nat.card α ≥ 4
  obtain ⟨n, hn⟩ := Nat.exists_eq_add_of_le' hα4
  apply IsMultiplyPretransitive.alternatingGroup_le
  suffices IsMultiplyPreprimitive G α (Nat.card α - 2) from
    IsMultiplyPreprimitive.isMultiplyPretransitive ..
  rw [show Nat.card α - 2 = n + 2 by grind]
  apply hG.isMultiplyPreprimitive (s := (g.supportᶜ : Set α))
  · apply Nat.add_left_cancel
    rw [Set.ncard_add_ncard_compl, Set.ncard_coe_finset,
      h3g.card_support, add_comm, hn]
  · grind
  have := isPretransitive_of_isCycle_mem h3g.isCycle hg
  apply IsPreprimitive.of_prime_card
  convert! Nat.prime_three
  rw [Nat.card_eq_fintype_card, Fintype.card_subtype, ← h3g.card_support]
  apply congr_arg
  ext x
  simp [SubMulAction.mem_ofFixingSubgroup_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
inl : ∀ (hα4 : Nat.card α < 4), alternatingGroup α ≤ G
inr inr₁ : ∀ (hα4 : Nat.card α ≥ 4), alternatingGroup α ≤ G
inr₂ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), alternatingGroup α ≤ G
inr₃ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
inr₄ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), IsMultiplyPreprimitive (↥G) α (Nat.card α - 2)
inr₅ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), IsMultiplyPreprimitive (↥G) α (n + 2)
inr₆ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), (↑g.support : Set α)ᶜ.ncard = n + 1
inr₇ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), n + 2 < Nat.card α
inr₈ :
  ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4),
    IsPreprimitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
inr₉ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4), n + 2 < Nat.card α
inr₁₀ inr₁₁ :
  ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4),
    IsPreprimitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
⊢ alternatingGroup α ≤ G
have inr₁₂ : ∀ (hα4 : Nat.card α ≥ 4) (n : ℕ) (hn : Nat.card α = n + 4)
  (this :
    IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)),
  IsPreprimitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
Tactic: classical
  rcases Nat.lt_or_ge (Nat.card α) 4 with hα4 | hα4
  · -- trivial case : Fintype.card α ≤ 3
    rw [Nat.lt_succ_iff] at hα4
    apply alternatingGroup_le_of_index_le_two
    rw [← Nat.mul_le_mul_right_iff (k := Nat.card G) (Nat.card_pos),
      Subgroup.index_mul_card, Nat.card_perm]
    apply le_trans (Nat.factorial_le hα4)
    rw [show Nat.factorial 3 = 2 * 3 by simp [Nat.factorial]]
    simp only [mul_le_mul_iff_right₀, Nat.succ_pos]
    apply Nat.le_of_dvd Nat.card_pos
    suffices 3 = orderOf (⟨g, hg⟩ : G) by
      rw [this, Nat.card_eq_fintype_card]
      exact orderOf_dvd_card
    simp only [orderOf_mk, h3g.orderOf]
    -- important case : Nat.card α ≥ 4
  obtain ⟨n, hn⟩ := Nat.exists_eq_add_of_le' hα4
  apply IsMultiplyPretransitive.alternatingGroup_le
  suffices IsMultiplyPreprimitive G α (Nat.card α - 2) from
    IsMultiplyPreprimitive.isMultiplyPretransitive ..
  rw [show Nat.card α - 2 = n + 2 by grind]
  apply hG.isMultiplyPreprimitive (s := (g.supportᶜ : Set α))
  · apply Nat.add_left_cancel
    rw [Set.ncard_add_ncard_compl, Set.ncard_coe_finset,
      h3g.card_support, add_comm, hn]
  · grind
  have := isPretransitive_of_isCycle_mem h3g.isCycle hg
  apply IsPreprimitive.of_prime_card
  convert! Nat.prime_three
  rw [Nat.card_eq_fintype_card, Fintype.card_subtype, ← h3g.card_support]
  apply congr_arg
  ext x
  simp [SubMulAction.mem_ofFixingSubgroup_iff]
-- 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 α
⊢ IsMultiplyPreprimitive M α 1 ↔ IsPreprimitive M α
have mp : IsMultiplyPreprimitive M α 1 → IsPreprimitive M α
Tactic: constructor
-- 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 α
mp : IsMultiplyPreprimitive M α 1 → IsPreprimitive M α
⊢ IsMultiplyPreprimitive M α 1 ↔ IsPreprimitive M α
have mpr : IsPreprimitive M α → IsMultiplyPreprimitive M α 1
Tactic: constructor
-- 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 α
H1 : IsMultiplyPreprimitive M α 1
⊢ IsPreprimitive M α
have mp : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup.{u_1, u_2} M (α := α) ∅) ↥(ofFixingSubgroup M ∅)
Tactic: rw [← isPreprimitive_of_fixingSubgroup_empty_iff]
-- 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 α
h : IsPreprimitive M α
⊢ IsMultiplyPreprimitive M α 1
have mpr : IsMultiplyPretransitive M α 1 ∧
  ∀ {s : Set α} (hs : s.encard + 1 = (↑1 : ℕ∞)), IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
Tactic: rw [isMultiplyPreprimitive_iff]
-- 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 α
h : IsPreprimitive M α
⊢ IsMultiplyPretransitive M α 1 ∧
    ∀ {s : Set α} (hs : s.encard + 1 = (↑1 : ℕ∞)),
      IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
have mpr : IsMultiplyPretransitive M α 1
Tactic: constructor
-- 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 α
h : IsPreprimitive M α
mpr : IsMultiplyPretransitive M α 1
⊢ IsMultiplyPretransitive M α 1 ∧
    ∀ {s : Set α} (hs : s.encard + 1 = (↑1 : ℕ∞)),
      IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
have mpr₁ : ∀ {s : Set α} (hs : s.encard + 1 = (↑1 : ℕ∞)), IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
Tactic: constructor
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
⊢ IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
have inl : ∀ (h0 : n < 1), IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
Tactic: rcases Nat.lt_or_ge n 1 with h0 | h1
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
inl : ∀ (h0 : n < 1), IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
⊢ IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
have inr : ∀ (h1 : n ≥ 1), IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
Tactic: rcases Nat.lt_or_ge n 1 with h0 | h1
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
h0 : n < 1
⊢ IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
have h0₁ : n = 0
Tactic: rw [Nat.lt_one_iff] at h0
Cleared hypotheses: h0
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
h0 : n = 0
⊢ IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
have inl : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) 0
Tactic: rw [h0]
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
⊢ IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
have inr : IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n ∧
  ∀ {s : Set ↥(ofStabilizer M a)} (hs : s.encard + 1 = (↑n : ℕ∞)),
    IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(ofFixingSubgroup (↥(stabilizer M a)) s)
Tactic: rw [isMultiplyPreprimitive_iff]
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
⊢ IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n ∧
    ∀ {s : Set ↥(ofStabilizer M a)} (hs : s.encard + 1 = (↑n : ℕ∞)),
      IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(ofFixingSubgroup (↥(stabilizer M a)) s)
have inr : IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
Tactic: constructor
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
inr : IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
⊢ IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n ∧
    ∀ {s : Set ↥(ofStabilizer M a)} (hs : s.encard + 1 = (↑n : ℕ∞)),
      IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(ofFixingSubgroup (↥(stabilizer M a)) s)
have inr₁ : ∀ {s : Set ↥(ofStabilizer M a)} (hs : s.encard + 1 = (↑n : ℕ∞)),
  IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(ofFixingSubgroup (↥(stabilizer M a)) s)
Tactic: constructor
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
⊢ IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
have inr : IsMultiplyPretransitive M α n.succ
Tactic: rw [← ofStabilizer.isMultiplyPretransitive]
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
s : Set ↥(ofStabilizer M a)
hs : s.encard + 1 = (↑n : ℕ∞)
⊢ IsPreprimitive.{u_1, u_2}
    ↥(fixingSubgroup M
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
            s)))
    ↥(ofFixingSubgroup M
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
            s)))
have apply : (insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          s)).encard +
    1 =
  (↑n.succ : ℕ∞)
Tactic: apply IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup M 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 α
inst_2 : IsPretransitive M α
n : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
s : Set ↥(ofStabilizer M a)
hs : s.encard + 1 = (↑n : ℕ∞)
⊢ (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
            s)).encard +
      1 =
    (↑n.succ : ℕ∞)
have rw : a ∉
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
    s
Tactic: rw [Set.encard_insert_of_notMem, Subtype.coe_injective.encard_image, hs, Nat.cast_succ]
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
s : Set ↥(ofStabilizer M a)
hs : s.encard + 1 = (↑n : ℕ∞)
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(ofFixingSubgroup (↥(stabilizer M a)) s)
have this : IsPreprimitive.{u_1, u_2}
  ↥(fixingSubgroup M
      (insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          s)))
  ↥(ofFixingSubgroup M
      (insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          s)))
Tactic: have : IsPreprimitive ↥(fixingSubgroup M (insert a (Subtype.val '' s)))
      ↥(ofFixingSubgroup M (insert a (Subtype.val '' s))) := by
      apply IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup M n.succ
      rw [Set.encard_insert_of_notMem, Subtype.coe_injective.encard_image, hs, Nat.cast_succ]
      aesop
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
⊢ IsMultiplyPreprimitive M α n.succ ↔ IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
have mp : IsMultiplyPreprimitive M α n.succ → IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
Tactic: constructor
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
mp : IsMultiplyPreprimitive M α n.succ → IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
⊢ IsMultiplyPreprimitive M α n.succ ↔ IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
have mpr : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n → IsMultiplyPreprimitive M α n.succ
Tactic: constructor
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
⊢ IsMultiplyPreprimitive M α n.succ
have mpr : IsMultiplyPretransitive M α n.succ ∧
  ∀ {s : Set α} (hs : s.encard + 1 = (↑n.succ : ℕ∞)),
    IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
Tactic: rw [isMultiplyPreprimitive_iff]
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
⊢ IsMultiplyPretransitive M α n.succ ∧
    ∀ {s : Set α} (hs : s.encard + 1 = (↑n.succ : ℕ∞)),
      IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
have mpr : IsMultiplyPretransitive M α n.succ
Tactic: constructor
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
mpr : IsMultiplyPretransitive M α n.succ
⊢ IsMultiplyPretransitive M α n.succ ∧
    ∀ {s : Set α} (hs : s.encard + 1 = (↑n.succ : ℕ∞)),
      IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
have mpr₁ : ∀ {s : Set α} (hs : s.encard + 1 = (↑n.succ : ℕ∞)),
  IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
Tactic: constructor
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
⊢ ∃ (b : α), b ∈ s
have rw : s ≠ ∅
Tactic: rw [← Set.nonempty_def, Set.nonempty_iff_ne_empty]
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
h : s = ∅
⊢ False
have apply : n < 1
Tactic: apply not_lt.mpr hn
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
h : s = ∅
⊢ n < 1
have hs₁ : 0 = n
Tactic: rw [h, Set.encard_empty, zero_add, ← Nat.cast_one, Nat.cast_inj, Nat.succ_inj] at hs
Cleared hypotheses: hs, 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
have this : ∃ (b : α), b ∈ s
Tactic: have : ∃ b : α, b ∈ s := by
        rw [← Set.nonempty_def, Set.nonempty_iff_ne_empty]
        intro h
        apply not_lt.mpr hn
        rw [h, Set.encard_empty, zero_add, ← Nat.cast_one, Nat.cast_inj, Nat.succ_inj] at hs
        simp only [← hs, zero_lt_one]
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
this : ∃ (b : α), b ∈ s
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
have mpr : ∀ (b : α) (hb : b ∈ s), IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
Tactic: obtain ⟨b, hb⟩ := this
Cleared hypotheses: this
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
b : α
hb : b ∈ s
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
have mpr : ∀ (g : M) (hg : g • b = a), IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
Tactic: obtain ⟨g, hg : g • b = a⟩ := exists_smul_eq M b a
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
b : α
hb : b ∈ s
g : M
hg : g • b = a
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
have mpr : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M (g • s)) ↥(ofFixingSubgroup M (g • s))
Tactic: rw [isPreprimitive_ofFixingSubgroup_conj_iff (g := g)]
-- 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
b : α
hb : b ∈ s
g : M
hg : g • b = a
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M (g • s)) ↥(ofFixingSubgroup M (g • s))
have mpr : let s' := g • s;
∀ (hs' : s' = g • s), IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s') ↥(ofFixingSubgroup M s')
Tactic: set s' := g • s with 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 α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
⊢ s' =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
have h : ∀ (x : α),
  x ∈ s' ↔
    x ∈
      insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          t)
Tactic: ext x