awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : Finite α
this_2 : Fintype α
this_3 : IsPretransitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
⊢ IsPreprimitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
have obtain : ∀ (s : (↑(powersetCard α n) : Type u_2)), IsPreprimitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
Tactic: obtain ⟨s⟩ := this.to_nonempty
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : Finite α
this_2 : Fintype α
this_3 : IsPretransitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
⊢ IsPreprimitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
have rw : IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
Tactic: rw [← isCoatom_stabilizer_iff_preprimitive _ s]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : Finite α
this_2 : Fintype α
this_3 : IsPretransitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) s)
have rw : IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) (↑s : Set α))
Tactic: rw [stabilizer_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : Finite α
this_2 : Fintype α
this_3 : IsPretransitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) (↑s : Set α))
have hs_nonempty : (↑s : Set α).Nonempty
Tactic: apply isCoatom_stabilizer
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : Finite α
this_2 : Fintype α
this_3 : IsPretransitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
hs_nonempty : (↑s : Set α).Nonempty
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) (↑s : Set α))
have hsc_nonempty : (↑s : Set α)ᶜ.Nonempty
Tactic: apply isCoatom_stabilizer
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : Finite α
this_2 : Fintype α
this_3 : IsPretransitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
hs_nonempty : (↑s : Set α).Nonempty
hsc_nonempty : (↑s : Set α)ᶜ.Nonempty
⊢ IsCoatom (α := Subgroup (Perm α)) (stabilizer (Perm α) (↑s : Set α))
have hα₁ : Nat.card α ≠ 2 * (↑s : Set α).ncard
Tactic: apply isCoatom_stabilizer
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : Finite α
this_2 : Fintype α
this_3 : IsPretransitive.{u_2, u_2} (Perm α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
⊢ (↑s : Set α)ᶜ.Nonempty
have hsc_nonempty : ¬n = Nat.card α
Tactic: rw [nonempty_compl, ne_eq, eq_univ_iff_ncard, ncard_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
⊢ IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
have inr : ∀
  (this :
    ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α)
      (hn : 2 * n ≤ Nat.card α), IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2))
  (hn : Nat.card α < 2 * n), IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
Tactic: wlog! hn : 2 * n ≤ Nat.card α
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
inr :
  ∀
    (this :
      ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α)
        (hn : 2 * n ≤ Nat.card α), IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2))
    (hn : Nat.card α < 2 * n), IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
⊢ IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
have wlog! : ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α) (hn : 2 * n ≤ Nat.card α),
  IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
Tactic: wlog! hn : 2 * n ≤ Nat.card α
Cleared hypotheses: inst_1, hα
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
this :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α) (hn : 2 * n ≤ Nat.card α),
    IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
hn : Nat.card α < 2 * n
⊢ IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α (Nat.card α - n)) : Type u_2)
have apply : 2 * (Nat.card α - n) ≤ Nat.card α
Tactic: apply this hα
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (hypothesis)
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
this :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α) (hn : 2 * n ≤ Nat.card α),
    IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
hn : Nat.card α < 2 * n
⊢ IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
have this₁ : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α (Nat.card α - n)) : Type u_2)
Tactic: have : IsPretransitive (alternatingGroup α) (powersetCard α (Nat.card α - n)) := by
      apply this hα
      grind
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
this_1 :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α) (hn : 2 * n ≤ Nat.card α),
    IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
hn : Nat.card α < 2 * n
this : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α (Nat.card α - n)) : Type u_2)
⊢ IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
have pos : ∀ (hn' : n ≤ Nat.card α), IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
Tactic: by_cases hn' : n ≤ Nat.card α
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
this_1 :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α) (hn : 2 * n ≤ Nat.card α),
    IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
