awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
hx :
  Membership.mem (α := Perm α)
    (MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
      (kerParam g))
    ((kerParam g :
          (a :
              Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α)))) →
            Perm α)
        (y, uv) :
      Perm α)
c : Perm α
hc : c ∈ g.cycleFactorsFinset
h :
  Membership.mem (γ := Finset ↥g.cycleFactorsFinset) univ
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)
k : ℤ
hk :
  (fun (x : ℤ) ↦ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α) ^ x) k =
    (↑(uv (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)) : Perm α)
⊢ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α).IsCycle
have h : ∀ (hc_1 : c.IsCycle ∧ ∀ a ∈ c.support, Eq (α := α) ((c : (a : α) → α) a : α) ((g : (a : α) → α) a : α)),
  Membership.mem (γ := Finset ↥g.cycleFactorsFinset) univ
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) →
    ∀ (k : ℤ)
      (hk :
        (fun (x : ℤ) ↦ (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α) ^ x) k =
          (↑(uv (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc)) : Perm α)),
      (↑(Subtype.mk (p := fun (x : Perm α) ↦ x ∈ g.cycleFactorsFinset) c hc) : Perm α).IsCycle
Tactic: rw [mem_cycleFactorsFinset_iff] at hc
Cleared hypotheses: h, k, hk
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
hx :
  Membership.mem (α := Perm α)
    (MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
      (kerParam g))
    ((kerParam g :
          (a :
              Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α)))) →
            Perm α)
        (y, uv) :
      Perm α)
⊢ Eq (α := ℤˣ) (1 : ℤˣ)
    (((sign : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) →* ℤˣ) :
          (a : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)) → ℤˣ)
        y :
      ℤˣ)
have h : y = 1
Tactic: suffices y = 1 by simp [this]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
h_odd : ∀ c ∈ g.cycleType, Odd c
h_fixed : Fintype.card α ≤ g.cycleType.sum + 1
h_count : ∀ (i : ℕ), Multiset.count i g.cycleType ≤ 1
y : Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1)
uv : (c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))
hx :
  Membership.mem (α := Perm α)
    (MonoidHom.range (G :=
      Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
        ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α))))
      (kerParam g))
    ((kerParam g :
          (a :
              Perm (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) ×
                ((c : ↥g.cycleFactorsFinset) → ↥(Subgroup.zpowers (↑c : Perm α)))) →
            Perm α)
        (y, uv) :
      Perm α)
⊢ y = 1
have this : Fintype.card.{u_1} (↑(Function.fixedPoints (⇑g : (a : α) → α)) : Type u_1) = Fintype.card α - g.cycleType.sum
Tactic: have := card_fixedPoints g
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g : Perm α).IsThreeCycle
⊢ Membership.mem (γ := Set ↥(alternatingGroup α)) (commutatorSet ↥(alternatingGroup α)) g
have hg₁ : IsConj g (HPow.hPow (β := ℕ) g 2)
Tactic: apply mem_commutatorSet_of_isConj_sq
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g : Perm α).IsThreeCycle
⊢ IsConj g (HPow.hPow (β := ℕ) g 2)
have hg₁ : (↑(HPow.hPow (β := ℕ) g 2) : Perm α).IsThreeCycle
Tactic: apply alternatingGroup.isThreeCycle_isConj h5 hg
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g : Perm α).IsThreeCycle
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) g
have rw : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.closure (commutatorSet ↥(alternatingGroup α))) g
Tactic: rw [commutator_eq_closure]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
g : ↥(alternatingGroup α)
hg : (↑g : Perm α).IsThreeCycle
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (Subgroup.closure (commutatorSet ↥(alternatingGroup α))) g
have a : Membership.mem (γ := Set ↥(alternatingGroup α)) (commutatorSet ↥(alternatingGroup α)) g
Tactic: apply Subgroup.subset_closure
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
⊢ _root_.commutator (Perm α) ≤ alternatingGroup α
have simp : ∀ (x x_1 x_2 : Perm α) (h : ⁅x_1, x_2⁆ = x), Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) x : ℤˣ) (1 : ℤˣ)
Tactic: simp only [commutator_eq_closure, closure_le, Set.subset_def, mem_commutatorSet_iff,
    SetLike.mem_coe, mem_alternatingGroup, forall_exists_index]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
this :
  Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (closure {b : ↥(alternatingGroup α) | (↑b : Perm α).IsThreeCycle})
    ⊤
⊢ Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (_root_.commutator ↥(alternatingGroup α)) ⊤
have rw : {b : ↥(alternatingGroup α) | (↑b : Perm α).IsThreeCycle} ⊆
  (↑(_root_.commutator ↥(alternatingGroup α)) : Set ↥(alternatingGroup α))
