awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
rw : HPow.hPow (α := ℕ) (β := ℕ) 2 ((Nat.factorization 12 : (a : ℕ) → ℕ) 2 : ℕ) = 4
⊢ Nat.card.{u_1} ↥(↑S : Subgroup ↥(alternatingGroup α)) = 4

Tactic:
rw [Sylow.card_eq_multiplicity, card_of_card_eq_four hα4]

Premises used: Sylow.card_eq_multiplicity, alternatingGroup.card_of_card_eq_four
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ 12 = HPow.hPow (α := ℕ) (β := ℕ) 2 2 * 3

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ 12 = HPow.hPow (α := ℕ) (β := ℕ) 2 2 * 3

Tactic:
have : 12 = 2 ^ 2 * 3 := by simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
this : 12 = HPow.hPow (α := ℕ) (β := ℕ) 2 2 * 3
⊢ (HPow.hPow (α := ℕ) (β := ℕ) 2 2).Coprime 3

Tactic:
decide
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
this : 12 = HPow.hPow (α := ℕ) (β := ℕ) 2 2 * 3
⊢ ¬Dvd.dvd (α := ℕ) 2 3

Tactic:
decide
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
this : 12 = HPow.hPow (α := ℕ) (β := ℕ) 2 2 * 3
rw : HPow.hPow (α := ℕ) 2 (HMul.hMul (α := ℕ) 2 1 + 0) = 4
⊢ HPow.hPow (α := ℕ) (β := ℕ) 2 ((Nat.factorization 12 : (a : ℕ) → ℕ) 2 : ℕ) = 4

Tactic:
rw [this, Nat.factorization_mul_apply_of_coprime (by decide), Nat.factorization_pow,
    Finsupp.coe_smul, Pi.smul_apply, smul_eq_mul, Nat.prime_two.factorization_self,
    Nat.factorization_eq_zero_of_not_dvd (by decide)]

Premises used: Nat.factorization_eq_zero_of_not_dvd, Nat.factorization_mul_apply_of_coprime, Nat.prime_two, Nat.Prime.factorization_self, Finsupp.coe_smul, Nat.factorization_pow, smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
this : 12 = HPow.hPow (α := ℕ) (β := ℕ) 2 2 * 3
⊢ HPow.hPow (α := ℕ) 2 (HMul.hMul (α := ℕ) 2 1 + 0) = 4

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ (↑S : Set ↥(alternatingGroup α)) = {1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}

Tactic:
Set.eq_of_subset_of_card_le (fun k hk ↦ ?_) ?_

