-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem eval_mul_X_sub_C {p : R[X]} (r : R) : (p * (X - C r)).eval r = 0

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
r : R
⊢ eval r (p * (X - C r)) = 0

Tactic:
simp only [eval, eval₂_eq_sum, RingHom.id_apply]

Result:
R : Type u
inst✝ : Ring R
p : R[X]
r : R
⊢ ((p * (X - C r)).sum fun e a => a * r ^ e) = 0

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
r : R
bound : (p * (X - C r)).natDegree < p.natDegree + 2
⊢ ∀ (n : ℕ), 0 * r ^ n = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
r : R
bound : (p * (X - C r)).natDegree < p.natDegree + 2
⊢ ∑ a ∈ range (p.natDegree + 2), (p * (X - C r)).coeff a * r ^ a = 0

Tactic:
rw [sum_range_succ']

Result:
R : Type u
inst✝ : Ring R
p : R[X]
r : R
bound : (p * (X - C r)).natDegree < p.natDegree + 2
⊢ ∑ k ∈ range (p.natDegree + 1), (p * (X - C r)).coeff (k + 1) * r ^ (k + 1) + (p * (X - C r)).coeff 0 * r ^ 0 = 0

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
r : R
bound : (p * (X - C r)).natDegree < p.natDegree + 2
⊢ ∑ k ∈ range (p.natDegree + 1), (p * (X - C r)).coeff (k + 1) * r ^ (k + 1) + (p * (X - C r)).coeff 0 * r ^ 0 = 0

Tactic:
conv_lhs =>
  congr
  arg 2
  simp [coeff_mul_X_sub_C, sub_mul, mul_assoc, ← pow_succ']

Result:
R : Type u
inst✝ : Ring R
p : R[X]
r : R
bound : (p * (X - C r)).natDegree < p.natDegree + 2
⊢ ∑ k ∈ range (p.natDegree + 1), (p.coeff k * r ^ (k + 1) - p.coeff (k + 1) * r ^ (k + 1 + 1)) +
      (p * (X - C r)).coeff 0 * r ^ 0 =
    0

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
r : R
bound : (p * (X - C r)).natDegree < p.natDegree + 2
⊢ ∑ a ∈ range (p.natDegree + 2), (p * (X - C r)).coeff a * r ^ a = 0

R : Type u
inst✝ : Ring R
p : R[X]
r : R
bound : (p * (X - C r)).natDegree < p.natDegree + 2
⊢ ∀ (n : ℕ), 0 * r ^ n = 0

Tactic:
swap

Result:
R : Type u
inst✝ : Ring R
p : R[X]
r : R
bound : (p * (X - C r)).natDegree < p.natDegree + 2
⊢ ∀ (n : ℕ), 0 * r ^ n = 0

R : Type u
inst✝ : Ring R
p : R[X]
r : R
bound : (p * (X - C r)).natDegree < p.natDegree + 2
⊢ ∑ a ∈ range (p.natDegree + 2), (p * (X - C r)).coeff a * r ^ a = 0

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
r : R
bound : (p * (X - C r)).natDegree < p.natDegree + 2
⊢ ((p * (X - C r)).sum fun e a => a * r ^ e) = 0

Tactic:
rw [sum_over_range' _ _ (p.natDegree + 2) bound]

Result:
R : Type u
inst✝ : Ring R
p : R[X]
r : R
bound : (p * (X - C r)).natDegree < p.natDegree + 2
⊢ ∑ a ∈ range (p.natDegree + 2), (p * (X - C r)).coeff a * r ^ a = 0

R : Type u
inst✝ : Ring R
p : R[X]
r : R
bound : (p * (X - C r)).natDegree < p.natDegree + 2
⊢ ∀ (n : ℕ), 0 * r ^ n = 0

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
r : R
bound : (p * (X - C r)).natDegree < p.natDegree + 2
⊢ p.coeff 0 * r ^ (0 + 1) - p.coeff (p.natDegree + 1) * r ^ (p.natDegree + 1 + 1) + (p * (X - C r)).coeff 0 * r ^ 0 = 0

Tactic:
simp [coeff_monomial]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
r : R
bound : (p * (X - C r)).natDegree < p.natDegree + 2
⊢ ∑ k ∈ range (p.natDegree + 1), (p.coeff k * r ^ (k + 1) - p.coeff (k + 1) * r ^ (k + 1 + 1)) +
      (p * (X - C r)).coeff 0 * r ^ 0 =
    0

Tactic:
rw [sum_range_sub']

Result:
R : Type u
inst✝ : Ring R
p : R[X]
r : R
bound : (p * (X - C r)).natDegree < p.natDegree + 2
⊢ p.coeff 0 * r ^ (0 + 1) - p.coeff (p.natDegree + 1) * r ^ (p.natDegree + 1 + 1) + (p * (X - C r)).coeff 0 * r ^ 0 = 0

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
r : R
⊢ ((p * (X - C r)).sum fun e a => a * r ^ e) = 0

Tactic:
have bound :=
  calc
    (p * (X - C r)).natDegree ≤ p.natDegree + (X - C r).natDegree := natDegree_mul_le
    _ ≤ p.natDegree + 1 := add_le_add_left (natDegree_X_sub_C_le _) _
    _ < p.natDegree + 2 := lt_add_one _

Result:
R : Type u
inst✝ : Ring R
p : R[X]
r : R
bound : (p * (X - C r)).natDegree < p.natDegree + 2
⊢ ((p * (X - C r)).sum fun e a => a * r ^ e) = 0