Tactic: rw [eq_top_iff, ← this, Subgroup.closure_le]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (_root_.commutator ↥(alternatingGroup α)) ⊤
have suffices : Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (closure {b : ↥(alternatingGroup α) | (↑b : Perm α).IsThreeCycle}) ⊤
Tactic: suffices closure {b : alternatingGroup α | (b : Perm α).IsThreeCycle} = ⊤ by
    rw [eq_top_iff, ← this, Subgroup.closure_le]
    intro b hb
    exact hb.mem_commutator_alternatingGroup h5
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ Eq.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (closure {b : ↥(alternatingGroup α) | (↑b : Perm α).IsThreeCycle})
    ⊤
have rw : Eq.{u_1 + 1} (α := Subgroup ↥(closure {σ : Perm α | σ.IsThreeCycle}))
  (closure {b : ↥(closure {σ : Perm α | σ.IsThreeCycle}) | (↑b : Perm α).IsThreeCycle}) ⊤
Tactic: rw [← closure_three_cycles_eq_alternating]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ ⁅alternatingGroup α, alternatingGroup α⁆ = alternatingGroup α
have rw : Subgroup.map (alternatingGroup α).subtype (_root_.commutator ↥(alternatingGroup α)) = alternatingGroup α
Tactic: rw [← Subgroup.map_subtype_commutator, commutator_alternatingGroup_eq_top h5,
    ← MonoidHom.range_eq_map, Subgroup.range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
rw : Subgroup.map (alternatingGroup α).subtype (_root_.commutator ↥(alternatingGroup α)) = alternatingGroup α
⊢ ⁅alternatingGroup α, alternatingGroup α⁆ = alternatingGroup α
have rw₁ : Subgroup.map (alternatingGroup α).subtype ⊤ = alternatingGroup α
Tactic: rw [← Subgroup.map_subtype_commutator, commutator_alternatingGroup_eq_top h5,
    ← MonoidHom.range_eq_map, Subgroup.range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
rw : Subgroup.map (alternatingGroup α).subtype (_root_.commutator ↥(alternatingGroup α)) = alternatingGroup α
rw₁ : Subgroup.map (alternatingGroup α).subtype ⊤ = alternatingGroup α
⊢ ⁅alternatingGroup α, alternatingGroup α⁆ = alternatingGroup α
have rw₂ : (alternatingGroup α).subtype.range = alternatingGroup α
Tactic: rw [← Subgroup.map_subtype_commutator, commutator_alternatingGroup_eq_top h5,
    ← MonoidHom.range_eq_map, Subgroup.range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
rw : Subgroup.map (alternatingGroup α).subtype (_root_.commutator ↥(alternatingGroup α)) = alternatingGroup α
rw₁ : Subgroup.map (alternatingGroup α).subtype ⊤ = alternatingGroup α
rw₂ : (alternatingGroup α).subtype.range = alternatingGroup α
⊢ ⁅alternatingGroup α, alternatingGroup α⁆ = alternatingGroup α
have rw₃ : alternatingGroup α = alternatingGroup α
Tactic: rw [← Subgroup.map_subtype_commutator, commutator_alternatingGroup_eq_top h5,
    ← MonoidHom.range_eq_map, Subgroup.range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ _root_.commutator (Perm α) = alternatingGroup α
have apply : alternatingGroup α ≤ _root_.commutator (Perm α)
Tactic: apply le_antisymm alternatingGroup.commutator_perm_le
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ alternatingGroup α ≤ _root_.commutator (Perm α)
have rw : ⁅alternatingGroup α, alternatingGroup α⁆ ≤ _root_.commutator (Perm α)
Tactic: rw [← commutator_alternatingGroup_eq_self h5]
-- 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 α
hg0 : g ∈ alternatingGroup α
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}
have rw : ∀ (hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1) {n : ℕ}
  (hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n), g.cycleType = ∅ ∨ g.cycleType = {2, 2}
Tactic: rw [mem_alternatingGroup, sign_of_cycleType] at hg0
Cleared hypotheses: hg0, n, 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 α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
⊢ g.cycleType.sum ≤ 4
have rw : g.support.card ≤ Fintype.card α
Tactic: rw [sum_cycleType, ← hα4, Nat.card_eq_fintype_card]
-- 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 α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}
have h1 : g.cycleType.sum ≤ 4
Tactic: have h1 : g.cycleType.sum ≤ 4 := by
    rw [sum_cycleType, ← hα4, Nat.card_eq_fintype_card]
    exact g.support.card_le_univ
-- 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 α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : k ∈ g.cycleType
⊢ k = 2
have hk4 : k ≤ 4
Tactic: have hk4 := (Multiset.le_sum_of_mem hk).trans h1
-- 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 α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : k ∈ g.cycleType
hk4 : k ≤ 4
⊢ k = 2
have hk1 : 1 < k
Tactic: have hk1 := one_lt_of_mem_cycleType 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
g : Perm α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : k ∈ g.cycleType
hk4 : k ≤ 4
hk1 : 1 < k
⊢ k = 2
have 2 : ∀ (hk : 2 ∈ g.cycleType) (hk4 : LE.le (α := ℕ) 2 4) (hk1 : LT.lt (α := ℕ) 1 2), Eq (α := ℕ) 2 2
Tactic: interval_cases k
Cleared hypotheses: hk, hk4, hk1
-- 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 α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : k ∈ g.cycleType
hk4 : k ≤ 4
hk1 : 1 < k
2 : ∀ (hk : 2 ∈ g.cycleType) (hk4 : LE.le (α := ℕ) 2 4) (hk1 : LT.lt (α := ℕ) 1 2), Eq (α := ℕ) 2 2
⊢ k = 2
have 3 : ∀ (hk : 3 ∈ g.cycleType) (hk4 : LE.le (α := ℕ) 3 4) (hk1 : LT.lt (α := ℕ) 1 3), Eq (α := ℕ) 3 2
Tactic: interval_cases k
Cleared hypotheses: hk, hk4, hk1
-- 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 α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : k ∈ g.cycleType
hk4 : k ≤ 4
hk1 : 1 < k
2 : ∀ (hk : 2 ∈ g.cycleType) (hk4 : LE.le (α := ℕ) 2 4) (hk1 : LT.lt (α := ℕ) 1 2), Eq (α := ℕ) 2 2
3 : ∀ (hk : 3 ∈ g.cycleType) (hk4 : LE.le (α := ℕ) 3 4) (hk1 : LT.lt (α := ℕ) 1 3), Eq (α := ℕ) 3 2
⊢ k = 2
have 4 : ∀ (hk : 4 ∈ g.cycleType) (hk4 : LE.le (α := ℕ) 4 4) (hk1 : LT.lt (α := ℕ) 1 4), Eq (α := ℕ) 4 2
Tactic: interval_cases k
Cleared hypotheses: hk, hk4, hk1
-- 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 α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 3 ∈ g.cycleType
hk4 : LE.le (α := ℕ) 3 4
hk1 : LT.lt (α := ℕ) 1 3
⊢ Eq (α := ℕ) 3 2
have 3 : ∀ (hg : ∀ b ∈ g.cycleType, b ∣ HPow.hPow (α := ℕ) 2 n) (h1 : g.cycleType.sum ≤ 4) (k : ℕ) (hk : 3 ∈ g.cycleType)
  (hk4 : LE.le (α := ℕ) 3 4) (hk1 : LT.lt (α := ℕ) 1 3), Eq (α := ℕ) 3 2
Tactic: rw [← lcm_cycleType, Multiset.lcm_dvd] at hg
Cleared hypotheses: hg, h1, k, hk, hk4, hk1
-- 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 α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : LE.le (α := ℕ) 4 4
hk1 : LT.lt (α := ℕ) 1 4
⊢ Eq (α := ℕ) 4 2
have 4 : ∀ (hg0 : Ne (α := ℕ) 4 2), HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) ≠ 1
Tactic: contrapose! hg0
Cleared hypotheses: hg0
-- 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 α
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : LE.le (α := ℕ) 4 4
hk1 : LT.lt (α := ℕ) 1 4
hg0 : Ne (α := ℕ) 4 2
⊢ HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) ≠ 1
have 4 : ∀ (t : Multiset ℕ) (ht : g.cycleType = 4 ::ₘ t), HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) ≠ 1
Tactic: obtain ⟨t, ht⟩ := Multiset.exists_cons_of_mem 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
g : Perm α
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : LE.le (α := ℕ) 4 4
hk1 : LT.lt (α := ℕ) 1 4
hg0 : Ne (α := ℕ) 4 2
t : Multiset ℕ
ht : g.cycleType = 4 ::ₘ t
⊢ HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) ≠ 1
have h1₁ : t = Multiset.replicate t.card 0
Tactic: rw [ht, Multiset.sum_cons, add_le_iff_nonpos_right, le_zero_iff,
        Multiset.sum_eq_zero_iff, ← Multiset.eq_replicate_card] at h1
