awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hPirr : Irreducible P
A : K[X]
hA : cyclotomic n K = P * A
⊢ P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
have hQ : HMul.hMul (β := K[X]) P ((C : (a : K) → K[X]) P.leadingCoeff⁻¹ : K[X]) ∣ cyclotomic n K
Tactic: have hQ : P * C P.leadingCoeff⁻¹ ∣ cyclotomic n K := by
    refine ⟨A * C P.leadingCoeff, ?_⟩
    calc
      _ = P * A := hA
      _ = P * (C P.leadingCoeff⁻¹ * C P.leadingCoeff) * A := by
        simp [← C_mul, leadingCoeff_ne_zero.mpr hPirr.ne_zero]
      _ = _ := by ring
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPdeg : P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
⊢ Irreducible P
have hP0 : P ≠ 0
Tactic: have hP0 : P ≠ 0 := ne_zero_of_dvd_ne_zero (cyclotomic_ne_zero n K) hP
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPdeg : P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
hP0 : P ≠ 0
⊢ Irreducible P
have obtain : ∀ (Q : K[X]) (HQ : Q ∈ normalizedFactors P), Irreducible P
Tactic: obtain ⟨Q, HQ⟩ := exists_mem_normalizedFactors hP0 <| not_isUnit_of_natDegree_pos _ <|
    pos_of_ne_zero <| fun h ↦ orderOf_eq_zero_iff.mp (h ▸ hPdeg.symm) <| isOfFinOrder_of_finite ..
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPdeg : P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
hP0 : P ≠ 0
Q : K[X]
HQ : Q ∈ normalizedFactors P
⊢ Irreducible P
have refine : P.natDegree ≤ Q.natDegree
Tactic: refine (associated_of_dvd_of_natDegree_le (dvd_of_mem_normalizedFactors HQ) hP0 ?_).irreducible
    (irreducible_of_normalized_factor Q HQ)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPdeg : P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
