Theorem: alternatingGroup.Nat.Combination.isPreprimitive_of_alt (Jordan/AlternatingMaximal.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
h_one_le : 1 ≤ n
hn : n < Fintype.card α
hα : Fintype.card α ≠ 2 * n
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Tactic:
have hα' : 3 ≤ Fintype.card α := three_le h_one_le hn hα
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 α
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)

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 α
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Tactic:
have : Nontrivial α := by
  rw [← Fintype.one_lt_card_iff_nontrivial];
  exact lt_of_le_of_lt h_one_le hn
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 α
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)

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 α
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Tactic:
cases' Nat.eq_or_lt_of_le h_one_le with h_one h_one_lt
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 α n)

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
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)

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)
⊢ IsPreprimitive ↥(alternatingGroup α) ↑(Nat.Combination α n)
Tactic:
have : Nontrivial (n.Combination α) :=
  Nat.Combination_nontrivial α (lt_trans (Nat.lt_succ_self 0) h_one_lt) hn
State after:
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)

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 α)
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)

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
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)

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
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)

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]
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)

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]
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)

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]
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)

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 α)
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

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]
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 α

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
State after:
no goals

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]
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)

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
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 α)) α

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α'
State after:
no goals

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
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)

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)]
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))

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
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)

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 _)
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)

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
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 α

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
State after:
no goals

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]
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 α)

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]
State after:
no goals

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
State after:
no goals

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
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

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]
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

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]
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

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 ↔ _
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

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]
State after:
no goals

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]
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

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
State after:
no goals

State before:
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)ᶜ
Tactic:
simp only [← Finset.coe_compl, Finset.coe_nonempty, ← Finset.card_compl_lt_iff_nonempty,
  compl_compl, hs]
State after:
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
⊢ n < Fintype.card α

State before:
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
⊢ n < Fintype.card α
Tactic:
exact hn
State after:
no goals

State before:
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
Tactic:
simp only [Set.ncard_coe_Finset, hs]
State after:
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 * n

State before:
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 * n
Tactic:
exact hα
State after:
no goals