α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
this : Nontrivial α
⊢ Nontrivial { x // x ∈ alternatingGroup α }
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
⊢ Nontrivial { x // x ∈ alternatingGroup α }
haveI := Fintype.one_lt_card_iff_nontrivial.1 (lt_trans (by decide) h3)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
this : Nontrivial α
⊢ 1 < card { x // x ∈ alternatingGroup α }
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
this : Nontrivial α
⊢ Nontrivial { x // x ∈ alternatingGroup α }
rw [← Fintype.one_lt_card_iff_nontrivial]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
this : Nontrivial α
⊢ 2 * 1 < 2 * card { x // x ∈ alternatingGroup α }
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
this : Nontrivial α
⊢ 1 < card { x // x ∈ alternatingGroup α }
refine' lt_of_mul_lt_mul_left _ (le_of_lt Nat.prime_two.pos)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
this : Nontrivial α
⊢ Nat.succ (2 * 1) ≤ Nat.factorial (card α)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
this : Nontrivial α
⊢ 2 * 1 < 2 * card { x // x ∈ alternatingGroup α }
rw [two_mul_card_alternatingGroup, card_perm, ← Nat.succ_le_iff]
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
this : Nontrivial α
⊢ Nat.succ (2 * 1) ≤ Nat.factorial (card α)
exact le_trans h3 (card α).self_le_factorial
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h3 : 3 ≤ card α
⊢ 1 < 2
decide