-- Mathlib/Algebra/Polynomial/Div.lean
theorem modByMonic_X_sub_C_eq_C_eval (p : R[X]) (a : R) : p %ₘ (X - C a) = C (p.eval a)

Proof state:
case bot
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
⊢ ⊥ < 1 → ⊥ ≤ 0

Tactic:
exact fun _ => bot_le

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
⊢ p %ₘ (X - C a) = C (eval a p)

Tactic:
have : degree (p %ₘ (X - C a)) < 1 :=
  degree_X_sub_C a ▸ degree_modByMonic_lt p (monic_X_sub_C a)

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
this : (p %ₘ (X - C a)).degree < 1
⊢ p %ₘ (X - C a) = C (eval a p)

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : (p %ₘ (X - C a)).coeff 0 = eval a p
this✝ : (p %ₘ (X - C a)).degree < 1
this : (p %ₘ (X - C a)).degree ≤ 0
⊢ p %ₘ (X - C a) = C (eval a p)

Tactic:
rw [eq_C_of_degree_le_zero this, h]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
⊢ eval a (p %ₘ (X - C a)) = eval a p

Tactic:
rw [modByMonic_eq_sub_mul_div _ (monic_X_sub_C a), eval_sub, eval_mul, eval_sub, eval_X,
  eval_C, sub_self, zero_mul, sub_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
this✝ : (p %ₘ (X - C a)).degree < 1
this : (p %ₘ (X - C a)).degree ≤ 0
⊢ p %ₘ (X - C a) = C (eval a p)

Tactic:
rw [eq_C_of_degree_le_zero this, eval_C] at h

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : (p %ₘ (X - C a)).coeff 0 = eval a p
this✝ : (p %ₘ (X - C a)).degree < 1
this : (p %ₘ (X - C a)).degree ≤ 0
⊢ p %ₘ (X - C a) = C (eval a p)

Proof state:
case coe
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝¹ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
a✝ : ℕ
⊢ ↑a✝ < 1 → ↑a✝ ≤ 0

Tactic:
exact fun h => WithBot.coe_le_coe.2 (Nat.le_of_lt_succ (WithBot.coe_lt_coe.1 h))

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
⊢ p %ₘ (X - C a) = C (eval a p)

Tactic:
have h : (p %ₘ (X - C a)).eval a = p.eval a := by
  rw [modByMonic_eq_sub_mul_div _ (monic_X_sub_C a), eval_sub, eval_mul, eval_sub, eval_X,
    eval_C, sub_self, zero_mul, sub_zero]

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
⊢ p %ₘ (X - C a) = C (eval a p)

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
⊢ (p %ₘ (X - C a)).degree < 1 → (p %ₘ (X - C a)).degree ≤ 0

Tactic:
cases degree (p %ₘ (X - C a))

Result:
case bot
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
⊢ ⊥ < 1 → ⊥ ≤ 0

case coe
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝¹ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
a✝ : ℕ
⊢ ↑a✝ < 1 → ↑a✝ ≤ 0

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
⊢ p %ₘ (X - C a) = C (eval a p)

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
⊢ p %ₘ (X - C a) = C (eval a p)

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
this : (p %ₘ (X - C a)).degree < 1
⊢ (p %ₘ (X - C a)).degree ≤ 0

Tactic:
revert this

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
a : R
a✝ : Nontrivial R
h : eval a (p %ₘ (X - C a)) = eval a p
⊢ (p %ₘ (X - C a)).degree < 1 → (p %ₘ (X - C a)).degree ≤ 0