-- Mathlib/RingTheory/Polynomial/Quotient.lean
theorem eval₂_C_mk_eq_zero {I : Ideal R} :
    ∀ f ∈ (map (C : R →+* R[X]) I : Ideal R[X]), eval₂RingHom (C.comp (Quotient.mk I)) X f = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ eval₂ (C.comp (Quotient.mk I)) X (a.sum fun n a => (monomial n) a) = 0

Tactic:
rw [eval₂_sum]

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ (a.sum fun n a => eval₂ (C.comp (Quotient.mk I)) X ((monomial n) a)) = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ (eval₂RingHom (C.comp (Quotient.mk I)) X) a = 0

Tactic:
rw [← sum_monomial_eq a]

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ (eval₂RingHom (C.comp (Quotient.mk I)) X) (a.sum fun n a => (monomial n) a) = 0

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
m : ℕ
h : m = 0
⊢ (if m = 0 then (Quotient.mk I) (a.coeff n) else 0) = coeff 0 m

Tactic:
simpa [h] using Quotient.eq_zero_iff_mem.2 ((mem_map_C_iff.1 ha) n)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
⊢ eval₂ (C.comp (Quotient.mk I)) X ((monomial n) (a.coeff n)) = 0

Tactic:
rw [eval₂_monomial (C.comp (Quotient.mk I)) X]

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
⊢ (C.comp (Quotient.mk I)) (a.coeff n) * X ^ n = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ (a.sum fun n a => eval₂ (C.comp (Quotient.mk I)) X ((monomial n) a)) = 0

Tactic:
refine Finset.sum_eq_zero fun n _ => ?_

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
⊢ (fun n a => eval₂ (C.comp (Quotient.mk I)) X ((monomial n) a)) n (a.coeff n) = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
⊢ (C.comp (Quotient.mk I)) (a.coeff n) * X ^ n = 0

Tactic:
refine mul_eq_zero_of_left (Polynomial.ext fun m => ?_) (X ^ n)

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
m : ℕ
⊢ ((C.comp (Quotient.mk I)) (a.coeff n)).coeff m = coeff 0 m

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ (eval₂RingHom (C.comp (Quotient.mk I)) X) (a.sum fun n a => (monomial n) a) = 0

Tactic:
dsimp

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ eval₂ (C.comp (Quotient.mk I)) X (a.sum fun n a => (monomial n) a) = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
m : ℕ
⊢ ((C.comp (Quotient.mk I)) (a.coeff n)).coeff m = coeff 0 m

Tactic:
erw [coeff_C]

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
m : ℕ
⊢ (if m = 0 then (Quotient.mk I) (a.coeff n) else 0) = coeff 0 m

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
⊢ (fun n a => eval₂ (C.comp (Quotient.mk I)) X ((monomial n) a)) n (a.coeff n) = 0

Tactic:
dsimp

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
⊢ eval₂ (C.comp (Quotient.mk I)) X ((monomial n) (a.coeff n)) = 0

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
m : ℕ
h : ¬m = 0
⊢ (if m = 0 then (Quotient.mk I) (a.coeff n) else 0) = coeff 0 m

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ f ∈ map C I, (eval₂RingHom (C.comp (Quotient.mk I)) X) f = 0

Tactic:
intro a ha

Result:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ (eval₂RingHom (C.comp (Quotient.mk I)) X) a = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
m : ℕ
⊢ (if m = 0 then (Quotient.mk I) (a.coeff n) else 0) = coeff 0 m

Tactic:
by_cases h : m = 0

Result:
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
m : ℕ
h : m = 0
⊢ (if m = 0 then (Quotient.mk I) (a.coeff n) else 0) = coeff 0 m

case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ a.support
m : ℕ
h : ¬m = 0
⊢ (if m = 0 then (Quotient.mk I) (a.coeff n) else 0) = coeff 0 m