-- Mathlib/RingTheory/Polynomial/Ideal.lean
theorem mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero {b : R[X]} {P : R[X][X]} :
    P ∈ Ideal.span {C (X - C a), X - C b} ↔ (P.eval b).eval a = 0

Proof state:
case mpr
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
⊢ ∃ a_1 b_1, a_1 * C (X - C a) + b_1 * (X - C b) = P

Tactic:
rcases dvd_iff_isRoot.mpr h with ⟨p, hp⟩

Result:
case mpr.intro
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = (X - C a) * p
⊢ ∃ a_1 b_1, a_1 * C (X - C a) + b_1 * (X - C b) = P

Proof state:
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
⊢ P ∈ Ideal.span {C (X - C a), X - C b} ↔ eval a (eval b P) = 0

Tactic:
rw [Ideal.mem_span_pair]

Result:
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
⊢ (∃ a_1 b_1, a_1 * C (X - C a) + b_1 * (X - C b) = P) ↔ eval a (eval b P) = 0

Proof state:
case mpr.intro.intro
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = (X - C a) * p
q : R[X][X]
hq : P - C (eval b P) = (X - C b) * q
⊢ ∃ a_1 b_1, a_1 * C (X - C a) + b_1 * (X - C b) = P

Tactic:
exact ⟨C p, q, by rw [mul_comm, mul_comm q, eq_add_of_sub_eq' hq, hp, C_mul]⟩

Result:
no goals

Proof state:
case mpr.intro
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = (X - C a) * p
⊢ ∃ a_1 b_1, a_1 * C (X - C a) + b_1 * (X - C b) = P

Tactic:
rcases @X_sub_C_dvd_sub_C_eval _ b _ P with ⟨q, hq⟩

Result:
case mpr.intro.intro
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = (X - C a) * p
q : R[X][X]
hq : P - C (eval b P) = (X - C b) * q
⊢ ∃ a_1 b_1, a_1 * C (X - C a) + b_1 * (X - C b) = P

Proof state:
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
w✝¹ w✝ : R[X][X]
⊢ eval a (eval b (w✝¹ * C (X - C a) + w✝ * (X - C b))) = 0

Tactic:
simp only [eval_C, eval_X, eval_add, eval_sub, eval_mul, add_zero, mul_zero, sub_self]

Result:
no goals

Proof state:
case mp
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : ∃ a_1 b_1, a_1 * C (X - C a) + b_1 * (X - C b) = P
⊢ eval a (eval b P) = 0

Tactic:
rcases h with ⟨_, _, rfl⟩

Result:
case mp.intro.intro
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
w✝¹ w✝ : R[X][X]
⊢ eval a (eval b (w✝¹ * C (X - C a) + w✝ * (X - C b))) = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
⊢ (∃ a_1 b_1, a_1 * C (X - C a) + b_1 * (X - C b) = P) ↔ eval a (eval b P) = 0

Tactic:
constructor <;> intro h

Result:
case mp
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : ∃ a_1 b_1, a_1 * C (X - C a) + b_1 * (X - C b) = P
⊢ eval a (eval b P) = 0

case mpr
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
⊢ ∃ a_1 b_1, a_1 * C (X - C a) + b_1 * (X - C b) = P

Proof state:
R : Type u_1
inst✝ : CommRing R
a : R
b : R[X]
P : R[X][X]
h : eval a (eval b P) = 0
p : R[X]
hp : eval b P = (X - C a) * p
q : R[X][X]
hq : P - C (eval b P) = (X - C b) * q
⊢ C p * C (X - C a) + q * (X - C b) = P

Tactic:
rw [mul_comm, mul_comm q, eq_add_of_sub_eq' hq, hp, C_mul]

Result:
no goals