-- Mathlib/Algebra/Polynomial/Div.lean
lemma eval_divByMonic_eq_trailingCoeff_comp {p : R[X]} {t : R} :
    (p /ₘ (X - C t) ^ p.rootMultiplicity t).eval t = (p.comp (X + C t)).trailingCoeff

Proof state:
case inl
R : Type u
inst✝ : CommRing R
t : R
⊢ eval t (0 /ₘ (X - C t) ^ rootMultiplicity t 0) = (comp 0 (X + C t)).trailingCoeff

Tactic:
rw [zero_divByMonic, eval_zero, zero_comp, trailingCoeff_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
⊢ (g.comp (X + C t)).coeff 0 = eval t g

Tactic:
rw [coeff_zero_eq_eval_zero, eval_comp, eval_add, eval_X, eval_C, zero_add]

Result:
no goals

Proof state:
case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
mul_eq : (X - C t) ^ m * (p /ₘ (X - C t) ^ m) = p
⊢ eval t (p /ₘ (X - C t) ^ m) = (p.comp (X + C t)).trailingCoeff

Tactic:
set g := p /ₘ (X - C t) ^ m

Result:
case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
⊢ eval t g = (p.comp (X + C t)).trailingCoeff

Proof state:
case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
⊢ eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = (p.comp (X + C t)).trailingCoeff

Tactic:
have mul_eq := p.pow_mul_divByMonic_rootMultiplicity_eq t

Result:
case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
mul_eq : (X - C t) ^ rootMultiplicity t p * (p /ₘ (X - C t) ^ rootMultiplicity t p) = p
⊢ eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = (p.comp (X + C t)).trailingCoeff

Proof state:
case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
⊢ eval t g = (p.comp (X + C t)).trailingCoeff

Tactic:
have : (g.comp (X + C t)).coeff 0 = g.eval t := by
  rw [coeff_zero_eq_eval_zero, eval_comp, eval_add, eval_X, eval_C, zero_add]

Result:
case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
g : R[X] := p /ₘ (X - C t) ^ m
mul_eq : (X - C t) ^ m * g = p
this : (g.comp (X + C t)).coeff 0 = eval t g
⊢ eval t g = (p.comp (X + C t)).trailingCoeff

Proof state:
case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
mul_eq : (X - C t) ^ rootMultiplicity t p * (p /ₘ (X - C t) ^ rootMultiplicity t p) = p
⊢ eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = (p.comp (X + C t)).trailingCoeff

Tactic:
set m := p.rootMultiplicity t

Result:
case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
m : ℕ := rootMultiplicity t p
mul_eq : (X - C t) ^ m * (p /ₘ (X - C t) ^ m) = p
⊢ eval t (p /ₘ (X - C t) ^ m) = (p.comp (X + C t)).trailingCoeff

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
⊢ eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = (p.comp (X + C t)).trailingCoeff

Tactic:
obtain rfl | hp := eq_or_ne p 0

Result:
case inl
R : Type u
inst✝ : CommRing R
t : R
⊢ eval t (0 /ₘ (X - C t) ^ rootMultiplicity t 0) = (comp 0 (X + C t)).trailingCoeff

case inr
R : Type u
inst✝ : CommRing R
p : R[X]
t : R
hp : p ≠ 0
⊢ eval t (p /ₘ (X - C t) ^ rootMultiplicity t p) = (p.comp (X + C t)).trailingCoeff