Premises used: Set.eq_of_subset_of_card_le
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
refine_1 :
  ∀ (k : ↥(alternatingGroup α)) (hk : k ∈ (↑S : Set ↥(alternatingGroup α))),
    Membership.mem (γ := Set ↥(alternatingGroup α))
      ({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) k
refine_2 :
  Fintype.card.{u_1} (↑({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) : Type u_1) ≤
    Fintype.card.{u_1} (↑(↑S : Set ↥(alternatingGroup α)) : Type u_1)
⊢ (↑S : Set ↥(alternatingGroup α)) = {1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}

Tactic:
refine Set.eq_of_subset_of_card_le (fun k hk ↦ ?_) ?_

Premises used: Set.eq_of_subset_of_card_le
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : k ∈ (↑S : Set ↥(alternatingGroup α))
refine_1 :
  ∀ (n : ℕ)
    (hn :
      orderOf (Subtype.mk (p := fun (x : ↥(alternatingGroup α)) ↦ x ∈ (↑S : Subgroup ↥(alternatingGroup α))) k hk) =
        HPow.hPow (α := ℕ) 2 n),
    Membership.mem (γ := Set ↥(alternatingGroup α))
      ({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) k
⊢ Membership.mem (γ := Set ↥(alternatingGroup α)) ({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}})
    k

Tactic:
obtain ⟨n, hn⟩ := (IsPGroup.iff_orderOf.mp S.isPGroup') ⟨k, hk⟩

Premises used: Sylow.isPGroup', Subtype.mk, Iff.mp, IsPGroup.iff_orderOf
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : k ∈ (↑S : Set ↥(alternatingGroup α))
n : ℕ
hn :
  orderOf (Subtype.mk (p := fun (x : ↥(alternatingGroup α)) ↦ x ∈ (↑S : Subgroup ↥(alternatingGroup α))) k hk) =
    HPow.hPow (α := ℕ) 2 n
⊢ orderOf (↑k : Perm α) = HPow.hPow (α := ℕ) 2 n

Tactic:
simpa using hn
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : k ∈ (↑S : Set ↥(alternatingGroup α))
n : ℕ
hn :
  orderOf (Subtype.mk (p := fun (x : ↥(alternatingGroup α)) ↦ x ∈ (↑S : Subgroup ↥(alternatingGroup α))) k hk) =
    HPow.hPow (α := ℕ) 2 n
⊢ orderOf (↑k : Perm α) = HPow.hPow (α := ℕ) 2 n

Tactic:
replace hn : (orderOf (k : Perm α)) = 2 ^ n := by simpa using hn
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : k ∈ (↑S : Set ↥(alternatingGroup α))
n : ℕ
hn : orderOf (↑k : Perm α) = HPow.hPow (α := ℕ) 2 n
⊢ (↑k : Perm α).cycleType = ∅ ∨ (↑k : Perm α).cycleType = {2, 2}

Tactic:
mem_kleinFour_of_order_two_pow hα4 k.2 hn.dvd

Premises used: Eq.dvd, alternatingGroup.mem_kleinFour_of_order_two_pow, Subtype.property
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : k ∈ (↑S : Set ↥(alternatingGroup α))
n : ℕ
hn : orderOf (↑k : Perm α) = HPow.hPow (α := ℕ) 2 n
a :
  Membership.mem (γ := Set ↥(alternatingGroup α)) ({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}})
      k ↔
    (↑k : Perm α).cycleType = ∅ ∨ (↑k : Perm α).cycleType = {2, 2}
⊢ Membership.mem (γ := Set ↥(alternatingGroup α)) ({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}})
    k

Tactic:
convert! mem_kleinFour_of_order_two_pow hα4 k.2 hn.dvd

Premises used: Eq.dvd, alternatingGroup.mem_kleinFour_of_order_two_pow, Subtype.property
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
k : ↥(alternatingGroup α)
hk : k ∈ (↑S : Set ↥(alternatingGroup α))
n : ℕ
hn : orderOf (↑k : Perm α) = HPow.hPow (α := ℕ) 2 n
⊢ Membership.mem (γ := Set ↥(alternatingGroup α)) ({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}})
      k ↔
    (↑k : Perm α).cycleType = ∅ ∨ (↑k : Perm α).cycleType = {2, 2}

