awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K)
simp :
  HMul.hMul (α := K[X]) (∏ i ∈ n.properDivisors, cyclotomic' i K) (cyclotomic' n K) =
      HMul.hMul (α := K[X]) (cyclotomic' n K) (∏ i ∈ n.properDivisors, cyclotomic' i K) ∧
    ⊥ < degree.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K)
⊢ 0 + HMul.hMul (α := K[X]) (∏ i ∈ n.properDivisors, cyclotomic' i K) (cyclotomic' n K) =
      HMul.hMul (α := K[X]) (cyclotomic' n K) (∏ x ∈ n.properDivisors, cyclotomic' x K) ∧
    degree.{u_2} (R := K) 0 < degree.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K)

Tactic:
simp only [degree_zero, zero_add]

Premises used: Polynomial.degree_zero, zero_add
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K)
rw rw₁ :
  HMul.hMul (α := K[X]) (cyclotomic' n K) (∏ i ∈ n.properDivisors, cyclotomic' i K) =
    HMul.hMul (α := K[X]) (cyclotomic' n K) (∏ i ∈ n.properDivisors, cyclotomic' i K)
⊢ HMul.hMul (α := K[X]) (∏ i ∈ n.properDivisors, cyclotomic' i K) (cyclotomic' n K) =
    HMul.hMul (α := K[X]) (cyclotomic' n K) (∏ i ∈ n.properDivisors, cyclotomic' i K)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K)
refine : ⊥ < degree.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K)
⊢ HMul.hMul (α := K[X]) (∏ i ∈ n.properDivisors, cyclotomic' i K) (cyclotomic' n K) =
      HMul.hMul (α := K[X]) (cyclotomic' n K) (∏ i ∈ n.properDivisors, cyclotomic' i K) ∧
    ⊥ < degree.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K)

Tactic:
refine ⟨by rw [mul_comm], ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h : IsPrimitiveRoot ζ n
prod_monic : Monic.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K)
rw : degree.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K) ≠ ⊥
⊢ ⊥ < degree.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K)

Tactic:
rw [bot_lt_iff_ne_bot]

Premises used: bot_lt_iff_ne_bot
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h_1 : IsPrimitiveRoot ζ n
prod_monic : Monic.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K)
h : degree.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K) = ⊥
⊢ False

Tactic:
Monic.ne_zero prod_monic (degree_eq_bot.1 h)

Premises used: Iff.mp, Polynomial.degree_eq_bot, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
hpos : 0 < n
h_1 : IsPrimitiveRoot ζ n
prod_monic : Monic.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K)
h : degree.{u_2} (R := K) (∏ i ∈ n.properDivisors, cyclotomic' i K) = ⊥
⊢ False

Tactic:
exact Monic.ne_zero prod_monic (degree_eq_bot.1 h)

Premises used: Iff.mp, Polynomial.degree_eq_bot, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ ∃ (P : ℤ[X]),
    Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' n K) ∧ P.degree = degree (cyclotomic' n K) ∧ P.Monic

Tactic:
lifts_and_degree_eq_and_monic ?_ (cyclotomic'.monic n K)

Premises used: Polynomial.lifts_and_degree_eq_and_monic, Polynomial.cyclotomic'.monic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
h : IsPrimitiveRoot ζ n
refine : Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' n K)
⊢ ∃ (P : ℤ[X]),
    Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' n K) ∧ P.degree = degree (cyclotomic' n K) ∧ P.Monic

Tactic:
refine lifts_and_degree_eq_and_monic ?_ (cyclotomic'.monic n K)

Premises used: Polynomial.lifts_and_degree_eq_and_monic, Polynomial.cyclotomic'.monic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
n : ℕ
h : IsPrimitiveRoot ζ n
h₁ :
  ∀ (k : ℕ)
    (ihk :
      ∀ m < k,
        ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
          Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K))
    {ζ : K} (h : IsPrimitiveRoot ζ k),
    Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' k K)
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' n K)

Tactic:
induction n using Nat.strong_induction_on generalizing ζ with | _ k ihk
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
h₁ :
  ∀
    (ihk :
      ∀ m < 0,
        ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
          Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K))
    (h : IsPrimitiveRoot ζ 0),
    Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' 0 K)
h₂ : ∀ (hpos : k > 0), Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' k K)
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' k K)

Tactic:
rcases k.eq_zero_or_pos with (rfl | hpos)

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
ihk :
  ∀ m < 0,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
