internlm/Lean-Github huggingface dataset:
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}}
⊢ Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}
Tactic:
apply Or.intro_right
Proof 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}
Theorem: alternatingGroup.V4_is_unique_sylow
Proof 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
Proof state after:
no goals
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 α)
⊢ ↑S ≤ V4 α
Tactic:
intro k
Proof 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 α
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 α)
k : ↥(alternatingGroup α)
⊢ k ∈ ↑S → k ∈ V4 α
Tactic:
rw [← Subgroup.mem_carrier, A4_sylow_carrier α hα4 S, Set.mem_setOf_eq, or_imp]
Proof 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 α)
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 α)
k : ↥(alternatingGroup α)
⊢ (Equiv.Perm.cycleType ↑k = 0 → k ∈ V4 α) ∧ (Equiv.Perm.cycleType ↑k = {2, 2} → k ∈ V4 α)
Tactic:
constructor
Proof 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 α
Theorem: alternatingGroup.V4_is_unique_sylow
Proof 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
Proof 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 α
Theorem: alternatingGroup.V4_is_unique_sylow
Proof 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 _
Proof 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
Theorem: alternatingGroup.V4_is_unique_sylow
Proof 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]
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 α)
k : ↥(alternatingGroup α)
hk✝ : Equiv.Perm.cycleType ↑k = 0
hk : k = 1
⊢ k ∈ V4 α
Tactic:
rw [hk]
Proof 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 α
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 α)
k : ↥(alternatingGroup α)
hk✝ : Equiv.Perm.cycleType ↑k = 0
hk : k = 1
⊢ 1 ∈ V4 α
Tactic:
exact Subgroup.one_mem _
Proof state after:
no goals
Theorem: alternatingGroup.V4_is_unique_sylow
Proof 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
Proof 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 α
Theorem: alternatingGroup.V4_is_unique_sylow
Proof 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]
Proof 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}}
Theorem: alternatingGroup.V4_is_unique_sylow
Proof 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
Proof 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}}
Theorem: alternatingGroup.V4_is_unique_sylow
Proof 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]
Proof 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}
Theorem: alternatingGroup.V4_is_unique_sylow
Proof 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
Proof state after:
no goals
Theorem: alternatingGroup.A4_card_two_sylow_eq_one
Proof 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]
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ ∃ x, ∀ (y : Sylow 2 ↥(alternatingGroup α)), y = x
Theorem: alternatingGroup.A4_card_two_sylow_eq_one
Proof 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 α)
Proof 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
Theorem: alternatingGroup.A4_card_two_sylow_eq_one
Proof 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
Proof 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
Theorem: alternatingGroup.A4_card_two_sylow_eq_one
Proof 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
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S T : Sylow 2 ↥(alternatingGroup α)
⊢ T = S
Theorem: alternatingGroup.A4_card_two_sylow_eq_one
Proof 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]
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S T : Sylow 2 ↥(alternatingGroup α)
⊢ ↑T = ↑S
Theorem: alternatingGroup.A4_card_two_sylow_eq_one
Proof 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]
Proof state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S T : Sylow 2 ↥(alternatingGroup α)
⊢ ↑T = V4 α
Theorem: alternatingGroup.A4_card_two_sylow_eq_one
Proof 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]
Proof state after:
no goals
Theorem: alternatingGroup.V4_is_characteristic
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ Subgroup.Characteristic (V4 α)
Tactic:
obtain ⟨S : Sylow 2 (alternatingGroup α)⟩ := Sylow.nonempty (G := alternatingGroup α)
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.Characteristic (V4 α)
Theorem: alternatingGroup.V4_is_characteristic
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.Characteristic (V4 α)
Tactic:
rw [V4_is_unique_sylow α hα4 S]
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.Characteristic ↑S
Theorem: alternatingGroup.V4_is_characteristic
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.Characteristic ↑S
Tactic:
refine' Sylow.characteristic_of_normal S _
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.Normal ↑S
Theorem: alternatingGroup.V4_is_characteristic
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.Normal ↑S
Tactic:
rw [← Subgroup.normalizer_eq_top]
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.normalizer ↑S = ⊤
Theorem: alternatingGroup.V4_is_characteristic
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.normalizer ↑S = ⊤
Tactic:
rw [← Subgroup.index_eq_one]
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.index (Subgroup.normalizer ↑S) = 1
Theorem: alternatingGroup.V4_is_characteristic
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.index (Subgroup.normalizer ↑S) = 1
Tactic:
rw [← card_sylow_eq_index_normalizer]
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card (Sylow 2 ↥(alternatingGroup α)) = 1
Theorem: alternatingGroup.V4_is_characteristic
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card (Sylow 2 ↥(alternatingGroup α)) = 1
Tactic:
exact A4_card_two_sylow_eq_one α hα4
Proof state after:
no goals
Theorem: alternatingGroup.V4_is_normal
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ Subgroup.Normal (V4 α)
Tactic:
haveI := V4_is_characteristic α hα4
Proof state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Characteristic (V4 α)
⊢ Subgroup.Normal (V4 α)
Theorem: alternatingGroup.V4_is_normal
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
this : Subgroup.Characteristic (V4 α)
⊢ Subgroup.Normal (V4 α)
Tactic:
infer_instance
Proof state after:
no goals
Theorem: alternatingGroup.V4_card
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ Fintype.card ↥(V4 α) = 4
Tactic:
obtain ⟨S : Sylow 2 (alternatingGroup α)⟩ := Sylow.nonempty (G := alternatingGroup α)
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card ↥(V4 α) = 4
Theorem: alternatingGroup.V4_card
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card ↥(V4 α) = 4
Tactic:
rw [V4_is_unique_sylow α hα4 S]
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card ↥↑S = 4
Theorem: alternatingGroup.V4_card
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Fintype.card ↥↑S = 4
Tactic:
exact A4_sylow_card α hα4 S
Proof state after:
no goals
Theorem: alternatingGroup.isCommutative_of_exponent_two
Proof state before:
α : Type ?u.56052
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
hG2 : ∀ (g : G), g ^ 2 = 1
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
suffices ∀ g : G, g⁻¹ = g by
  constructor
  intro a b
  rw [← mul_inv_eq_iff_eq_mul, ← mul_inv_eq_one, this, this, ← hG2 (a * b), pow_two,
    mul_assoc (a * b) a b]