Tactic:
simp
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
refine_2 :
  Nat.card.{u_1} (↑({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) : Type u_1) ≤
    Nat.card.{u_1} (↑(↑S : Set ↥(alternatingGroup α)) : Type u_1)
⊢ Fintype.card.{u_1} (↑({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) : Type u_1) ≤
    Fintype.card.{u_1} (↑(↑S : Set ↥(alternatingGroup α)) : Type u_1)

Tactic:
simp_rw [← Nat.card_eq_fintype_card]

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Nat.card.{u_1} (↑({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) : Type u_1) ≤
    Nat.card.{u_1} (↑(↑S : Set ↥(alternatingGroup α)) : Type u_1)

Tactic:
(card_two_sylow_of_card_eq_four hα4 S).trans_ge ?_

Premises used: alternatingGroup.card_two_sylow_of_card_eq_four, Set.Mem, Eq.trans_ge
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
refine_2 : Nat.card.{u_1} (↑({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) : Type u_1) ≤ 4
⊢ Nat.card.{u_1} (↑({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) : Type u_1) ≤
    Nat.card.{u_1} (↑(↑S : Set ↥(alternatingGroup α)) : Type u_1)

Tactic:
refine (card_two_sylow_of_card_eq_four hα4 S).trans_ge ?_

Premises used: alternatingGroup.card_two_sylow_of_card_eq_four, Eq.trans_ge
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
refine_2 :
  Finset.card (α := ↥(alternatingGroup α)) ({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) ≤ 4
⊢ Nat.card.{u_1} (↑({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) : Type u_1) ≤ 4

Tactic:
rw [Nat.card_eq_card_toFinset, Set.toFinset_union, Set.toFinset_singleton, Set.toFinset_setOf]

Premises used: Set.toFinset_union, Set.toFinset_singleton, Nat.card_eq_card_toFinset, Set.toFinset_setOf
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
refine_2 :
  Finset.card (α := ↥(alternatingGroup α)) {1} +
      Finset.card.{u_1} (α := ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}} ≤
    4
⊢ Finset.card (α := ↥(alternatingGroup α)) ({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) ≤ 4

Tactic:
apply (Finset.card_union_le _ _).trans

Premises used: Finset.card_union_le, LE.le.trans
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
refine_2 :
  (1 +
      if
          (LE.le (α := ℕ) (Multiset.sum {2, 2}) 4 ∧ ∀ (a : ℕ), Membership.mem (γ := Multiset ℕ) {2, 2} a → 2 ≤ a) ∧
            Even (Multiset.sum {2, 2} + Multiset.card (α := ℕ) {2, 2}) then
        Nat.factorial 4 /
          ((HSub.hSub (α := ℕ) 4 (Multiset.sum {2, 2})).factorial *
            HMul.hMul (α := ℕ) (Multiset.prod {2, 2})
              (∏ n ∈ Multiset.toFinset {2, 2}, (Multiset.count n {2, 2}).factorial))
      else 0) ≤
    4
⊢ Finset.card (α := ↥(alternatingGroup α)) {1} +
      Finset.card.{u_1} (α := ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}} ≤
    4

Tactic:
rw [Finset.card_singleton, AlternatingGroup.card_of_cycleType, ← Nat.card_eq_fintype_card, hα4]

Premises used: AlternatingGroup.card_of_cycleType, Nat.card_eq_fintype_card, Finset.card_singleton
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ (1 +
      if
          (LE.le (α := ℕ) (Multiset.sum {2, 2}) 4 ∧ ∀ (a : ℕ), Membership.mem (γ := Multiset ℕ) {2, 2} a → 2 ≤ a) ∧
            Even (Multiset.sum {2, 2} + Multiset.card (α := ℕ) {2, 2}) then
        Nat.factorial 4 /
          ((HSub.hSub (α := ℕ) 4 (Multiset.sum {2, 2})).factorial *
            HMul.hMul (α := ℕ) (Multiset.prod {2, 2})
              (∏ n ∈ Multiset.toFinset {2, 2}, (Multiset.count n {2, 2}).factorial))
      else 0) ≤
    4

Tactic:
decide
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
refine_1 :
  ∀ (k : ↥(alternatingGroup α)) (hk : k ∈ (↑S : Set ↥(alternatingGroup α))),
    Membership.mem (γ := Set ↥(alternatingGroup α))
      ({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) k
refine_2 refine_2₁ :
  Fintype.card.{u_1} (↑({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) : Type u_1) ≤
    Fintype.card.{u_1} (↑(↑S : Set ↥(alternatingGroup α)) : Type u_1)
⊢ (↑S : Set ↥(alternatingGroup α)) = {1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}

Tactic:
classical
  refine Set.eq_of_subset_of_card_le (fun k hk ↦ ?_) ?_
  · -- inclusion S ⊆ {1} ∪ {g |  cycleType g = { 2, 2 }}
    obtain ⟨n, hn⟩ := (IsPGroup.iff_orderOf.mp S.isPGroup') ⟨k, hk⟩
    replace hn : (orderOf (k : Perm α)) = 2 ^ n := by simpa using hn
    convert! mem_kleinFour_of_order_two_pow hα4 k.2 hn.dvd
    simp
  · -- card (kleinFour α) ≤ card S
    simp_rw [← Nat.card_eq_fintype_card]
    refine (card_two_sylow_of_card_eq_four hα4 S).trans_ge ?_
    rw [Nat.card_eq_card_toFinset, Set.toFinset_union, Set.toFinset_singleton, Set.toFinset_setOf]
    apply (Finset.card_union_le _ _).trans
    rw [Finset.card_singleton, AlternatingGroup.card_of_cycleType, ← Nat.card_eq_fintype_card, hα4]
    decide

Premises used: Set.toFinset_union, alternatingGroup.card_two_sylow_of_card_eq_four, Eq.trans_ge, Finset.card_union_le, AlternatingGroup.card_of_cycleType, Set.toFinset_singleton, Set.eq_of_subset_of_card_le, Nat.card_eq_card_toFinset, LE.le.trans, Set.toFinset_setOf, Nat.card_eq_fintype_card, Finset.card_singleton
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
rw : (↑S : Subgroup ↥(alternatingGroup α)) = Subgroup.closure (↑S : Set ↥(alternatingGroup α))
rw₁ : Sylow 2 ↥(alternatingGroup α)
⊢ (↑S : Subgroup ↥(alternatingGroup α)) = kleinFour α

Tactic:
rw [kleinFour, ← Subgroup.closure_insert_one,
    ← Set.singleton_union, ← coe_two_sylow_of_card_eq_four hα4]

Premises used: Subgroup.closure_insert_one, Set.singleton_union, alternatingGroup.coe_two_sylow_of_card_eq_four, alternatingGroup.kleinFour
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ (↑S : Subgroup ↥(alternatingGroup α)) = Subgroup.closure (↑S : Set ↥(alternatingGroup α))

Tactic:
S.closure_eq.symm

Premises used: Sylow.toSubgroup, Subgroup.closure_eq, Eq.symm
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S T : Sylow 2 ↥(alternatingGroup α)
rw : (↑S : Subgroup ↥(alternatingGroup α)) = (↑T : Subgroup ↥(alternatingGroup α))
⊢ S = T

Tactic:
rw [Sylow.ext_iff]

Premises used: Sylow.ext_iff
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S T : Sylow 2 ↥(alternatingGroup α)
⊢ (↑S : Subgroup ↥(alternatingGroup α)) = (↑T : Subgroup ↥(alternatingGroup α))

Tactic:
simp [two_sylow_eq_kleinFour_of_card_eq_four hα4]

Premises used: alternatingGroup.two_sylow_eq_kleinFour_of_card_eq_four
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
obtain : ∀ (S : Sylow 2 ↥(alternatingGroup α)), Subgroup.Characteristic (G := ↥(alternatingGroup α)) (kleinFour α)
⊢ Subgroup.Characteristic (G := ↥(alternatingGroup α)) (kleinFour α)

Tactic:
obtain ⟨S : Sylow 2 (alternatingGroup α)⟩ := Sylow.nonempty (G := alternatingGroup α)

Premises used: Sylow, Membership.mem, Sylow.nonempty, Subtype, alternatingGroup, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subsingleton.{u_1 + 1} (Sylow 2 ↥(alternatingGroup α))

Tactic:
have _ := subsingleton_two_sylow hα4
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
h : Subsingleton.{u_1 + 1} (Sylow 2 ↥(alternatingGroup α))
rw : (↑S : Subgroup ↥(alternatingGroup α)).Characteristic
⊢ Subgroup.Characteristic (G := ↥(alternatingGroup α)) (kleinFour α)

Tactic:
rw [← two_sylow_eq_kleinFour_of_card_eq_four hα4 S]

Premises used: alternatingGroup.two_sylow_eq_kleinFour_of_card_eq_four
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
h : Subsingleton.{u_1 + 1} (Sylow 2 ↥(alternatingGroup α))
⊢ (↑S : Subgroup ↥(alternatingGroup α)).Characteristic

Tactic:
Sylow.characteristic_of_subsingleton _

Premises used: Sylow.characteristic_of_subsingleton
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
h : Subsingleton.{u_1 + 1} (Sylow 2 ↥(alternatingGroup α))
⊢ (↑S : Subgroup ↥(alternatingGroup α)).Characteristic

Tactic:
exact Sylow.characteristic_of_subsingleton _

Premises used: Sylow.characteristic_of_subsingleton
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
⊢ Subgroup.Characteristic (G := ↥(alternatingGroup α)) (kleinFour α)

Tactic:
have _ := characteristic_kleinFour hα4
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Characteristic (G := ↥(alternatingGroup α)) (kleinFour α)
⊢ Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)

Tactic:
apply Subgroup.normal_of_characteristic

Premises used: Subgroup.normal_of_characteristic
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
obtain : ∀ (S : Sylow 2 ↥(alternatingGroup α)), Nat.card.{u_1} ↥(kleinFour α) = 4
⊢ Nat.card.{u_1} ↥(kleinFour α) = 4

Tactic:
obtain ⟨S : Sylow 2 (alternatingGroup α)⟩ := Sylow.nonempty (G := alternatingGroup α)

Premises used: Sylow, Membership.mem, Sylow.nonempty, Subtype, alternatingGroup, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
rw : Nat.card.{u_1} ↥(↑S : Subgroup ↥(alternatingGroup α)) = 4
rw₁ rw₂ : Eq (α := ℕ) 4 4
⊢ Nat.card.{u_1} ↥(kleinFour α) = 4

Tactic:
rw [← two_sylow_eq_kleinFour_of_card_eq_four hα4 S, card_two_sylow_of_card_eq_four hα4 S]

Premises used: alternatingGroup.card_two_sylow_of_card_eq_four, alternatingGroup.two_sylow_eq_kleinFour_of_card_eq_four
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
obtain :
  ∀ (S : Sylow 2 ↥(alternatingGroup α)),
    (↑(kleinFour α) : Set ↥(alternatingGroup α)) = {1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}
⊢ (↑(kleinFour α) : Set ↥(alternatingGroup α)) = {1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}

Tactic:
obtain ⟨S : Sylow 2 (alternatingGroup α)⟩ := Sylow.nonempty (G := alternatingGroup α)

Premises used: Sylow, Membership.mem, Sylow.nonempty, Subtype, alternatingGroup, OfNat.ofNat
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
rw :
  (↑(↑S : Subgroup ↥(alternatingGroup α)) : Set ↥(alternatingGroup α)) =
    {1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}
⊢ (↑(kleinFour α) : Set ↥(alternatingGroup α)) = {1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}

Tactic:
rw [← two_sylow_eq_kleinFour_of_card_eq_four hα4 S]

Premises used: alternatingGroup.two_sylow_eq_kleinFour_of_card_eq_four
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ (↑(↑S : Subgroup ↥(alternatingGroup α)) : Set ↥(alternatingGroup α)) =
    {1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}

Tactic:
coe_two_sylow_of_card_eq_four hα4 S

Premises used: alternatingGroup.coe_two_sylow_of_card_eq_four
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ (↑(↑S : Subgroup ↥(alternatingGroup α)) : Set ↥(alternatingGroup α)) =
    {1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}

Tactic:
exact coe_two_sylow_of_card_eq_four hα4 S

Premises used: alternatingGroup.coe_two_sylow_of_card_eq_four
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
rw : ∀ (g : ↥(kleinFour α)), orderOf g ∣ 2
⊢ Monoid.exponent.{u_1} ↥(kleinFour α) ∣ 2

Tactic:
rw [Monoid.exponent_dvd]

Premises used: Monoid.exponent_dvd
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (kleinFour α)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
simp : HPow.hPow (β := ℕ) g 2 = 1
⊢ orderOf
      (Subtype.mk (p := fun (x : ↥(alternatingGroup α)) ↦
        Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (kleinFour α) x)
        (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg) hg') ∣
    2

Tactic:
simp only [Subgroup.orderOf_mk, orderOf_dvd_iff_pow_eq_one]

Premises used: Subgroup.orderOf_mk, orderOf_dvd_iff_pow_eq_one
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (kleinFour α)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
⊢ Membership.mem (γ := Set ↥(alternatingGroup α)) ({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}})
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)

Tactic:
rw [← SetLike.mem_coe, coe_kleinFour_of_card_eq_four hα4] at hg'

Premises used: alternatingGroup.coe_kleinFour_of_card_eq_four, SetLike.mem_coe
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Set ↥(alternatingGroup α)) ({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}})
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
inl :
  ∀
    (hg' :
      Membership.mem (γ := Set ↥(alternatingGroup α)) {1}
        (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)),
    HPow.hPow (β := ℕ) g 2 = 1
inr :
  ∀
    (hg' :
      Membership.mem (γ := Set ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}
        (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)),
    HPow.hPow (β := ℕ) g 2 = 1
⊢ HPow.hPow (β := ℕ) g 2 = 1

Tactic:
rcases hg' with hg' | hg'
-- Module: Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Set ↥(alternatingGroup α)) {1} (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
⊢ HPow.hPow (α := Perm α) (β := ℕ) 1 2 = 1

Tactic:
one_pow _

Premises used: one_pow