internlm/Lean-Github huggingface dataset:
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Tactic:
obtain ⟨sn⟩ := Nontrivial.to_nonempty (α := n.Combination α)
Proof state after:
case inr.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case inr.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Tactic:
let s := sn.val
Proof state after:
case inr.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case inr.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Tactic:
let hs : s.card = n := sn.prop
Proof state after:
case inr.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case inr.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Tactic:
rw [← maximal_stabilizer_iff_preprimitive (alternatingGroup α) sn]
Proof state after:
case inr.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) sn)
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case inr.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) sn)
Tactic:
have : stabilizer (alternatingGroup α) sn =
  stabilizer (alternatingGroup α) (s : Set α) := by
  ext g
  simp only [mem_stabilizer_iff]
  rw [← Subtype.coe_inj]
  change g • s = s ↔ _
  rw [← Finset.coe_smul_finset, ← Finset.coe_inj]
Proof state after:
case inr.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝¹ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (↥(alternatingGroup α)) sn = stabilizer ↥(alternatingGroup α) ↑s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) sn)
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case inr.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝¹ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (↥(alternatingGroup α)) sn = stabilizer ↥(alternatingGroup α) ↑s
⊢ Subgroup.IsMaximal (stabilizer (↥(alternatingGroup α)) sn)
Tactic:
rw [this]
Proof state after:
case inr.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝¹ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (↥(alternatingGroup α)) sn = stabilizer ↥(alternatingGroup α) ↑s
⊢ Subgroup.IsMaximal (stabilizer ↥(alternatingGroup α) ↑s)
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case inr.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝¹ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (↥(alternatingGroup α)) sn = stabilizer ↥(alternatingGroup α) ↑s
⊢ Subgroup.IsMaximal (stabilizer ↥(alternatingGroup α) ↑s)
Tactic:
apply Stabilizer.isMaximal (s : Set α)
Proof state after:
case inr.intro.h0
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝¹ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (↥(alternatingGroup α)) sn = stabilizer ↥(alternatingGroup α) ↑s
⊢ Set.Nonempty ↑s

case inr.intro.h1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝¹ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (↥(alternatingGroup α)) sn = stabilizer ↥(alternatingGroup α) ↑s
⊢ Set.Nonempty (↑s)ᶜ

case inr.intro.hs
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝¹ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (↥(alternatingGroup α)) sn = stabilizer ↥(alternatingGroup α) ↑s
⊢ Fintype.card α ≠ 2 * Set.ncard ↑s
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
⊢ Nontrivial α
Tactic:
rw [← Fintype.one_lt_card_iff_nontrivial]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
⊢ 1 < Fintype.card α
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
⊢ 1 < Fintype.card α
Tactic:
exact lt_of_le_of_lt h_one_le hn
Proof state after:
no goals
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this : Nontrivial α
h_one : 1 = n
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Tactic:
rw [← h_one]
Proof state after:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this : Nontrivial α
h_one : 1 = n
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α 1)
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this : Nontrivial α
h_one : 1 = n
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α 1)
Tactic:
apply isPreprimitive_of_surjective_map
  (Nat.bijective_toCombination_one_equivariant _ α).surjective
Proof state after:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this : Nontrivial α
h_one : 1 = n
⊢ IsPreprimitive (↥(alternatingGroup α)) α
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this : Nontrivial α
h_one : 1 = n
⊢ IsPreprimitive (↥(alternatingGroup α)) α
Tactic:
exact AlternatingGroup.isPreprimitive hα'
Proof state after:
no goals
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this : Nontrivial α
h_one_lt : 1 < n
⊢ IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Tactic:
have : Fintype.card α - n + n = Fintype.card α := by apply Nat.sub_add_cancel; exact le_of_lt hn
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
this : Fintype.card α - n + n = Fintype.card α
⊢ IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
this : Fintype.card α - n + n = Fintype.card α
⊢ IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Tactic:
rw [isPretransitive.of_bijective_map_iff Function.surjective_id
    (Nat.Combination_compl_bijective (alternatingGroup α) α this)]
Proof state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
this : Fintype.card α - n + n = Fintype.card α
⊢ IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α (Fintype.card α - n))
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
this : Fintype.card α - n + n = Fintype.card α
⊢ IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α (Fintype.card α - n))
Tactic:
apply Nat.Combination_isPretransitive_of_IsMultiplyPretransitive
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
this : Fintype.card α - n + n = Fintype.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - n)
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
this : Fintype.card α - n + n = Fintype.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - n)
Tactic:
apply isMultiplyPretransitive_of_higher (alternatingGroup α) α _
  (Nat.sub_le_sub_left h_one_lt _)
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
this : Fintype.card α - n + n = Fintype.card α
⊢ ↑(Fintype.card α - Nat.succ 1) ≤ PartENat.card α

