-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem int_coeff_of_cyclotomic' {K : Type*} [CommRing K] [IsDomain K] {ζ : K} {n : ℕ}
    (h : IsPrimitiveRoot ζ n) : ∃ P : ℤ[X], map (Int.castRingHom K) P =
      cyclotomic' n K ∧ P.degree = (cyclotomic' n K).degree ∧ P.Monic

Proof state:
case h.inr.intro.intro.intro
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom 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] := (X ^ k - 1) /ₘ B₁
huniq : 0 + B * cyclotomic' k K = X ^ k - 1 ∧ degree 0 < B.degree
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)

Tactic:
replace huniq := div_modByMonic_unique (cyclotomic' k K) (0 : K[X]) Bmo huniq

Result:
case h.inr.intro.intro.intro
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom 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] := (X ^ k - 1) /ₘ B₁
huniq : (X ^ k - 1) /ₘ B = cyclotomic' k K ∧ (X ^ k - 1) %ₘ B = 0
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)

Proof state:
case h
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)

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

Result:
case h.inl
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
ihk : ∀ m < 0, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
h : IsPrimitiveRoot ζ 0
⊢ cyclotomic' 0 K ∈ lifts (Int.castRingHom K)

case h.inr
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)

Proof state:
case intro
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom 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
⊢ cyclotomic' x K ∈ lifts (Int.castRingHom K)

Tactic:
rw [mul_comm] at hd

Result:
case intro
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom 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
⊢ cyclotomic' x K ∈ lifts (Int.castRingHom K)

Proof state:
case h.inl
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
ihk : ∀ m < 0, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
h : IsPrimitiveRoot ζ 0
⊢ cyclotomic' 0 K ∈ lifts (Int.castRingHom K)

Tactic:
use 1

Result:
case h
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
ζ : K
ihk : ∀ m < 0, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
h : IsPrimitiveRoot ζ 0
⊢ (mapRingHom (Int.castRingHom K)) 1 = cyclotomic' 0 K

Proof state:
case hs
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
i : ℕ
a✝ : i ∈ k.properDivisors
⊢ (cyclotomic' i K).Monic

Tactic:
exact cyclotomic'.monic i K

Result:
no goals

Proof state:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom 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
⊢ cyclotomic' x K ∈ lifts (Int.castRingHom K)

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

Result:
case intro
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom 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
⊢ cyclotomic' x K ∈ lifts (Int.castRingHom K)

Proof state:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
⊢ ∀ c ∈ k.properDivisors, cyclotomic' c K ∈ lifts (Int.castRingHom K)

Tactic:
intro x hx

Result:
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom 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
⊢ cyclotomic' x K ∈ lifts (Int.castRingHom K)

Proof state:
case h.inr
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
Bint : B ∈ lifts (Int.castRingHom K)
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)

Tactic:
replace Bint := lifts_and_degree_eq_and_monic Bint Bmo

Result:
case h.inr
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
Bint : ∃ q, map (Int.castRingHom K) q = B ∧ q.degree = B.degree ∧ q.Monic
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)

Proof state:
case h.inr
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom K)
ζ : K
h : IsPrimitiveRoot ζ k
hpos : k > 0
B : K[X] := ∏ i ∈ k.properDivisors, cyclotomic' i K
Bmo : B.Monic
Bint : ∃ q, map (Int.castRingHom K) q = B ∧ q.degree = B.degree ∧ q.Monic
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)

Tactic:
obtain ⟨B₁, hB₁, _, hB₁mo⟩ := Bint

Result:
case h.inr.intro.intro.intro
K : Type u_2
inst✝¹ : CommRing K
inst✝ : IsDomain K
k : ℕ
ihk : ∀ m < k, ∀ {ζ : K}, IsPrimitiveRoot ζ m → cyclotomic' m K ∈ lifts (Int.castRingHom 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
⊢ cyclotomic' k K ∈ lifts (Int.castRingHom K)