awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
⊢ Nat.card.{u_1} ↥(alternatingGroup α) = 12
have this : Nontrivial α
Tactic: have : Nontrivial α := by
    rw [← Finite.one_lt_card_iff_nontrivial, hα4]
    simp
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
this : Nontrivial α
⊢ Nat.card.{u_1} ↥(alternatingGroup α) = 12
have rw : Nat.factorial 4 / 2 = 12
Tactic: rw [nat_card_alternatingGroup, hα4]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Nat.card.{u_1} ↥(↑S : Subgroup ↥(alternatingGroup α)) = 4
have rw : HPow.hPow (α := ℕ) (β := ℕ) 2 ((Nat.factorization 12 : (a : ℕ) → ℕ) 2 : ℕ) = 4
Tactic: rw [Sylow.card_eq_multiplicity, card_of_card_eq_four hα4]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ HPow.hPow (α := ℕ) (β := ℕ) 2 ((Nat.factorization 12 : (a : ℕ) → ℕ) 2 : ℕ) = 4
have this : 12 = HPow.hPow (α := ℕ) (β := ℕ) 2 2 * 3
Tactic: have : 12 = 2 ^ 2 * 3 := by simp
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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 ((Nat.factorization 12 : (a : ℕ) → ℕ) 2 : ℕ) = 4
have rw : HPow.hPow (α := ℕ) 2 (HMul.hMul (α := ℕ) 2 1 + 0) = 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)]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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}}
have refine_1 : ∀ (k : ↥(alternatingGroup α)) (hk : k ∈ (↑S : Set ↥(alternatingGroup α))),
  Membership.mem (γ := Set ↥(alternatingGroup α)) ({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}})
    k
Tactic: refine Set.eq_of_subset_of_card_le (fun k hk ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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
⊢ (↑S : Set ↥(alternatingGroup α)) = {1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}
have 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)
Tactic: refine Set.eq_of_subset_of_card_le (fun k hk ↦ ?_) ?_
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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 α))
⊢ Membership.mem (γ := Set ↥(alternatingGroup α)) ({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}})
    k
have 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
Tactic: obtain ⟨n, hn⟩ := (IsPGroup.iff_orderOf.mp S.isPGroup') ⟨k, hk⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (hypothesis)
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
⊢ Membership.mem (γ := Set ↥(alternatingGroup α)) ({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}})
    k
have hn₁ : orderOf (↑k : Perm α) = HPow.hPow (α := ℕ) 2 n
Tactic: replace hn : (orderOf (k : Perm α)) = 2 ^ n := by simpa using hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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
have a : Membership.mem (γ := Set ↥(alternatingGroup α)) ({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}})
    k ↔
  (↑k : Perm α).cycleType = ∅ ∨ (↑k : Perm α).cycleType = {2, 2}
Tactic: convert! mem_kleinFour_of_order_two_pow hα4 k.2 hn.dvd
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ 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)
have 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)
Tactic: simp_rw [← Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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)
have refine_2 : Nat.card.{u_1} (↑({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) : Type u_1) ≤ 4
Tactic: refine (card_two_sylow_of_card_eq_four hα4 S).trans_ge ?_
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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) ≤ 4
have refine_2 : Finset.card (α := ↥(alternatingGroup α)) ({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) ≤ 4
Tactic: rw [Nat.card_eq_card_toFinset, Set.toFinset_union, Set.toFinset_singleton, Set.toFinset_setOf]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Finset.card (α := ↥(alternatingGroup α)) ({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}) ≤ 4
have refine_2 : Finset.card (α := ↥(alternatingGroup α)) {1} +
    Finset.card.{u_1} (α := ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}} ≤
  4
Tactic: apply (Finset.card_union_le _ _).trans
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Finset.card (α := ↥(alternatingGroup α)) {1} +
      Finset.card.{u_1} (α := ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}} ≤
    4