Proof state after:
α : Type ?u.56052
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
hG2 : ∀ (g : G), g ^ 2 = 1
⊢ ∀ (g : G), g⁻¹ = g
Theorem: alternatingGroup.isCommutative_of_exponent_two
Proof state before:
α : Type ?u.56052
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
hG2 : ∀ (g : G), g ^ 2 = 1
⊢ ∀ (g : G), g⁻¹ = g
Tactic:
intro g
Proof state after:
α : Type ?u.56052
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
hG2 : ∀ (g : G), g ^ 2 = 1
g : G
⊢ g⁻¹ = g
Theorem: alternatingGroup.isCommutative_of_exponent_two
Proof state before:
α : Type ?u.56052
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
hG2 : ∀ (g : G), g ^ 2 = 1
g : G
⊢ g⁻¹ = g
Tactic:
rw [← mul_eq_one_iff_inv_eq, ← hG2 g, pow_two]
Proof state after:
no goals
Theorem: alternatingGroup.isCommutative_of_exponent_two
Proof state before:
α : Type ?u.56052
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
hG2 : ∀ (g : G), g ^ 2 = 1
this : ∀ (g : G), g⁻¹ = g
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
constructor
Proof state after:
case comm
α : Type ?u.56052
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
hG2 : ∀ (g : G), g ^ 2 = 1
this : ∀ (g : G), g⁻¹ = g
⊢ ∀ (a b : G), a * b = b * a
Theorem: alternatingGroup.isCommutative_of_exponent_two
Proof state before:
case comm
α : Type ?u.56052
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
hG2 : ∀ (g : G), g ^ 2 = 1
this : ∀ (g : G), g⁻¹ = g
⊢ ∀ (a b : G), a * b = b * a
Tactic:
intro a b
Proof state after:
case comm
α : Type ?u.56052
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
hG2 : ∀ (g : G), g ^ 2 = 1
this : ∀ (g : G), g⁻¹ = g
a b : G
⊢ a * b = b * a
Theorem: alternatingGroup.isCommutative_of_exponent_two
Proof state before:
case comm
α : Type ?u.56052
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : Type u_1
inst✝ : Group G
hG2 : ∀ (g : G), g ^ 2 = 1
this : ∀ (g : G), g⁻¹ = g
a b : G
⊢ a * b = b * a
Tactic:
rw [← mul_inv_eq_iff_eq_mul, ← mul_inv_eq_one, this, this, ← hG2 (a * b), pow_two,
  mul_assoc (a * b) a b]