hP0 : P ≠ 0
Q : K[X]
HQ : Q ∈ normalizedFactors P
⊢ P.natDegree ≤ Q.natDegree
have rw : Q ∣ cyclotomic n K
Tactic: rw [hPdeg, ← natDegree_of_dvd_cyclotomic_of_irreducible hK hn ?_
    (irreducible_of_normalized_factor Q HQ)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPdeg : P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
⊢ Irreducible P
have have : ∀ (hP0 : P ≠ 0), Irreducible P
Tactic: classical
  have hP0 : P ≠ 0 := ne_zero_of_dvd_ne_zero (cyclotomic_ne_zero n K) hP
  obtain ⟨Q, HQ⟩ := exists_mem_normalizedFactors hP0 <| not_isUnit_of_natDegree_pos _ <|
    pos_of_ne_zero <| fun h ↦ orderOf_eq_zero_iff.mp (h ▸ hPdeg.symm) <| isOfFinOrder_of_finite ..
  refine (associated_of_dvd_of_natDegree_le (dvd_of_mem_normalizedFactors HQ) hP0 ?_).irreducible
    (irreducible_of_normalized_factor Q HQ)
  rw [hPdeg, ← natDegree_of_dvd_cyclotomic_of_irreducible hK hn ?_
    (irreducible_of_normalized_factor Q HQ)]
  exact dvd_of_mem_normalizedFactors <| mem_of_le
    ((dvd_iff_normalizedFactors_le_normalizedFactors hP0 (cyclotomic_ne_zero n K)).mp hP) HQ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPdeg : P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
have have₁ have₂ : ∀ (hP0 : P ≠ 0), Irreducible P
⊢ Irreducible P
have have₃ : ∀ (hP0 : P ≠ 0) (Q : K[X]) (HQ : Q ∈ normalizedFactors P), Irreducible P
Tactic: classical
  have hP0 : P ≠ 0 := ne_zero_of_dvd_ne_zero (cyclotomic_ne_zero n K) hP
  obtain ⟨Q, HQ⟩ := exists_mem_normalizedFactors hP0 <| not_isUnit_of_natDegree_pos _ <|
    pos_of_ne_zero <| fun h ↦ orderOf_eq_zero_iff.mp (h ▸ hPdeg.symm) <| isOfFinOrder_of_finite ..
  refine (associated_of_dvd_of_natDegree_le (dvd_of_mem_normalizedFactors HQ) hP0 ?_).irreducible
    (irreducible_of_normalized_factor Q HQ)
  rw [hPdeg, ← natDegree_of_dvd_cyclotomic_of_irreducible hK hn ?_
    (irreducible_of_normalized_factor Q HQ)]
  exact dvd_of_mem_normalizedFactors <| mem_of_le
    ((dvd_iff_normalizedFactors_le_normalizedFactors hP0 (cyclotomic_ne_zero n K)).mp hP) HQ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPdeg : P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
have have₁ have₂ : ∀ (hP0 : P ≠ 0), Irreducible P
have₃ : ∀ (hP0 : P ≠ 0) (Q : K[X]) (HQ : Q ∈ normalizedFactors P), Irreducible P
⊢ Irreducible P
have have₄ : ∀ (hP0 : P ≠ 0) (Q : K[X]) (HQ : Q ∈ normalizedFactors P), P.natDegree ≤ Q.natDegree
Tactic: classical
  have hP0 : P ≠ 0 := ne_zero_of_dvd_ne_zero (cyclotomic_ne_zero n K) hP
  obtain ⟨Q, HQ⟩ := exists_mem_normalizedFactors hP0 <| not_isUnit_of_natDegree_pos _ <|
    pos_of_ne_zero <| fun h ↦ orderOf_eq_zero_iff.mp (h ▸ hPdeg.symm) <| isOfFinOrder_of_finite ..
  refine (associated_of_dvd_of_natDegree_le (dvd_of_mem_normalizedFactors HQ) hP0 ?_).irreducible
    (irreducible_of_normalized_factor Q HQ)
  rw [hPdeg, ← natDegree_of_dvd_cyclotomic_of_irreducible hK hn ?_
    (irreducible_of_normalized_factor Q HQ)]
  exact dvd_of_mem_normalizedFactors <| mem_of_le
    ((dvd_iff_normalizedFactors_le_normalizedFactors hP0 (cyclotomic_ne_zero n K)).mp hP) HQ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPdeg : P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
have have₁ have₂ : ∀ (hP0 : P ≠ 0), Irreducible P
have₃ : ∀ (hP0 : P ≠ 0) (Q : K[X]) (HQ : Q ∈ normalizedFactors P), Irreducible P
have₄ : ∀ (hP0 : P ≠ 0) (Q : K[X]) (HQ : Q ∈ normalizedFactors P), P.natDegree ≤ Q.natDegree
⊢ Irreducible P
have have₅ : ∀ (hP0 : P ≠ 0) (Q : K[X]) (HQ : Q ∈ normalizedFactors P), Q ∣ cyclotomic n K
Tactic: classical
  have hP0 : P ≠ 0 := ne_zero_of_dvd_ne_zero (cyclotomic_ne_zero n K) hP
  obtain ⟨Q, HQ⟩ := exists_mem_normalizedFactors hP0 <| not_isUnit_of_natDegree_pos _ <|
    pos_of_ne_zero <| fun h ↦ orderOf_eq_zero_iff.mp (h ▸ hPdeg.symm) <| isOfFinOrder_of_finite ..
  refine (associated_of_dvd_of_natDegree_le (dvd_of_mem_normalizedFactors HQ) hP0 ?_).irreducible
    (irreducible_of_normalized_factor Q HQ)
  rw [hPdeg, ← natDegree_of_dvd_cyclotomic_of_irreducible hK hn ?_
    (irreducible_of_normalized_factor Q HQ)]
  exact dvd_of_mem_normalizedFactors <| mem_of_le
    ((dvd_iff_normalizedFactors_le_normalizedFactors hP0 (cyclotomic_ne_zero n K)).mp hP) HQ
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
⊢ Finset.card (α := K[X]) (toFinset (normalizedFactors (cyclotomic n K))) = φ n / orderOf (unitOfCoprime (p ^ f) ⋯)
have h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
Tactic: have h := prod_normalizedFactors (cyclotomic_ne_zero n K)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
⊢ Finset.card (α := K[X]) (toFinset (normalizedFactors (cyclotomic n K))) = φ n / orderOf (unitOfCoprime (p ^ f) ⋯)
have this : ∀ (P : K[X]),
  Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P →
    P.natDegree = orderOf (unitOfCoprime (p ^ f) sorry)
Tactic: have : ∀ P ∈ normalizedFactors (cyclotomic n K),
      P.natDegree = orderOf (unitOfCoprime _ (hn.pow_left f)) := fun P hP ↦
    natDegree_of_mem_normalizedFactors_cyclotomic hK hn hP
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
this :
  ∀ (P : K[X]),
    Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P →
      P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
⊢ Finset.card (α := K[X]) (toFinset (normalizedFactors (cyclotomic n K))) = φ n / orderOf (unitOfCoprime (p ^ f) ⋯)
have H : natDegree (prod (normalizedFactors (cyclotomic n K))) = natDegree (cyclotomic n K)
Tactic: have H := natDegree_eq_of_degree_eq <| degree_eq_degree_of_associated h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
this :
  ∀ (P : K[X]),
    Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P →
      P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H : natDegree (prod (normalizedFactors (cyclotomic n K))) = natDegree (cyclotomic n K)
⊢ Finset.card (α := K[X]) (toFinset (normalizedFactors (cyclotomic n K))) = φ n / orderOf (unitOfCoprime (p ^ f) ⋯)
have H₁ : Multiset.sum (Multiset.map (fun (x : K[X]) ↦ orderOf (unitOfCoprime (p ^ f) sorry)) (normalizedFactors (cyclotomic n K))) =
  φ n
Tactic: rw [natDegree_cyclotomic, natDegree_multiset_prod _ (zero_notMem_normalizedFactors _),
    map_congr rfl this] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
this :
  ∀ (P : K[X]),
    Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P →
      P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H :
  Multiset.sum
      (Multiset.map (fun (x : K[X]) ↦ orderOf (unitOfCoprime (p ^ f) ⋯)) (normalizedFactors (cyclotomic n K))) =
    φ n
⊢ Finset.card (α := K[X]) (toFinset (normalizedFactors (cyclotomic n K))) = φ n / orderOf (unitOfCoprime (p ^ f) ⋯)
have H₁ : Multiset.card (α := K[X]) (normalizedFactors (cyclotomic n K)) * orderOf (unitOfCoprime (p ^ f) sorry) = φ n
Tactic: simp only [map_const', sum_replicate, smul_eq_mul] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
this :
  ∀ (P : K[X]),
    Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P →
      P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H : Multiset.card (α := K[X]) (normalizedFactors (cyclotomic n K)) * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
⊢ Finset.card (α := K[X]) (toFinset (normalizedFactors (cyclotomic n K))) = φ n / orderOf (unitOfCoprime (p ^ f) ⋯)
have rw : Nodup (α := K[X]) (normalizedFactors (cyclotomic n K))
Tactic: rw [← H, mul_div_left _ (orderOf_pos _), toFinset_card_of_nodup]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
this :
  ∀ (P : K[X]),
    Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P →
      P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H : Multiset.card (α := K[X]) (normalizedFactors (cyclotomic n K)) * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
⊢ Nodup (α := K[X]) (normalizedFactors (cyclotomic n K))
have refine : ∀ (P : K[X]), Multiset.count P (normalizedFactors (cyclotomic n K)) ≤ 1
Tactic: refine nodup_iff_count_le_one.mpr (fun P ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
this :
  ∀ (P : K[X]),
    Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P →
      P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H : Multiset.card (α := K[X]) (normalizedFactors (cyclotomic n K)) * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
⊢ Multiset.count P (normalizedFactors (cyclotomic n K)) ≤ 1
have by_contra! : ∀ (H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
this :
  ∀ (P : K[X]),
    Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P →
      P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H_1 : Multiset.card (α := K[X]) (normalizedFactors (cyclotomic n K)) * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
⊢ NeZero.{u_1} (R := K) (↑n : K)
have refine : ∀ (H : Eq.{u_1 + 1} (α := K) (↑n : K) 0), False
Tactic: refine ⟨fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
this :
  ∀ (P : K[X]),
    Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P →
      P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H_1 : Multiset.card (α := K[X]) (normalizedFactors (cyclotomic n K)) * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
H_2 : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
H : Eq.{u_1 + 1} (α := K) (↑n : K) 0
⊢ False
have this₁ : CharP K p
Tactic: have := charP_of_card_eq_prime_pow hK
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
this :
  ∀ (P : K[X]),
    Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P →
      P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H_1 : Multiset.card (α := K[X]) (normalizedFactors (cyclotomic n K)) * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
⊢ False
have this₁ : NeZero.{u_1} (R := K) (↑n : K)
Tactic: have : NeZero (n : K) := by
    refine ⟨fun H ↦ ?_⟩
    have := charP_of_card_eq_prime_pow hK
    exact hp.out.coprime_iff_not_dvd.mp ((coprime_pow_left_iff
      (pos_of_ne_zero <| f_ne_zero hK) _ _).mp (hn.pow_left f))
        ((CharP.cast_eq_zero_iff K p _).mp H)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
this_1 :
  ∀ (P : K[X]),
    Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P →
      P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H_1 : Multiset.card (α := K[X]) (normalizedFactors (cyclotomic n K)) * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
this : NeZero.{u_1} (R := K) (↑n : K)
⊢ False
have hP : Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P
Tactic: have hP : P ∈ normalizedFactors (cyclotomic n K) := count_pos.mp (by lia)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
this_1 :
  ∀ (P : K[X]),
    Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P →
      P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H_1 : Multiset.card (α := K[X]) (normalizedFactors (cyclotomic n K)) * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
this : NeZero.{u_1} (R := K) (↑n : K)
hP : Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P
⊢ False
have refine : P * P ∣ cyclotomic n K
Tactic: refine (prime_of_normalized_factor _ hP).not_unit (squarefree_cyclotomic n K P ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
this_1 :
  ∀ (P : K[X]),
    Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P →
      P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H_1 : Multiset.card (α := K[X]) (normalizedFactors (cyclotomic n K)) * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
this : NeZero.{u_1} (R := K) (↑n : K)
hP : Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P
⊢ LE.le (α := Multiset K[X]) {P, P} (normalizedFactors (cyclotomic n K))
have refine : ∀ (Q : K[X]), Multiset.count Q {P, P} ≤ Multiset.count Q (normalizedFactors (cyclotomic n K))
Tactic: refine le_iff_count.mpr (fun Q ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
this_1 :
  ∀ (P : K[X]),
    Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P →
      P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H_1 : Multiset.card (α := K[X]) (normalizedFactors (cyclotomic n K)) * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
this : NeZero.{u_1} (R := K) (↑n : K)
hP : Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P
Q : K[X]
⊢ Multiset.count Q {P, P} ≤ Multiset.count Q (normalizedFactors (cyclotomic n K))
have pos : ∀ (hQ : Q = P), Multiset.count Q {P, P} ≤ Multiset.count Q (normalizedFactors (cyclotomic n K))
Tactic: by_cases hQ : Q = P
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
this_1 :
  ∀ (P : K[X]),
    Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P →
      P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H_1 : Multiset.card (α := K[X]) (normalizedFactors (cyclotomic n K)) * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
this : NeZero.{u_1} (R := K) (↑n : K)
hP : Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P
Q : K[X]
pos : ∀ (hQ : Q = P), Multiset.count Q {P, P} ≤ Multiset.count Q (normalizedFactors (cyclotomic n K))
⊢ Multiset.count Q {P, P} ≤ Multiset.count Q (normalizedFactors (cyclotomic n K))
have neg : ∀ (hQ : ¬Q = P), Multiset.count Q {P, P} ≤ Multiset.count Q (normalizedFactors (cyclotomic n K))
Tactic: by_cases hQ : Q = P
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
this_1 :
  ∀ (P : K[X]),
    Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P →
      P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H_1 : Multiset.card (α := K[X]) (normalizedFactors (cyclotomic n K)) * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
this : NeZero.{u_1} (R := K) (↑n : K)
hP : Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P
Q : K[X]
hQ : Q = P
⊢ Multiset.count Q {P, P} ≤ Multiset.count Q (normalizedFactors (cyclotomic n K))
have pos : 2 ≤ Multiset.count P (normalizedFactors (cyclotomic n K))
Tactic: simp only [hQ, insert_eq_cons, count_cons_self, nodup_singleton, mem_singleton,
        count_eq_one_of_mem, reduceAdd]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst_2 : DecidableEq K
h : Associated (M := K[X]) (prod (normalizedFactors (cyclotomic n K))) (cyclotomic n K)
this_1 :
  ∀ (P : K[X]),
    Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P →
      P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H_1 : Multiset.card (α := K[X]) (normalizedFactors (cyclotomic n K)) * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
P : K[X]
H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
this : NeZero.{u_1} (R := K) (↑n : K)
hP : Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P
⊢ P * P ∣ cyclotomic n K
have this₁ : LE.le (α := Multiset K[X]) {P, P} (normalizedFactors (cyclotomic n K))
Tactic: have : {P, P} ≤ normalizedFactors (cyclotomic n K) := by
    refine le_iff_count.mpr (fun Q ↦ ?_)
    by_cases hQ : Q = P
    · simp only [hQ, insert_eq_cons, count_cons_self, nodup_singleton, mem_singleton,
        count_eq_one_of_mem, reduceAdd]
      lia
    · simp [hQ]