Cleared hypotheses: h1, ht
-- 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 α
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : LE.le (α := ℕ) 4 4
hk1 : LT.lt (α := ℕ) 1 4
hg0 : Ne (α := ℕ) 4 2
t : Multiset ℕ
h1 : t = Multiset.replicate t.card 0
ht : g.cycleType = 4 ::ₘ t
⊢ HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) ≠ 1
have h : 0 ∉ g.cycleType
Tactic: have h : 0 ∉ g.cycleType := Nat.not_succ_lt_self ∘ one_lt_of_mem_cycleType
-- 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 α
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
k : ℕ
hk : 4 ∈ g.cycleType
hk4 : LE.le (α := ℕ) 4 4
hk1 : LT.lt (α := ℕ) 1 4
hg0 : Ne (α := ℕ) 4 2
t : Multiset ℕ
h1 : t = Multiset.replicate t.card 0
ht : g.cycleType = 4 ::ₘ t
h : 0 ∉ g.cycleType
⊢ HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) ≠ 1
have h₁ : t = 0
Tactic: replace h : t = 0 := by simpa [h1 ▸ ht, Multiset.mem_replicate] using h
Cleared hypotheses: h
-- 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 α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}
have h2 : ∀ k ∈ g.cycleType, k = 2
Tactic: have h2 : ∀ k ∈ g.cycleType, k = 2 := by
    intro k hk
    have hk4 := (Multiset.le_sum_of_mem hk).trans h1
    have hk1 := one_lt_of_mem_cycleType hk
    interval_cases k
    · rfl
    · rw [← lcm_cycleType, Multiset.lcm_dvd] at hg
      exact Nat.prime_eq_prime_of_dvd_pow Nat.prime_three Nat.prime_two (hg 3 hk)
    · contrapose! hg0
      obtain ⟨t, ht⟩ := Multiset.exists_cons_of_mem hk
      rw [ht, Multiset.sum_cons, add_le_iff_nonpos_right, le_zero_iff,
        Multiset.sum_eq_zero_iff, ← Multiset.eq_replicate_card] at h1
      have h : 0 ∉ g.cycleType := Nat.not_succ_lt_self ∘ one_lt_of_mem_cycleType
      replace h : t = 0 := by simpa [h1 ▸ ht, Multiset.mem_replicate] using h
      simp [ht, h, Units.ext_iff]