Proof state after:
no goals
Theorem: alternatingGroup.V4_carrier_eq
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ (V4 α).carrier = {g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}}
Tactic:
obtain ⟨S : Sylow 2 (alternatingGroup α)⟩ := Sylow.nonempty (G := alternatingGroup α)
Proof state after:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ (V4 α).carrier = {g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}}
Theorem: alternatingGroup.V4_carrier_eq
Proof state before:
case intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ (V4 α).carrier = {g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}}
Tactic:
rw [V4_is_unique_sylow α hα4 S]
Proof state after:
case intro
α : 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}}
Theorem: alternatingGroup.V4_carrier_eq
Proof state before:
case intro
α : 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:
rw [A4_sylow_carrier α hα4 S]
Proof state after:
no goals
Theorem: alternatingGroup.V4_is_of_exponent_two
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ ∀ (g : ↥(V4 α)), g ^ 2 = 1
Tactic:
rintro ⟨⟨g, hg⟩, hg'⟩
Proof state after:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ V4 α
⊢ { val := { val := g, property := hg }, property := hg' } ^ 2 = 1
Theorem: alternatingGroup.V4_is_of_exponent_two
Proof state before:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ V4 α
⊢ { val := { val := g, property := hg }, property := hg' } ^ 2 = 1
Tactic:
simp only [← Subtype.coe_inj, SubmonoidClass.mk_pow, Subgroup.coe_mk, Subgroup.coe_one]
Proof state after:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ V4 α
⊢ g ^ 2 = 1
Theorem: alternatingGroup.V4_is_of_exponent_two
Proof state before:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ V4 α
⊢ g ^ 2 = 1
Tactic:
rw [← Subgroup.mem_carrier, V4_carrier_eq α hα4] at hg'
Proof state after:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ {g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}}
⊢ g ^ 2 = 1
Theorem: alternatingGroup.V4_is_of_exponent_two
Proof state before:
case mk.mk
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : { val := g, property := hg } ∈ {g | Equiv.Perm.cycleType ↑g = 0 ∨ Equiv.Perm.cycleType ↑g = {2, 2}}
⊢ g ^ 2 = 1
Tactic:
cases' hg' with hg' hg'
Proof state after:
case mk.mk.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : Equiv.Perm.cycleType ↑{ val := g, property := hg } = 0
⊢ g ^ 2 = 1

case mk.mk.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : Equiv.Perm.cycleType ↑{ val := g, property := hg } = {2, 2}
⊢ g ^ 2 = 1
Theorem: alternatingGroup.V4_is_of_exponent_two
Proof state before:
case mk.mk.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : Equiv.Perm.cycleType ↑{ val := g, property := hg } = 0
⊢ g ^ 2 = 1
Tactic:
simp only [Subgroup.coe_mk, Equiv.Perm.cycleType_eq_zero] at hg'
Proof state after:
case mk.mk.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : g = 1
⊢ g ^ 2 = 1
Theorem: alternatingGroup.V4_is_of_exponent_two
Proof state before:
case mk.mk.inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : g = 1
⊢ g ^ 2 = 1
Tactic:
simp only [hg', one_pow]
Proof state after:
no goals
Theorem: alternatingGroup.V4_is_of_exponent_two
Proof state before:
case mk.mk.inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : Equiv.Perm.cycleType ↑{ val := g, property := hg } = {2, 2}
⊢ g ^ 2 = 1
Tactic:
convert pow_orderOf_eq_one g
Proof state after:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : Equiv.Perm.cycleType ↑{ val := g, property := hg } = {2, 2}
⊢ 2 = orderOf g
Theorem: alternatingGroup.V4_is_of_exponent_two
Proof state before:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : Equiv.Perm.cycleType ↑{ val := g, property := hg } = {2, 2}
⊢ 2 = orderOf g
Tactic:
simp only [Subgroup.coe_mk] at hg'
Proof state after:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : Equiv.Perm.cycleType g = {2, 2}
⊢ 2 = orderOf g
Theorem: alternatingGroup.V4_is_of_exponent_two
Proof state before:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : Equiv.Perm.cycleType g = {2, 2}
⊢ 2 = orderOf g
Tactic:
rw [← Equiv.Perm.lcm_cycleType, hg']
Proof state after:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : Equiv.Perm.cycleType g = {2, 2}
⊢ 2 = Multiset.lcm {2, 2}
Theorem: alternatingGroup.V4_is_of_exponent_two
Proof state before:
case h.e'_2.h.e'_6
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
g : Equiv.Perm α
hg : g ∈ alternatingGroup α
hg' : Equiv.Perm.cycleType g = {2, 2}
⊢ 2 = Multiset.lcm {2, 2}
Tactic:
norm_num
Proof state after:
no goals