have 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
Tactic: rw [Finset.card_singleton, AlternatingGroup.card_of_cycleType, ← Nat.card_eq_fintype_card, hα4]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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}}
have refine_1 : ∀ (k : ↥(alternatingGroup α)) (hk : k ∈ (↑S : Set ↥(alternatingGroup α))),
  Membership.mem (γ := Set ↥(alternatingGroup α)) ({1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}})
    k
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
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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
⊢ (↑S : Set ↥(alternatingGroup α)) = {1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}
have 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)
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
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ (↑S : Subgroup ↥(alternatingGroup α)) = kleinFour α
have rw : (↑S : Subgroup ↥(alternatingGroup α)) = Subgroup.closure (↑S : Set ↥(alternatingGroup α))
Tactic: rw [kleinFour, ← Subgroup.closure_insert_one,
    ← Set.singleton_union, ← coe_two_sylow_of_card_eq_four hα4]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S T : Sylow 2 ↥(alternatingGroup α)
⊢ S = T
have rw : (↑S : Subgroup ↥(alternatingGroup α)) = (↑T : Subgroup ↥(alternatingGroup α))
Tactic: rw [Sylow.ext_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
⊢ Subgroup.Characteristic (G := ↥(alternatingGroup α)) (kleinFour α)
have obtain : ∀ (S : Sylow 2 ↥(alternatingGroup α)), Subgroup.Characteristic (G := ↥(alternatingGroup α)) (kleinFour α)
Tactic: obtain ⟨S : Sylow 2 (alternatingGroup α)⟩ := Sylow.nonempty (G := alternatingGroup α)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Subgroup.Characteristic (G := ↥(alternatingGroup α)) (kleinFour α)
have x : Subsingleton.{u_1 + 1} (Sylow 2 ↥(alternatingGroup α))
Tactic: have _ := subsingleton_two_sylow hα4
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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 α))
⊢ Subgroup.Characteristic (G := ↥(alternatingGroup α)) (kleinFour α)
have rw : (↑S : Subgroup ↥(alternatingGroup α)).Characteristic
Tactic: rw [← two_sylow_eq_kleinFour_of_card_eq_four hα4 S]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
⊢ Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
have x : Subgroup.Characteristic (G := ↥(alternatingGroup α)) (kleinFour α)
Tactic: have _ := characteristic_kleinFour hα4
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
⊢ Nat.card.{u_1} ↥(kleinFour α) = 4
have obtain : ∀ (S : Sylow 2 ↥(alternatingGroup α)), Nat.card.{u_1} ↥(kleinFour α) = 4
Tactic: obtain ⟨S : Sylow 2 (alternatingGroup α)⟩ := Sylow.nonempty (G := alternatingGroup α)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ Nat.card.{u_1} ↥(kleinFour α) = 4
have rw : Nat.card.{u_1} ↥(↑S : Subgroup ↥(alternatingGroup α)) = 4
Tactic: rw [← two_sylow_eq_kleinFour_of_card_eq_four hα4 S, card_two_sylow_of_card_eq_four hα4 S]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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
⊢ Nat.card.{u_1} ↥(kleinFour α) = 4
have rw₁ : Eq (α := ℕ) 4 4
Tactic: rw [← two_sylow_eq_kleinFour_of_card_eq_four hα4 S, card_two_sylow_of_card_eq_four hα4 S]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
⊢ (↑(kleinFour α) : Set ↥(alternatingGroup α)) = {1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}
have obtain : ∀ (S : Sylow 2 ↥(alternatingGroup α)),
  (↑(kleinFour α) : Set ↥(alternatingGroup α)) = {1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}
Tactic: obtain ⟨S : Sylow 2 (alternatingGroup α)⟩ := Sylow.nonempty (G := alternatingGroup α)
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
S : Sylow 2 ↥(alternatingGroup α)
⊢ (↑(kleinFour α) : Set ↥(alternatingGroup α)) = {1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}
have rw : (↑(↑S : Subgroup ↥(alternatingGroup α)) : Set ↥(alternatingGroup α)) =
  {1} ∪ {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}
