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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ V4 α = ↑S
Tactic:
apply le_antisymm
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 α

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

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

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

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

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}}
⊢ Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}
Tactic:
apply Or.intro_right
State after:
case a.h
α : 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 = {2, 2}

State before:
case a.h
α : 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 = {2, 2}
Tactic:
exact hg
State after:
no goals

State before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ ↑S ≤ V4 α
Tactic:
intro k
State after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
⊢ k ∈ ↑S → k ∈ V4 α

State before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
⊢ k ∈ ↑S → k ∈ V4 α
Tactic:
rw [← Subgroup.mem_carrier, A4_sylow_carrier α hα4 S, Set.mem_setOf_eq, or_imp]
State after:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
⊢ (Equiv.Perm.cycleType ↑k = 0 → k ∈ V4 α) ∧ (Equiv.Perm.cycleType ↑k = {2, 2} → k ∈ V4 α)

State before:
case a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
⊢ (Equiv.Perm.cycleType ↑k = 0 → k ∈ V4 α) ∧ (Equiv.Perm.cycleType ↑k = {2, 2} → k ∈ V4 α)
Tactic:
constructor
State after:
case a.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
⊢ Equiv.Perm.cycleType ↑k = 0 → k ∈ V4 α

case a.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
⊢ Equiv.Perm.cycleType ↑k = {2, 2} → k ∈ V4 α

State before:
case a.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
⊢ Equiv.Perm.cycleType ↑k = 0 → k ∈ V4 α
Tactic:
intro hk
State after:
case a.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : Equiv.Perm.cycleType ↑k = 0
⊢ k ∈ V4 α

State before:
case a.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : Equiv.Perm.cycleType ↑k = 0
⊢ k ∈ V4 α
Tactic:
suffices hk : k = 1 by
  rw [hk]; exact Subgroup.one_mem _
State after:
case a.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : Equiv.Perm.cycleType ↑k = 0
⊢ k = 1

State before:
case a.left
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : Equiv.Perm.cycleType ↑k = 0
⊢ k = 1
Tactic:
rw [← Subtype.coe_inj, Subgroup.coe_one, ← Equiv.Perm.cycleType_eq_zero, hk]
State after:
no goals

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk✝ : Equiv.Perm.cycleType ↑k = 0
hk : k = 1
⊢ k ∈ V4 α
Tactic:
rw [hk]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk✝ : Equiv.Perm.cycleType ↑k = 0
hk : k = 1
⊢ 1 ∈ V4 α

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk✝ : Equiv.Perm.cycleType ↑k = 0
hk : k = 1
⊢ 1 ∈ V4 α
Tactic:
exact Subgroup.one_mem _
State after:
no goals

State before:
case a.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
⊢ Equiv.Perm.cycleType ↑k = {2, 2} → k ∈ V4 α
Tactic:
intro hk
State after:
case a.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : Equiv.Perm.cycleType ↑k = {2, 2}
⊢ k ∈ V4 α

State before:
case a.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : Equiv.Perm.cycleType ↑k = {2, 2}
⊢ k ∈ V4 α
Tactic:
simp only [V4]
State after:
case a.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : Equiv.Perm.cycleType ↑k = {2, 2}
⊢ k ∈ Subgroup.closure {g | Equiv.Perm.cycleType ↑g = {2, 2}}

State before:
case a.right
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : Equiv.Perm.cycleType ↑k = {2, 2}
⊢ k ∈ Subgroup.closure {g | Equiv.Perm.cycleType ↑g = {2, 2}}
Tactic:
apply Subgroup.subset_closure
State after:
case a.right.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : Equiv.Perm.cycleType ↑k = {2, 2}
⊢ k ∈ {g | Equiv.Perm.cycleType ↑g = {2, 2}}

State before:
case a.right.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : Equiv.Perm.cycleType ↑k = {2, 2}
⊢ k ∈ {g | Equiv.Perm.cycleType ↑g = {2, 2}}
Tactic:
simp only [Set.mem_setOf_eq]
State after:
case a.right.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : Equiv.Perm.cycleType ↑k = {2, 2}
⊢ Equiv.Perm.cycleType ↑k = {2, 2}

State before:
case a.right.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : Equiv.Perm.cycleType ↑k = {2, 2}
⊢ Equiv.Perm.cycleType ↑k = {2, 2}
Tactic:
exact hk
State after:
no goals