internlm/Lean-Github huggingface dataset:
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∉ Equiv.Perm.cycleType g
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hlcm : i = 2 ^ 2
hk1 : 1 < k
this : k = 2
⊢ 4 ∈ Equiv.Perm.cycleType g
Tactic:
norm_num at hlcm
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∉ Equiv.Perm.cycleType g
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hk1 : 1 < k
this : k = 2
hlcm : i = 4
⊢ 4 ∈ Equiv.Perm.cycleType g
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∉ Equiv.Perm.cycleType g
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hk1 : 1 < k
this : k = 2
hlcm : i = 4
⊢ 4 ∈ Equiv.Perm.cycleType g
Tactic:
rw [← hlcm]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∉ Equiv.Perm.cycleType g
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hk1 : 1 < k
this : k = 2
hlcm : i = 4
⊢ i ∈ Equiv.Perm.cycleType g
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∉ Equiv.Perm.cycleType g
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hk1 : 1 < k
this : k = 2
hlcm : i = 4
⊢ i ∈ Equiv.Perm.cycleType g
Tactic:
exact hi
Proof state after:
no goals
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case neg.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∉ Equiv.Perm.cycleType g
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hlcm : i = 2 ^ k
hk1 : 1 < k
⊢ k ≤ 2
Tactic:
rw [← Nat.pow_le_pow_iff_right (Nat.le_refl 2)]
Proof state after:
case neg.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∉ Equiv.Perm.cycleType g
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hlcm : i = 2 ^ k
hk1 : 1 < k
⊢ 2 ^ k ≤ 2 ^ 2
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case neg.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∉ Equiv.Perm.cycleType g
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hlcm : i = 2 ^ k
hk1 : 1 < k
⊢ 2 ^ k ≤ 2 ^ 2
Tactic:
norm_num
Proof state after:
case neg.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∉ Equiv.Perm.cycleType g
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hlcm : i = 2 ^ k
hk1 : 1 < k
⊢ 2 ^ k ≤ 4
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case neg.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∉ Equiv.Perm.cycleType g
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hlcm : i = 2 ^ k
hk1 : 1 < k
⊢ 2 ^ k ≤ 4
Tactic:
rw [← hα4, ← hlcm]
Proof state after:
case neg.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∉ Equiv.Perm.cycleType g
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hlcm : i = 2 ^ k
hk1 : 1 < k
⊢ i ≤ Fintype.card α
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case neg.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∉ Equiv.Perm.cycleType g
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hlcm : i = 2 ^ k
hk1 : 1 < k
⊢ i ≤ Fintype.card α
Tactic:
apply le_trans (Equiv.Perm.le_card_support_of_mem_cycleType hi)
Proof state after:
case neg.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∉ Equiv.Perm.cycleType g
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hlcm : i = 2 ^ k
hk1 : 1 < k
⊢ (Equiv.Perm.support g).card ≤ Fintype.card α
Theorem: alternatingGroup.mem_V4_of_order_two_pow
Proof state before:
case neg.intro.intro.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg0 : (-1) ^ (Multiset.sum (Equiv.Perm.cycleType g) + Multiset.card (Equiv.Perm.cycleType g)) = 1
n : ℕ
hg : Multiset.lcm (Equiv.Perm.cycleType g) ∣ 2 ^ n
hg4 : Multiset.sum (Equiv.Perm.cycleType g) ≤ 4
h4 : 4 ∉ Equiv.Perm.cycleType g
i : ℕ
hi : i ∈ Equiv.Perm.cycleType g
k : ℕ
hk : k ≤ n
hlcm : i = 2 ^ k
hk1 : 1 < k
⊢ (Equiv.Perm.support g).card ≤ Fintype.card α
Tactic:
apply Finset.card_le_univ
Proof state after:
no goals
Theorem: alternatingGroup.A4_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ Fintype.card ↥(alternatingGroup α) = 12
Tactic:
have : Nontrivial α := by
  rw [← Fintype.one_lt_card_iff_nontrivial, hα4]
  norm_num
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ Fintype.card ↥(alternatingGroup α) = 12
Theorem: alternatingGroup.A4_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ Fintype.card ↥(alternatingGroup α) = 12
Tactic:
apply mul_right_injective₀ (_: 2 ≠ 0)
Proof state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ (fun x => 2 * x) (Fintype.card ↥(alternatingGroup α)) = (fun x => 2 * x) 12

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ 2 ≠ 0
Theorem: alternatingGroup.A4_card
Proof state before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ (fun x => 2 * x) (Fintype.card ↥(alternatingGroup α)) = (fun x => 2 * x) 12

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ 2 ≠ 0
Tactic:
dsimp
Proof state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ 2 * Fintype.card ↥(alternatingGroup α) = 2 * 12

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ 2 ≠ 0
Theorem: alternatingGroup.A4_card
Proof state before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ 2 * Fintype.card ↥(alternatingGroup α) = 2 * 12

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ 2 ≠ 0
Tactic:
rw [two_mul_card_alternatingGroup, Fintype.card_perm, hα4]
Proof state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ Nat.factorial 4 = 2 * 12

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ 2 ≠ 0
Theorem: alternatingGroup.A4_card
Proof state before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ Nat.factorial 4 = 2 * 12