-- 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 α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
h2 : ∀ k ∈ g.cycleType, k = 2
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}
have h2₁ : g.cycleType = Multiset.replicate g.cycleType.card 2
Tactic: rw [← Multiset.eq_replicate_card] at h2
Cleared hypotheses: h2
-- 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 α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.sum ≤ 4
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}
have h1₁ : g.cycleType.card ≤ 4 / 2
Tactic: rw [h2, Multiset.sum_replicate, smul_eq_mul, ← Nat.le_div_iff_mul_le two_pos] at h1
Cleared hypotheses: h1, h2
-- 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 α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.card ≤ 4 / 2
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}
have 0 : ∀ (hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + 0) = 1) (h1 : 0 ≤ 4 / 2)
  (h2 : g.cycleType = Multiset.replicate 0 2), g.cycleType = ∅ ∨ g.cycleType = {2, 2}
Tactic: interval_cases g.cycleType.card
Cleared hypotheses: hg0, h1, h2
-- 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 α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.card ≤ 4 / 2
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
0 :
  ∀ (hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + 0) = 1) (h1 : 0 ≤ 4 / 2)
    (h2 : g.cycleType = Multiset.replicate 0 2), g.cycleType = ∅ ∨ g.cycleType = {2, 2}
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}
have 1 : ∀ (hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + 1) = 1) (h1 : 1 ≤ 4 / 2)
  (h2 : g.cycleType = Multiset.replicate 1 2), g.cycleType = ∅ ∨ g.cycleType = {2, 2}
Tactic: interval_cases g.cycleType.card
Cleared hypotheses: hg0, h1, h2
-- 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 α
hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + g.cycleType.card) = 1
n : ℕ
hg : orderOf g ∣ HPow.hPow (α := ℕ) 2 n
h1 : g.cycleType.card ≤ 4 / 2
h2 : g.cycleType = Multiset.replicate g.cycleType.card 2
0 :
  ∀ (hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + 0) = 1) (h1 : 0 ≤ 4 / 2)
    (h2 : g.cycleType = Multiset.replicate 0 2), g.cycleType = ∅ ∨ g.cycleType = {2, 2}
1 :
  ∀ (hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + 1) = 1) (h1 : 1 ≤ 4 / 2)
    (h2 : g.cycleType = Multiset.replicate 1 2), g.cycleType = ∅ ∨ g.cycleType = {2, 2}
⊢ g.cycleType = ∅ ∨ g.cycleType = {2, 2}
have 2 : ∀ (hg0 : HPow.hPow (α := ℤˣ) (-1) (g.cycleType.sum + 2) = 1) (h1 : 2 ≤ 4 / 2)
  (h2 : g.cycleType = Multiset.replicate 2 2), g.cycleType = ∅ ∨ g.cycleType = {2, 2}
Tactic: interval_cases g.cycleType.card
Cleared hypotheses: hg0, h1, h2
-- 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
⊢ Nontrivial α
have rw : LT.lt (α := ℕ) 1 4
Tactic: rw [← Finite.one_lt_card_iff_nontrivial, hα4]