Theorem: alternatingGroup.A4_sylow_carrier (Jordan/V4.lean)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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