hn : Nat.card α < 2 * n
this : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α (Nat.card α - n)) : Type u_2)
pos : ∀ (hn' : n ≤ Nat.card α), IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
⊢ IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
have neg : ∀ (hn' : ¬n ≤ Nat.card α), IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
Tactic: by_cases hn' : n ≤ Nat.card α
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
this_1 :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α) (hn : 2 * n ≤ Nat.card α),
    IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
hn : Nat.card α < 2 * n
this : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α (Nat.card α - n)) : Type u_2)
hn' : n ≤ Nat.card α
⊢ IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
have apply : n + (Nat.card α - n) = Fintype.card α
Tactic: apply IsPretransitive.of_surjective_map
        (mulActionHom_compl_bijective (alternatingGroup α) α _).surjective this
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
this_1 :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α) (hn : 2 * n ≤ Nat.card α),
    IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
hn : Nat.card α < 2 * n
this : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α (Nat.card α - n)) : Type u_2)
hn' : ¬n ≤ Nat.card α
⊢ IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
have neg : Subsingleton.{u_2 + 1} (↑(powersetCard α n) : Type u_2)
Tactic: suffices Subsingleton (powersetCard α n) by infer_instance
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (hypothesis)
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
this_1 :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α) (hn : 2 * n ≤ Nat.card α),
    IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
hn : Nat.card α < 2 * n
this : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α (Nat.card α - n)) : Type u_2)
hn' : ¬n ≤ Nat.card α
⊢ Subsingleton.{u_2 + 1} (↑(powersetCard α n) : Type u_2)
have hn'₁ : Nat.card α < n
Tactic: rw [not_le] at hn'
Cleared hypotheses: hn'
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
n : ℕ
inst : DecidableEq α
inst_1 : Fintype α
hα : 3 ≤ Nat.card α
this_1 :
  ∀ {α : Type u_2} {n : ℕ} [inst : DecidableEq α] [inst_2 : Fintype α] (hα : 3 ≤ Nat.card α) (hn : 2 * n ≤ Nat.card α),
    IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