Tactic: rw [← two_sylow_eq_kleinFour_of_card_eq_four hα4 S]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
⊢ Monoid.exponent.{u_1} ↥(kleinFour α) ∣ 2
have rw : ∀ (g : ↥(kleinFour α)), orderOf g ∣ 2
Tactic: rw [Monoid.exponent_dvd]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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)
⊢ 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
have simp : HPow.hPow (β := ℕ) g 2 = 1
Tactic: simp only [Subgroup.orderOf_mk, orderOf_dvd_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (hypothesis)
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)
⊢ HPow.hPow (β := ℕ) g 2 = 1
have 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'
Cleared hypotheses: hg'
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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)
⊢ HPow.hPow (β := ℕ) g 2 = 1
have inl : ∀
  (hg' :
    Membership.mem (γ := Set ↥(alternatingGroup α)) {1}
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)),
  HPow.hPow (β := ℕ) g 2 = 1
Tactic: rcases hg' with hg' | hg'
Cleared hypotheses: hg'
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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
⊢ HPow.hPow (β := ℕ) g 2 = 1
have 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
Tactic: rcases hg' with hg' | hg'
Cleared hypotheses: hg'
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
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 (β := ℕ) g 2 = 1
have h : g = 1
Tactic: convert! one_pow _
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
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
have h : 2 = orderOf g
Tactic: convert! pow_orderOf_eq_one g
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
g : Perm α
hg : g ∈ alternatingGroup α
hg' :
  Membership.mem (γ := Set ↥(alternatingGroup α)) {g : ↥(alternatingGroup α) | (↑g : Perm α).cycleType = {2, 2}}
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α) g hg)
⊢ 2 = orderOf g
have h : Eq (α := ℕ) 2 (Multiset.lcm {2, 2})
Tactic: rw [← Equiv.Perm.lcm_cycleType, hg']
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
⊢ Monoid.exponent.{u_1} ↥(kleinFour α) = 2
have this : Monoid.exponent.{u_1} ↥(kleinFour α) ∣ 2
Tactic: have : Monoid.exponent (kleinFour α) ∣ 2 := by
    rw [Monoid.exponent_dvd]
    rintro ⟨⟨g, hg⟩, hg'⟩
    simp only [Subgroup.orderOf_mk, orderOf_dvd_iff_pow_eq_one]
    rw [← SetLike.mem_coe, coe_kleinFour_of_card_eq_four hα4] at hg'
    rcases hg' with hg' | hg'
    · convert! one_pow _
      simpa only [Set.mem_singleton_iff, Subgroup.mk_eq_one] using hg'
    · convert! pow_orderOf_eq_one g
      rw [← Equiv.Perm.lcm_cycleType, hg']
      simp
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
this : Monoid.exponent.{u_1} ↥(kleinFour α) ∣ 2
⊢ Monoid.exponent.{u_1} ↥(kleinFour α) = 2
have this₁ : Monoid.exponent.{u_1} ↥(kleinFour α) = 1 ∨ Monoid.exponent.{u_1} ↥(kleinFour α) = 2
Tactic: rw [Nat.dvd_prime Nat.prime_two] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
this : Monoid.exponent.{u_1} ↥(kleinFour α) = 1 ∨ Monoid.exponent.{u_1} ↥(kleinFour α) = 2
⊢ Monoid.exponent.{u_1} ↥(kleinFour α) = 2
have apply : ¬Monoid.exponent.{u_1} ↥(kleinFour α) = 1
Tactic: apply Or.resolve_left this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
this : Monoid.exponent.{u_1} ↥(kleinFour α) = 1 ∨ Monoid.exponent.{u_1} ↥(kleinFour α) = 2
⊢ ¬Monoid.exponent.{u_1} ↥(kleinFour α) = 1
have rw : ¬LE.le (α := ℕ) 4 1
Tactic: rw [Monoid.exp_eq_one_iff, ← Finite.card_le_one_iff_subsingleton,
    kleinFour_card_of_card_eq_four hα4]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
⊢ Eq (α := Subgroup ↥(alternatingGroup α)) (kleinFour α) (commutator ↥(alternatingGroup α))
have x : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
Tactic: have _ : (kleinFour α).Normal := normal_kleinFour hα4
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (goal)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
⊢ Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
have rw : Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) *
    Nat.card.{u_1} ↥(kleinFour α) =
  3 * Nat.card.{u_1} ↥(kleinFour α)
Tactic: rw [← Nat.mul_left_inj (a := Nat.card (kleinFour α))]