α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
this : Fintype.card α - n + n = Fintype.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - Nat.succ 1)
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this : Nontrivial α
h_one_lt : 1 < n
⊢ Fintype.card α - n + n = Fintype.card α
Tactic:
apply Nat.sub_add_cancel
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this : Nontrivial α
h_one_lt : 1 < n
⊢ n ≤ Fintype.card α
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this : Nontrivial α
h_one_lt : 1 < n
⊢ n ≤ Fintype.card α
Tactic:
exact le_of_lt hn
Proof state after:
no goals
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
this : Fintype.card α - n + n = Fintype.card α
⊢ ↑(Fintype.card α - Nat.succ 1) ≤ PartENat.card α
Tactic:
rw [PartENat.card_eq_coe_fintype_card]
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
this : Fintype.card α - n + n = Fintype.card α
⊢ ↑(Fintype.card α - Nat.succ 1) ≤ ↑(Fintype.card α)
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
this : Fintype.card α - n + n = Fintype.card α
⊢ ↑(Fintype.card α - Nat.succ 1) ≤ ↑(Fintype.card α)
Tactic:
simp only [PartENat.coe_le_coe, tsub_le_self]
Proof state after:
no goals
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
this : Fintype.card α - n + n = Fintype.card α
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α (Fintype.card α - Nat.succ 1)
Tactic:
apply IsMultiplyPretransitive.alternatingGroup_of_sub_two
Proof state after:
no goals
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
⊢ stabilizer (↥(alternatingGroup α)) sn = stabilizer ↥(alternatingGroup α) ↑s
Tactic:
ext g
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
g : ↥(alternatingGroup α)
⊢ g ∈ stabilizer (↥(alternatingGroup α)) sn ↔ g ∈ stabilizer ↥(alternatingGroup α) ↑s
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
g : ↥(alternatingGroup α)
⊢ g ∈ stabilizer (↥(alternatingGroup α)) sn ↔ g ∈ stabilizer ↥(alternatingGroup α) ↑s
Tactic:
simp only [mem_stabilizer_iff]
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
g : ↥(alternatingGroup α)
⊢ g • sn = sn ↔ g • ↑s = ↑s
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
g : ↥(alternatingGroup α)
⊢ g • sn = sn ↔ g • ↑s = ↑s
Tactic:
rw [← Subtype.coe_inj]
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
g : ↥(alternatingGroup α)
⊢ ↑(g • sn) = ↑sn ↔ g • ↑s = ↑s
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
g : ↥(alternatingGroup α)
⊢ ↑(g • sn) = ↑sn ↔ g • ↑s = ↑s
Tactic:
change g • s = s ↔ _
Proof state after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
g : ↥(alternatingGroup α)
⊢ g • s = s ↔ g • ↑s = ↑s
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
g : ↥(alternatingGroup α)
⊢ g • s = s ↔ g • ↑s = ↑s
Tactic:
rw [← Finset.coe_smul_finset, ← Finset.coe_inj]
Proof state after:
no goals
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case inr.intro.h0
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝¹ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (↥(alternatingGroup α)) sn = stabilizer ↥(alternatingGroup α) ↑s
⊢ Set.Nonempty ↑s
Tactic:
simp only [Finset.coe_nonempty, ← Finset.card_pos, hs]
Proof state after:
case inr.intro.h0
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝¹ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (↥(alternatingGroup α)) sn = stabilizer ↥(alternatingGroup α) ↑s
⊢ 0 < n
Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt
Proof state before:
case inr.intro.h0
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
hα' : 3 ≤ Fintype.card α
this✝¹ : Nontrivial α
h_one_lt : 1 < n
ht : IsPretransitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
this✝ : Nontrivial ↑(Nat.Combination α n)
sn : ↑(Nat.Combination α n)
s : Finset α := ↑sn
hs : s.card = n := Subtype.prop sn
this : stabilizer (↥(alternatingGroup α)) sn = stabilizer ↥(alternatingGroup α) ↑s
⊢ 0 < n
Tactic:
apply lt_trans one_pos h_one_lt
Proof state after:
no goals