hn : Nat.card α < 2 * n
this : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α (Nat.card α - n)) : Type u_2)
hn' : Nat.card α < n
⊢ Subsingleton.{u_2 + 1} (↑(powersetCard α n) : Type u_2)
have neg : LE.le (α := ℕ) 0 1
Tactic: rw [← Finite.card_le_one_iff_subsingleton, powersetCard.card,
        Nat.choose_eq_zero_iff.mpr hn']
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α_1 : Type u_2
n_1 : ℕ
inst : DecidableEq α_1
α : Type u_2
n : ℕ
inst_1 : DecidableEq α
inst_2 : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
⊢ IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
have h : IsMultiplyPretransitive (↥(alternatingGroup α)) α n
Tactic: apply isPretransitive_of_isMultiplyPretransitive
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α_1 : Type u_2
n_1 : ℕ
inst : DecidableEq α_1
α : Type u_2
n : ℕ
inst_1 : DecidableEq α
inst_2 : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α n
have h : ∀ (hn : HMul.hMul (α := ℕ) 2 0 ≤ Nat.card α), IsMultiplyPretransitive (↥(alternatingGroup α)) α 0
Tactic: rcases eq_or_ne n 0 with rfl | hn0
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α_1 : Type u_2
n_1 : ℕ
inst : DecidableEq α_1
α : Type u_2
n : ℕ
inst_1 : DecidableEq α
inst_2 : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
h : ∀ (hn : HMul.hMul (α := ℕ) 2 0 ≤ Nat.card α), IsMultiplyPretransitive (↥(alternatingGroup α)) α 0
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α n
have h₁ : ∀ (hn0 : n ≠ 0), IsMultiplyPretransitive (↥(alternatingGroup α)) α n
Tactic: rcases eq_or_ne n 0 with rfl | hn0
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α_1 : Type u_2
n_1 : ℕ
inst : DecidableEq α_1
α : Type u_2
n : ℕ
inst_1 : DecidableEq α
inst_2 : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
hn0 : n ≠ 0
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α n
have h : ∀ (hn : HMul.hMul (α := ℕ) 2 1 ≤ Nat.card α) (hn0 : Ne (α := ℕ) 1 0),
  IsMultiplyPretransitive (↥(alternatingGroup α)) α 1
Tactic: rcases eq_or_ne n 1 with rfl | hn1
Cleared hypotheses: n, hn, hn0
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α_1 : Type u_2
n_1 : ℕ
inst : DecidableEq α_1
α : Type u_2
n : ℕ
inst_1 : DecidableEq α
inst_2 : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
hn0 : n ≠ 0
h :
  ∀ (hn : HMul.hMul (α := ℕ) 2 1 ≤ Nat.card α) (hn0 : Ne (α := ℕ) 1 0),
    IsMultiplyPretransitive (↥(alternatingGroup α)) α 1
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α n
have h₁ : ∀ (hn1 : n ≠ 1), IsMultiplyPretransitive (↥(alternatingGroup α)) α n
Tactic: rcases eq_or_ne n 1 with rfl | hn1
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α_1 : Type u_2
n : ℕ
inst : DecidableEq α_1
α : Type u_2
inst_1 : DecidableEq α
inst_2 : Fintype α
hα : 3 ≤ Nat.card α
hn : HMul.hMul (α := ℕ) 2 1 ≤ Nat.card α
hn0 : Ne (α := ℕ) 1 0
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α 1
have h : IsPretransitive (↥(alternatingGroup α)) α
Tactic: rw [is_one_pretransitive_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (hypothesis)
Goal:
α_1 : Type u_2
n_1 : ℕ
inst : DecidableEq α_1
α : Type u_2
n : ℕ
inst_1 : DecidableEq α
inst_2 : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α n
have this : IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
Tactic: have := alternatingGroup.isMultiplyPretransitive α
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α_1 : Type u_2
n_1 : ℕ
inst : DecidableEq α_1
α : Type u_2
n : ℕ
inst_1 : DecidableEq α
inst_2 : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
hn0 : n ≠ 0
hn1 : n ≠ 1
this : IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α n
have h : n ≤ Nat.card α - 2
Tactic: apply isMultiplyPretransitive_of_le (n := Nat.card α - 2)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α_1 : Type u_2
n_1 : ℕ
inst : DecidableEq α_1
α : Type u_2
n : ℕ
inst_1 : DecidableEq α
inst_2 : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
hn0 : n ≠ 0
hn1 : n ≠ 1
this : IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
h : n ≤ Nat.card α - 2
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α n
have h₁ : Nat.card α - 2 ≤ Nat.card α
Tactic: apply isMultiplyPretransitive_of_le (n := Nat.card α - 2)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
⊢ IsPreprimitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
have this : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
Tactic: have : IsPretransitive (alternatingGroup α) (powersetCard α n) :=
    isPretransitive_alternatingGroup (le_trans h_three_le hn.le)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (hypothesis)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
⊢ IsPreprimitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
have this₁ : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
Tactic: have : Nontrivial (powersetCard α n) := nontrivial (by positivity) (by simpa using hn)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
⊢ IsPreprimitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
have obtain : ∀ (s : (↑(powersetCard α n) : Type u_2)),
  IsPreprimitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
Tactic: obtain ⟨s⟩ := this.to_nonempty
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
⊢ IsPreprimitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
have rw : IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer ↥(alternatingGroup α) (↑s : Set α))
Tactic: rw [← isCoatom_stabilizer_iff_preprimitive _ s, stabilizer_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer ↥(alternatingGroup α) (↑s : Set α))
have h0 : (↑s : Set α).Nonempty
Tactic: apply alternatingGroup.isCoatom_stabilizer
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
h0 : (↑s : Set α).Nonempty
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer ↥(alternatingGroup α) (↑s : Set α))
have h1 : (↑s : Set α)ᶜ.Nonempty
Tactic: apply alternatingGroup.isCoatom_stabilizer
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
h0 : (↑s : Set α).Nonempty
h1 : (↑s : Set α)ᶜ.Nonempty
⊢ IsCoatom (α := Subgroup ↥(alternatingGroup α)) (stabilizer ↥(alternatingGroup α) (↑s : Set α))
have hs : Nat.card α ≠ 2 * (↑s : Set α).ncard
Tactic: apply alternatingGroup.isCoatom_stabilizer
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.Combination (goal)
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
n : ℕ
h_three_le : 3 ≤ n
hn : n < Nat.card α
hα : Nat.card α ≠ 2 * n
this_1 : IsPretransitive.{u_2, u_2} ↥(alternatingGroup α) (↑(powersetCard α n) : Type u_2)
this : Nontrivial.{u_2} (↑(powersetCard α n) : Type u_2)
s : (↑(powersetCard α n) : Type u_2)
⊢ (↑s : Set α).Nonempty
have h0 : 1 ≤ n
Tactic: rw [powersetCard.coe_nonempty_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (hypothesis)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
x_1 : ↥(fixingSubgroup M s)
x : α
c : M
hc : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) c
⊢ x ∈ sᶜ → Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) c hc • x ∈ sᶜ
have hc₁ : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) c⁻¹
Tactic: rw [← Subgroup.inv_mem_iff] at hc
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
x_1 : ↥(fixingSubgroup M s)
x : α
c : M
hc_1 : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) c
hc : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) c⁻¹
⊢ x ∈ sᶜ → Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) c hc_1 • x ∈ sᶜ
have simp : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) c hc_1 • x ∈ s → x ∈ s
Tactic: simp only [Set.mem_compl_iff, not_imp_not]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
x_1 : ↥(fixingSubgroup M s)
x : α
c : M
hc_1 : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) c
hc : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) c⁻¹
hcx : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) c hc_1 • x ∈ s
⊢ x ∈ s
have rwa : HSMul.hSMul.{u_1, u_2, u_2} (α := M) 1 x ∈ s
Tactic: rwa [← one_smul M x, ← inv_mul_cancel c, mul_smul, (mem_fixingSubgroup_iff M).mp hc (c • x) hcx]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
x_1 : ↥(fixingSubgroup M s)
x : α
c : M
hc_1 : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) c
hc : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) c⁻¹
hcx : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) c hc_1 • x ∈ s
rwa : HSMul.hSMul.{u_1, u_2, u_2} (α := M) 1 x ∈ s
⊢ x ∈ s
have rwa₁ : (c⁻¹ * c) • x ∈ s
Tactic: rwa [← one_smul M x, ← inv_mul_cancel c, mul_smul, (mem_fixingSubgroup_iff M).mp hc (c • x) hcx]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
x_1 : ↥(fixingSubgroup M s)
x : α
c : M
hc_1 : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) c
hc : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) c⁻¹
hcx : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) c hc_1 • x ∈ s
rwa : HSMul.hSMul.{u_1, u_2, u_2} (α := M) 1 x ∈ s
rwa₁ : (c⁻¹ * c) • x ∈ s
⊢ x ∈ s
have rwa₂ : c⁻¹ • c • x ∈ s
Tactic: rwa [← one_smul M x, ← inv_mul_cancel c, mul_smul, (mem_fixingSubgroup_iff M).mp hc (c • x) hcx]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup (goal)
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
x_1 : ↥(fixingSubgroup M s)
x : α
c : M
hc_1 : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) c
hc : Membership.mem (γ := Subgroup M) (fixingSubgroup M s) c⁻¹
hcx : Subtype.mk (p := fun (x : M) ↦ Membership.mem (γ := Subgroup M) (fixingSubgroup M s) x) c hc_1 • x ∈ s
rwa : HSMul.hSMul.{u_1, u_2, u_2} (α := M) 1 x ∈ s
rwa₁ : (c⁻¹ * c) • x ∈ s
rwa₂ : c⁻¹ • c • x ∈ s
⊢ x ∈ s
have rwa₃ : c • x ∈ s
Tactic: rwa [← one_smul M x, ← inv_mul_cancel c, mul_smul, (mem_fixingSubgroup_iff M).mp hc (c • x) hcx]