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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ Fintype.card (Sylow 2 ↥(alternatingGroup α)) = 1
Tactic:
rw [Fintype.card_eq_one_iff]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ ∃ x, ∀ (y : Sylow 2 ↥(alternatingGroup α)), y = x

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ ∃ x, ∀ (y : Sylow 2 ↥(alternatingGroup α)), y = x
Tactic:
obtain ⟨S : Sylow 2 (alternatingGroup α)⟩ := Sylow.nonempty (G := alternatingGroup α)
State after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ ∃ x, ∀ (y : Sylow 2 ↥(alternatingGroup α)), y = x

State before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ ∃ x, ∀ (y : Sylow 2 ↥(alternatingGroup α)), y = x
Tactic:
use S
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ ∀ (y : Sylow 2 ↥(alternatingGroup α)), y = S

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ ∀ (y : Sylow 2 ↥(alternatingGroup α)), y = S
Tactic:
intro T
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S T : Sylow 2 ↥(alternatingGroup α)
⊢ T = S

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S T : Sylow 2 ↥(alternatingGroup α)
⊢ T = S
Tactic:
rw [Sylow.ext_iff]
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S T : Sylow 2 ↥(alternatingGroup α)
⊢ ↑T = ↑S

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S T : Sylow 2 ↥(alternatingGroup α)
⊢ ↑T = ↑S
Tactic:
rw [← V4_is_unique_sylow α hα4 S]
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S T : Sylow 2 ↥(alternatingGroup α)
⊢ ↑T = V4 α

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S T : Sylow 2 ↥(alternatingGroup α)
⊢ ↑T = V4 α
Tactic:
rw [V4_is_unique_sylow α hα4 T]
State after:
no goals