awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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)
⊢ Multiset.sum
      (Multiset.map (fun (x : K[X]) ↦ orderOf (unitOfCoprime (p ^ f) ⋯)) (normalizedFactors (cyclotomic n K))) =
    φ n

Tactic:
rw [natDegree_cyclotomic, natDegree_multiset_prod _ (zero_notMem_normalizedFactors _),
    map_congr rfl this] at H

Premises used: Polynomial.natDegree_cyclotomic, Polynomial.natDegree_multiset_prod, Multiset.map_congr, UniqueFactorizationMonoid.zero_notMem_normalizedFactors, rfl
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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
⊢ Multiset.card (α := K[X]) (normalizedFactors (cyclotomic n K)) * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n

Tactic:
simp only [map_const', sum_replicate, smul_eq_mul] at H

Premises used: Multiset.sum_replicate, smul_eq_mul, Multiset.map_const'
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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
rw : Nodup (α := K[X]) (normalizedFactors (cyclotomic n K))
⊢ Finset.card (α := K[X]) (toFinset (normalizedFactors (cyclotomic n K))) = φ n / orderOf (unitOfCoprime (p ^ f) ⋯)

Tactic:
rw [← H, mul_div_left _ (orderOf_pos _), toFinset_card_of_nodup]

Premises used: Nat.mul_div_left, Multiset.toFinset_card_of_nodup, orderOf_pos
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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))

Tactic:
nodup_iff_count_le_one.mpr (fun P ↦ ?_)

Premises used: Iff.mpr, Multiset.nodup_iff_count_le_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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
refine : ∀ (P : K[X]), Multiset.count P (normalizedFactors (cyclotomic n K)) ≤ 1
⊢ Nodup (α := K[X]) (normalizedFactors (cyclotomic n K))

Tactic:
refine nodup_iff_count_le_one.mpr (fun P ↦ ?_)

Premises used: Iff.mpr, Multiset.nodup_iff_count_le_one
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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]
by_contra! : ∀ (H : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))), False
⊢ Multiset.count P (normalizedFactors (cyclotomic n K)) ≤ 1

Tactic:
by_contra! H
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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)

Tactic:
⟨fun H ↦ ?_⟩

Premises used: NeZero.mk
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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))
refine : ∀ (H : Eq.{u_1 + 1} (α := K) (↑n : K) 0), False
⊢ NeZero.{u_1} (R := K) (↑n : K)

Tactic:
refine ⟨fun H ↦ ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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
⊢ CharP K p

Tactic:
have := charP_of_card_eq_prime_pow hK
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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_2 : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
H : Eq.{u_1 + 1} (α := K) (↑n : K) 0
this : CharP K p
⊢ False

Tactic:
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)

Premises used: _private.0.Polynomial.f_ne_zero, Nat.Coprime.pow_left, pos_of_ne_zero, Iff.mp, CharP.cast_eq_zero_iff, Nat.Prime.coprime_iff_not_dvd, Nat.coprime_pow_left_iff, Fact.out
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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_2 : 1 < Multiset.count P (normalizedFactors (cyclotomic n K))
H : Eq.{u_1 + 1} (α := K) (↑n : K) 0
this : CharP K p
⊢ False

Tactic:
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)

Premises used: _private.0.Polynomial.f_ne_zero, Nat.Coprime.pow_left, pos_of_ne_zero, Iff.mp, CharP.cast_eq_zero_iff, Nat.Prime.coprime_iff_not_dvd, Nat.coprime_pow_left_iff, Fact.out
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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)

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)
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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)
⊢ 0 < Multiset.count P (normalizedFactors (cyclotomic n K))

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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)
⊢ Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P

Tactic:
have hP : P ∈ normalizedFactors (cyclotomic n K) := count_pos.mp (by lia)
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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

Tactic:
(prime_of_normalized_factor _ hP).not_unit (squarefree_cyclotomic n K P ?_)

Premises used: Polynomial.squarefree_cyclotomic, Prime.not_unit, UniqueFactorizationMonoid.prime_of_normalized_factor
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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
refine : P * P ∣ cyclotomic n K
⊢ False

Tactic:
refine (prime_of_normalized_factor _ hP).not_unit (squarefree_cyclotomic n K P ?_)

Premises used: Polynomial.squarefree_cyclotomic, Prime.not_unit, UniqueFactorizationMonoid.prime_of_normalized_factor
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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))

Tactic:
le_iff_count.mpr (fun Q ↦ ?_)

Premises used: Iff.mpr, Multiset.le_iff_count
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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
refine : ∀ (Q : K[X]), Multiset.count Q {P, P} ≤ Multiset.count Q (normalizedFactors (cyclotomic n K))
⊢ LE.le (α := Multiset K[X]) {P, P} (normalizedFactors (cyclotomic n K))

Tactic:
refine le_iff_count.mpr (fun Q ↦ ?_)

Premises used: Iff.mpr, Multiset.le_iff_count
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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))
neg : ∀ (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))

Tactic:
by_cases hQ : Q = P
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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
pos : 2 ≤ Multiset.count P (normalizedFactors (cyclotomic n K))
⊢ Multiset.count Q {P, P} ≤ Multiset.count Q (normalizedFactors (cyclotomic n K))

Tactic:
simp only [hQ, insert_eq_cons, count_cons_self, nodup_singleton, mem_singleton,
        count_eq_one_of_mem, reduceAdd]

Premises used: Nat.reduceAdd, Multiset.count_eq_one_of_mem, Multiset.mem_singleton, Multiset.count_cons_self, Multiset.insert_eq_cons, Multiset.nodup_singleton
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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
⊢ 2 ≤ Multiset.count P (normalizedFactors (cyclotomic n K))

Tactic:
lia
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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))

Tactic:
simp [hQ]
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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))

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]
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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_2 : NeZero.{u_1} (R := K) (↑n : K)
hP : Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P
this : LE.le (α := Multiset K[X]) {P, P} (normalizedFactors (cyclotomic n K))
⊢ Dvd.dvd (α := K[X]) (prod {P, P}) (prod (normalizedFactors (cyclotomic n K)))

Tactic:
have := prod_dvd_prod_of_le this
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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_2 : NeZero.{u_1} (R := K) (↑n : K)
hP : Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P
this_3 : LE.le (α := Multiset K[X]) {P, P} (normalizedFactors (cyclotomic n K))
this : Dvd.dvd (α := K[X]) (prod {P, P}) (prod (normalizedFactors (cyclotomic n K)))
⊢ P * P ∣ prod (normalizedFactors (cyclotomic n K))

Tactic:
simp only [insert_eq_cons, prod_cons, prod_singleton] at this

Premises used: Multiset.prod_cons, Multiset.prod_singleton, Multiset.insert_eq_cons
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
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_2 : NeZero.{u_1} (R := K) (↑n : K)
hP : Membership.mem (γ := Multiset K[X]) (normalizedFactors (cyclotomic n K)) P
this_3 : LE.le (α := Multiset K[X]) {P, P} (normalizedFactors (cyclotomic n K))
this : P * P ∣ prod (normalizedFactors (cyclotomic n K))
⊢ P * P ∣ cyclotomic n K

Tactic:
this.trans h.dvd

Premises used: Associated.dvd, Dvd.dvd.trans