α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ 2 ≠ 0
Tactic:
all_goals
  norm_num
Proof state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ Nat.factorial 4 = 24
Theorem: alternatingGroup.A4_card
Proof state before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ Nat.factorial 4 = 24
Tactic:
rfl
Proof state after:
no goals
Theorem: alternatingGroup.A4_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ Nontrivial α
Tactic:
rw [← Fintype.one_lt_card_iff_nontrivial, hα4]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ 1 < 4
Theorem: alternatingGroup.A4_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ 1 < 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: alternatingGroup.A4_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Nontrivial α
⊢ 2 ≠ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: alternatingGroup.A4_sylow_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card ↥↑S = 4
Tactic:
rw [Sylow.card_eq_multiplicity, ← Nat.factors_count_eq, A4_card α hα4]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ 2 ^ List.count 2 (Nat.factors 12) = 4
Theorem: alternatingGroup.A4_sylow_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ 2 ^ List.count 2 (Nat.factors 12) = 4
Tactic:
rfl
Proof state after:
no goals
Theorem: alternatingGroup.A4_sylow_carrier
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ S.carrier = {g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}}
Tactic:
apply Set.eq_of_subset_of_card_le
Proof state after:
case hsub
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ S.carrier ⊆ {g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}}

case hcard
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card ↑{g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}} ≤ Fintype.card ↑S.carrier
Theorem: alternatingGroup.A4_sylow_carrier
Proof state before:
case hcard
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card ↑{g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}} ≤ Fintype.card ↑S.carrier
Tactic:
change _ ≤ Fintype.card S
Proof state after:
case hcard
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card ↑{g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}} ≤ Fintype.card ↥↑S
Theorem: alternatingGroup.A4_sylow_carrier
Proof state before:
case hcard
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card ↑{g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}} ≤ Fintype.card ↥↑S
Tactic:
rw [A4_sylow_card α hα4 S]
Proof state after:
case hcard
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card ↑{g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}} ≤ 4
Theorem: alternatingGroup.A4_sylow_carrier
Proof state before:
case hcard
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card ↑{g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}} ≤ 4
Tactic:
apply le_trans (Fintype.card_subtype_or _ _)
Proof state after:
case hcard
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card { x // Equiv.Perm.cycleType ↑x = 0 } + Fintype.card { x // Equiv.Perm.cycleType ↑x = {2, 2} } ≤ 4
Theorem: alternatingGroup.A4_sylow_carrier
Proof state before:
case hcard
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card { x // Equiv.Perm.cycleType ↑x = 0 } + Fintype.card { x // Equiv.Perm.cycleType ↑x = {2, 2} } ≤ 4
Tactic:
rw [Fintype.card_subtype]
Proof state after:
case hcard
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ (Finset.filter (fun x => Equiv.Perm.cycleType ↑x = 0) Finset.univ).card +
      Fintype.card { x // Equiv.Perm.cycleType ↑x = {2, 2} } ≤
    4
Theorem: alternatingGroup.A4_sylow_carrier
Proof state before:
case hcard
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ (Finset.filter (fun x => Equiv.Perm.cycleType ↑x = 0) Finset.univ).card +
      Fintype.card { x // Equiv.Perm.cycleType ↑x = {2, 2} } ≤
    4
Tactic:
rw [Fintype.card_subtype]
Proof state after:
case hcard
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ (Finset.filter (fun x => Equiv.Perm.cycleType ↑x = 0) Finset.univ).card +
      (Finset.filter (fun x => Equiv.Perm.cycleType ↑x = {2, 2}) Finset.univ).card ≤
    4
Theorem: alternatingGroup.A4_sylow_carrier
Proof state before:
case hcard
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ (Finset.filter (fun x => Equiv.Perm.cycleType ↑x = 0) Finset.univ).card +
      (Finset.filter (fun x => Equiv.Perm.cycleType ↑x = {2, 2}) Finset.univ).card ≤
    4
Tactic:
simp only [OnCycleFactors.AlternatingGroup.card_of_cycleType, hα4]
Proof state after:
case hcard
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ ((if (Multiset.sum 0 ≤ 4 ∧ ∀ a ∈ 0, 2 ≤ a) ∧ Even (Multiset.sum 0 + Multiset.card 0) then
        Nat.factorial 4 /
          (Nat.factorial (4 - Multiset.sum 0) *
            (Multiset.prod 0 *
              Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n 0)) (Multiset.dedup 0))))
      else 0) +
      if (Multiset.sum {2, 2} ≤ 4 ∧ ∀ a ∈ {2, 2}, 2 ≤ a) ∧ Even (Multiset.sum {2, 2} + Multiset.card {2, 2}) then
        Nat.factorial 4 /
          (Nat.factorial (4 - Multiset.sum {2, 2}) *
            (Multiset.prod {2, 2} *
              Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n {2, 2})) (Multiset.dedup {2, 2}))))
      else 0) ≤
    4