h : IsPrimitiveRoot ζ 0
h₁ : Eq.{u_2 + 1} (α := K[X]) ((mapRingHom (Int.castRingHom K) : (a : ℤ[X]) → K[X]) 1 : K[X]) (cyclotomic' 0 K : K[X])
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' 0 K)

Tactic:
use 1
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
ζ : K
ihk :
  ∀ m < 0,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
h : IsPrimitiveRoot ζ 0
⊢ Eq.{u_2 + 1} (α := K[X]) ((mapRingHom (Int.castRingHom K) : (a : ℤ[X]) → K[X]) 1 : K[X]) (cyclotomic' 0 K : K[X])

Tactic:
simp only [cyclotomic'_zero, coe_mapRingHom, Polynomial.map_one]

Premises used: Polynomial.map_one, Polynomial.coe_mapRingHom, Polynomial.cyclotomic'_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
hs : ∀ i ∈ k.properDivisors, Monic (cyclotomic' i K)
⊢ B.Monic

Tactic:
apply monic_prod_of_monic

Premises used: Polynomial.monic_prod_of_monic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
i : ℕ
hs : i ∈ k.properDivisors → Monic (cyclotomic' i K)
⊢ i ∈ k.properDivisors → Monic (cyclotomic' i K)

Tactic:
_
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
i : ℕ
h_1 : i ∈ k.properDivisors
⊢ Monic (cyclotomic' i K)

Tactic:
cyclotomic'.monic i K

Premises used: Polynomial.cyclotomic'.monic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
i : ℕ
h_1 : i ∈ k.properDivisors
⊢ Monic (cyclotomic' i K)

Tactic:
exact cyclotomic'.monic i K

Premises used: Polynomial.cyclotomic'.monic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
⊢ B.Monic

Tactic:
have Bmo : B.Monic := by
    apply monic_prod_of_monic
    intro i _
    exact cyclotomic'.monic i K
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) B

Tactic:
Subsemiring.prod_mem (lifts (Int.castRingHom K)) ?_

Premises used: Set.Mem, Subsemiring.prod_mem, Int.castRingHom, Polynomial.lifts
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
refine :
  ∀ c ∈ k.properDivisors, Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' c K)
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) B

Tactic:
refine Subsemiring.prod_mem (lifts (Int.castRingHom K)) ?_

Premises used: Subsemiring.prod_mem, Int.castRingHom, Polynomial.lifts
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
x : ℕ
hx : x ∈ k.properDivisors
⊢ x < k

Tactic:
have xsmall := (Nat.mem_properDivisors.1 hx).2
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
x : ℕ
hx : x ∈ k.properDivisors
xsmall : x < k
obtain :
  ∀ (d : ℕ) (hd : k = x * d),
    Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' x K)
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' x K)

Tactic:
obtain ⟨d, hd⟩ := (Nat.mem_properDivisors.1 hx).1

Premises used: And.left, Iff.mp, Nat.mem_properDivisors
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
x : ℕ
hx : x ∈ k.properDivisors
xsmall : x < k
d : ℕ
hd : k = x * d
⊢ k = d * x

Tactic:
rw [mul_comm] at hd

Premises used: mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
x : ℕ
hx : x ∈ k.properDivisors
xsmall : x < k
d : ℕ
hd : k = d * x
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' x K)

Tactic:
ihk x xsmall (h.pow hpos hd)

Premises used: Set.Mem, IsPrimitiveRoot.pow
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
x : ℕ
hx : x ∈ k.properDivisors
xsmall : x < k
d : ℕ
hd : k = d * x
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' x K)

Tactic:
exact ihk x xsmall (h.pow hpos hd)

Premises used: IsPrimitiveRoot.pow
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) B

Tactic:
have Bint : B ∈ lifts (Int.castRingHom K) := by
    refine Subsemiring.prod_mem (lifts (Int.castRingHom K)) ?_
    intro x hx
    have xsmall := (Nat.mem_properDivisors.1 hx).2
    obtain ⟨d, hd⟩ := (Nat.mem_properDivisors.1 hx).1
    rw [mul_comm] at hd
    exact ihk x xsmall (h.pow hpos hd)
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
Bint : Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) B
⊢ ∃ (q : ℤ[X]), map (Int.castRingHom K) q = B ∧ q.degree = B.degree ∧ q.Monic

Tactic:
replace Bint := lifts_and_degree_eq_and_monic Bint Bmo
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
Bint : ∃ (q : ℤ[X]), map (Int.castRingHom K) q = B ∧ q.degree = B.degree ∧ q.Monic
h₁ :
  ∀ (B₁ : ℤ[X]) (hB₁ : map (Int.castRingHom K) B₁ = B),
    B₁.degree = B.degree →
      ∀ (hB₁mo : B₁.Monic),
        Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' k K)
⊢ Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' k K)

Tactic:
obtain ⟨B₁, hB₁, _, hB₁mo⟩ := Bint
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left_1 : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B₁
left : 0 + B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1
right : degree.{u_2} (R := K) 0 < B.degree
⊢ 0 + B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1 ∧ degree.{u_2} (R := K) 0 < B.degree

Tactic:
constructor
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left_1 : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B₁
left : B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1
left₁ : cyclotomic' k K * B = HPow.hPow (α := K[X]) X k - 1
left₂ : cyclotomic' k K * B = ∏ i ∈ k.divisors, cyclotomic' i K
left₃ : cyclotomic' k K * B = ∏ i ∈ Finset.cons k k.properDivisors ⋯, cyclotomic' i K
left₄ left₅ : cyclotomic' k K * B = HMul.hMul (α := K[X]) (cyclotomic' k K) (∏ x ∈ k.properDivisors, cyclotomic' x K)
⊢ 0 + B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1

Tactic:
rw [zero_add, mul_comm, ← prod_cyclotomic'_eq_X_pow_sub_one hpos h, ←
        Nat.cons_self_properDivisors hpos.ne', Finset.prod_cons]

Premises used: Polynomial.prod_cyclotomic'_eq_X_pow_sub_one, zero_add, LT.lt.ne', Nat.cons_self_properDivisors, Finset.prod_cons, mul_comm
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B₁
⊢ degree.{u_2} (R := K) 0 < B.degree

Tactic:
simpa only [degree_zero, bot_lt_iff_ne_bot, Ne, degree_eq_bot] using Bmo.ne_zero

Premises used: bot_lt_iff_ne_bot, Ne, Polynomial.degree_zero, Polynomial.degree_eq_bot, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B₁
⊢ 0 + B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1 ∧ degree.{u_2} (R := K) 0 < B.degree

Tactic:
have huniq : 0 + B * cyclotomic' k K = X ^ k - 1 ∧ (0 : K[X]).degree < B.degree := by
    constructor
    · rw [zero_add, mul_comm, ← prod_cyclotomic'_eq_X_pow_sub_one hpos h, ←
        Nat.cons_self_properDivisors hpos.ne', Finset.prod_cons]
    · simpa only [degree_zero, bot_lt_iff_ne_bot, Ne, degree_eq_bot] using Bmo.ne_zero
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B₁
huniq : 0 + B * cyclotomic' k K = HPow.hPow (α := K[X]) X k - 1 ∧ degree.{u_2} (R := K) 0 < B.degree
⊢ (HPow.hPow (α := K[X]) X k - 1) /ₘ B = cyclotomic' k K ∧ (HPow.hPow (α := K[X]) X k - 1) %ₘ B = 0

Tactic:
replace huniq := div_modByMonic_unique (cyclotomic' k K) (0 : K[X]) Bmo huniq
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B₁
huniq : (HPow.hPow (α := K[X]) X k - 1) /ₘ B = cyclotomic' k K ∧ (HPow.hPow (α := K[X]) X k - 1) %ₘ B = 0
h₁ : Eq.{u_2 + 1} (α := K[X]) ((mapRingHom (Int.castRingHom K) : (a : ℤ[X]) → K[X]) Q₁ : K[X]) (cyclotomic' k K : K[X])
⊢ ∃ (x : ℤ[X]),
    Eq.{u_2 + 1} (α := K[X]) ((mapRingHom (Int.castRingHom K) : (a : ℤ[X]) → K[X]) x : K[X]) (cyclotomic' k K : K[X])

Tactic:
use Q₁
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B₁
huniq : (HPow.hPow (α := K[X]) X k - 1) /ₘ B = cyclotomic' k K ∧ (HPow.hPow (α := K[X]) X k - 1) %ₘ B = 0
h₁ : map (Int.castRingHom K) (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B = (HPow.hPow (α := K[X]) X k - 1) /ₘ B
⊢ Eq.{u_2 + 1} (α := K[X]) ((mapRingHom (Int.castRingHom K) : (a : ℤ[X]) → K[X]) Q₁ : K[X]) (cyclotomic' k K : K[X])

Tactic:
rw [coe_mapRingHom, map_divByMonic (Int.castRingHom K) hB₁mo, hB₁, ← huniq.1]

Premises used: Polynomial.coe_mapRingHom, And.left, Int.castRingHom, Polynomial.map_divByMonic
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
k : ℕ
ihk :
  ∀ m < k,
    ∀ {ζ : K} (h : IsPrimitiveRoot ζ m),
      Membership.mem (γ := Subsemiring K[X]) (lifts (R := ℤ) (Int.castRingHom K)) (cyclotomic' m K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
B₁ : ℤ[X]
hB₁ : map (Int.castRingHom K) B₁ = B
left : B₁.degree = B.degree
hB₁mo : B₁.Monic
Q₁ : ℤ[X] := (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B₁
huniq : (HPow.hPow (α := K[X]) X k - 1) /ₘ B = cyclotomic' k K ∧ (HPow.hPow (α := K[X]) X k - 1) %ₘ B = 0
⊢ map (Int.castRingHom K) (HPow.hPow (α := ℤ[X]) X k - 1) /ₘ B = (HPow.hPow (α := K[X]) X k - 1) /ₘ B

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Goal:
K : Type u_2
inst : CommRing K
inst_1 : IsDomain K
inst_2 : CharZero K
ζ : K
n : ℕ+
h : IsPrimitiveRoot ζ (↑n : ℕ)
obtain :
  ∀ (P : ℤ[X])
    (hP :
      Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K) ∧
        P.degree = degree (cyclotomic' (↑n : ℕ) K) ∧ P.Monic),
    ∃! P : ℤ[X], Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K)
⊢ ∃! P : ℤ[X], Eq (α := K[X]) (map (Int.castRingHom K) P) (cyclotomic' (↑n : ℕ) K)

Tactic:
obtain ⟨P, hP⟩ := int_coeff_of_cyclotomic' h

Premises used: Polynomial.int_coeff_of_cyclotomic'