Theorem: alternatingGroup.A4_sylow_carrier
Proof state before:
case hcard
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ ((if (Multiset.sum 0 ≤ 4 ∧ ∀ a ∈ 0, 2 ≤ a) ∧ Even (Multiset.sum 0 + Multiset.card 0) then
        Nat.factorial 4 /
          (Nat.factorial (4 - Multiset.sum 0) *
            (Multiset.prod 0 *
              Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n 0)) (Multiset.dedup 0))))
      else 0) +
      if (Multiset.sum {2, 2} ≤ 4 ∧ ∀ a ∈ {2, 2}, 2 ≤ a) ∧ Even (Multiset.sum {2, 2} + Multiset.card {2, 2}) then
        Nat.factorial 4 /
          (Nat.factorial (4 - Multiset.sum {2, 2}) *
            (Multiset.prod {2, 2} *
              Multiset.prod (Multiset.map (fun n => Nat.factorial (Multiset.count n {2, 2})) (Multiset.dedup {2, 2}))))
      else 0) ≤
    4
Tactic:
norm_num
Proof state after:
case hcard
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ (Nat.factorial 4 / Nat.factorial 4 + if Even 6 then Nat.factorial 4 / 8 else 0) ≤ 4
Theorem: alternatingGroup.A4_sylow_carrier
Proof state before:
case hcard
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ (Nat.factorial 4 / Nat.factorial 4 + if Even 6 then Nat.factorial 4 / 8 else 0) ≤ 4
Tactic:
rfl
Proof state after:
no goals
Theorem: alternatingGroup.A4_sylow_carrier
Proof state before:
case hsub
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ S.carrier ⊆ {g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}}
Tactic:
intro k hk
Proof state after:
case hsub
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : k ∈ S.carrier
⊢ k ∈ {g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}}
Theorem: alternatingGroup.A4_sylow_carrier
Proof state before:
case hsub
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : k ∈ S.carrier
⊢ k ∈ {g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}}
Tactic:
simp only [Set.mem_setOf_eq]
Proof state after:
case hsub
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : k ∈ S.carrier
⊢ Equiv.Perm.cycleType ↑k = 0 ∨ Equiv.Perm.cycleType ↑k = {2, 2}
Theorem: alternatingGroup.A4_sylow_carrier
Proof state before:
case hsub
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : k ∈ S.carrier
⊢ Equiv.Perm.cycleType ↑k = 0 ∨ Equiv.Perm.cycleType ↑k = {2, 2}
Tactic:
obtain ⟨n, hn⟩ := (IsPGroup.iff_orderOf.mp S.isPGroup') ⟨k, hk⟩
Proof state after:
case hsub.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : k ∈ S.carrier
n : ℕ
hn : orderOf { val := k, property := hk } = 2 ^ n
⊢ Equiv.Perm.cycleType ↑k = 0 ∨ Equiv.Perm.cycleType ↑k = {2, 2}
Theorem: alternatingGroup.A4_sylow_carrier
Proof state before:
case hsub.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : k ∈ S.carrier
n : ℕ
hn : orderOf { val := k, property := hk } = 2 ^ n
⊢ Equiv.Perm.cycleType ↑k = 0 ∨ Equiv.Perm.cycleType ↑k = {2, 2}
Tactic:
apply mem_V4_of_order_two_pow α hα4 (↑k) k.prop n
Proof state after:
case hsub.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : k ∈ S.carrier
n : ℕ
hn : orderOf { val := k, property := hk } = 2 ^ n
⊢ orderOf ↑k ∣ 2 ^ n
Theorem: alternatingGroup.A4_sylow_carrier
Proof state before:
case hsub.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : k ∈ S.carrier
n : ℕ
hn : orderOf { val := k, property := hk } = 2 ^ n
⊢ orderOf ↑k ∣ 2 ^ n
Tactic:
rw [← orderOf_submonoid ⟨k, hk⟩, Subgroup.coe_mk] at hn
Proof state after:
case hsub.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : k ∈ S.carrier
n : ℕ
hn : orderOf k = 2 ^ n
⊢ orderOf ↑k ∣ 2 ^ n
Theorem: alternatingGroup.A4_sylow_carrier
Proof state before:
case hsub.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : k ∈ S.carrier
n : ℕ
hn : orderOf k = 2 ^ n
⊢ orderOf ↑k ∣ 2 ^ n
Tactic:
rw [orderOf_submonoid, hn]
Proof state after:
no goals
Theorem: alternatingGroup.V4_is_unique_sylow
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ V4 α = ↑S
Tactic:
apply le_antisymm
Proof state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ V4 α ≤ ↑S

case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ ↑S ≤ V4 α
Theorem: alternatingGroup.V4_is_unique_sylow
Proof state before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ V4 α ≤ ↑S
Tactic:
simp only [V4]
Proof state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.closure {g | Equiv.Perm.cycleType ↑g = {2, 2}} ≤ ↑S
Theorem: alternatingGroup.V4_is_unique_sylow
Proof state before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.closure {g | Equiv.Perm.cycleType ↑g = {2, 2}} ≤ ↑S
Tactic:
rw [Subgroup.closure_le]
Proof state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ {g | Equiv.Perm.cycleType ↑g = {2, 2}} ⊆ ↑↑S
Theorem: alternatingGroup.V4_is_unique_sylow
Proof state before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ {g | Equiv.Perm.cycleType ↑g = {2, 2}} ⊆ ↑↑S
Tactic:
intro g hg
Proof state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
g : ↥(alternatingGroup α)
hg : g ∈ {g | Equiv.Perm.cycleType ↑g = {2, 2}}
⊢ g ∈ ↑↑S
Theorem: alternatingGroup.V4_is_unique_sylow
Proof state before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
g : ↥(alternatingGroup α)
hg : g ∈ {g | Equiv.Perm.cycleType ↑g = {2, 2}}
⊢ g ∈ ↑↑S
Tactic:
rw [SetLike.mem_coe, ← Subgroup.mem_carrier, A4_sylow_carrier α hα4 S, Set.mem_setOf_eq]
Proof state after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
g : ↥(alternatingGroup α)
hg : g ∈ {g | Equiv.Perm.cycleType ↑g = {2, 2}}
⊢ Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}