-- Mathlib/RingTheory/Polynomial/Nilpotent.lean
protected lemma isNilpotent_iff :
    IsNilpotent P ↔ ∀ i, IsNilpotent (coeff P i)

Proof state:
case refine_2.succ
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
hr : IsNilpotent (C r)
i : ℕ
⊢ IsNilpotent ((p + C r).coeff (i + 1))

Tactic:
simp only [coeff_add, coeff_C_succ, add_zero]

Result:
case refine_2.succ
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
hr : IsNilpotent (C r)
i : ℕ
⊢ IsNilpotent (p.coeff (i + 1))

Proof state:
case refine_3.zero
R : Type u_1
inst✝ : CommRing R
P p : R[X]
x✝ : p ≠ 0
hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpX : IsNilpotent (p * X)
⊢ IsNilpotent ((p * X).coeff 0)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
P : R[X]
⊢ IsNilpotent P ↔ ∀ (i : ℕ), IsNilpotent (P.coeff i)

Tactic:
refine
  ⟨P.recOnHorner (by simp) (fun p r hp₀ _ hp hpr i ↦ ?_) (fun p _ hnp hpX i ↦ ?_), fun h ↦ ?_⟩

Result:
case refine_1
R : Type u_1
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
⊢ IsNilpotent P

case refine_2
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
i : ℕ
⊢ IsNilpotent ((p + C r).coeff i)

case refine_3
R : Type u_1
inst✝ : CommRing R
P p : R[X]
x✝ : p ≠ 0
hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpX : IsNilpotent (p * X)
i : ℕ
⊢ IsNilpotent ((p * X).coeff i)

Proof state:
case refine_2.succ.a
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
hr : IsNilpotent (C r)
i : ℕ
⊢ IsNilpotent p

Tactic:
simpa using Commute.isNilpotent_sub (Commute.all _ _) hpr hr

Result:
no goals

Proof state:
case refine_1
R : Type u_1
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
⊢ IsNilpotent (P.sum fun n a => (monomial n) a)

Tactic:
exact isNilpotent_sum (fun i _ ↦ by simpa only [isNilpotent_monomial_iff] using h i)

Result:
no goals

Proof state:
case refine_2
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
i : ℕ
⊢ IsNilpotent ((p + C r).coeff i)

Tactic:
have hr : IsNilpotent (C r) := by
  obtain ⟨k, hk⟩ := hpr
  replace hp : eval 0 p = 0 := by rwa [coeff_zero_eq_aeval_zero] at hp₀
  refine isNilpotent_C_iff.mpr ⟨k, ?_⟩
  simpa [coeff_zero_eq_aeval_zero, hp] using congr_arg (fun q ↦ coeff q 0) hk

Result:
case refine_2
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
i : ℕ
hr : IsNilpotent (C r)
⊢ IsNilpotent ((p + C r).coeff i)

Proof state:
case refine_2.succ
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
hr : IsNilpotent (C r)
i : ℕ
⊢ IsNilpotent (p.coeff (i + 1))

Tactic:
apply hp

Result:
case refine_2.succ.a
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
hr : IsNilpotent (C r)
i : ℕ
⊢ IsNilpotent p

Proof state:
case refine_2
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
i : ℕ
hr : IsNilpotent (C r)
⊢ IsNilpotent ((p + C r).coeff i)

Tactic:
rcases i with - | i

Result:
case refine_2.zero
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
hr : IsNilpotent (C r)
⊢ IsNilpotent ((p + C r).coeff 0)

case refine_2.succ
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
hr : IsNilpotent (C r)
i : ℕ
⊢ IsNilpotent ((p + C r).coeff (i + 1))

Proof state:
case refine_3.succ
R : Type u_1
inst✝ : CommRing R
P p : R[X]
x✝ : p ≠ 0
hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpX : IsNilpotent (p * X)
i : ℕ
⊢ IsNilpotent ((p * X).coeff (i + 1))

Tactic:
simpa using hnp (isNilpotent_mul_X_iff.mp hpX) i

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
P : R[X]
⊢ IsNilpotent 0 → ∀ (i : ℕ), IsNilpotent (coeff 0 i)

Tactic:
simp

Result:
no goals

Proof state:
case refine_2.zero
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (p + C r)
hr : IsNilpotent (C r)
⊢ IsNilpotent ((p + C r).coeff 0)

Tactic:
simpa [hp₀] using hr

Result:
no goals

Proof state:
case refine_3
R : Type u_1
inst✝ : CommRing R
P p : R[X]
x✝ : p ≠ 0
hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpX : IsNilpotent (p * X)
i : ℕ
⊢ IsNilpotent ((p * X).coeff i)

Tactic:
rcases i with - | i

Result:
case refine_3.zero
R : Type u_1
inst✝ : CommRing R
P p : R[X]
x✝ : p ≠ 0
hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpX : IsNilpotent (p * X)
⊢ IsNilpotent ((p * X).coeff 0)

case refine_3.succ
R : Type u_1
inst✝ : CommRing R
P p : R[X]
x✝ : p ≠ 0
hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpX : IsNilpotent (p * X)
i : ℕ
⊢ IsNilpotent ((p * X).coeff (i + 1))

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
i k : ℕ
hk : (p + C r) ^ k = 0
hp : eval 0 p = 0
⊢ IsNilpotent (C r)

Tactic:
refine isNilpotent_C_iff.mpr ⟨k, ?_⟩

Result:
case intro
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
i k : ℕ
hk : (p + C r) ^ k = 0
hp : eval 0 p = 0
⊢ r ^ k = 0

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
i k : ℕ
hk : (p + C r) ^ k = 0
⊢ IsNilpotent (C r)

Tactic:
replace hp : eval 0 p = 0 := by rwa [coeff_zero_eq_aeval_zero] at hp₀

Result:
case intro
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
i k : ℕ
hk : (p + C r) ^ k = 0
hp : eval 0 p = 0
⊢ IsNilpotent (C r)

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
i k : ℕ
hk : (p + C r) ^ k = 0
hp : eval 0 p = 0
⊢ r ^ k = 0

Tactic:
simpa [coeff_zero_eq_aeval_zero, hp] using congr_arg (fun q ↦ coeff q 0) hk

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
i k : ℕ
hk : (p + C r) ^ k = 0
⊢ eval 0 p = 0

Tactic:
rwa [coeff_zero_eq_aeval_zero] at hp₀

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
x✝ : i ∈ P.support
⊢ IsNilpotent ((fun n a => (monomial n) a) i (P.coeff i))

Tactic:
simpa only [isNilpotent_monomial_iff] using h i

Result:
no goals

Proof state:
case refine_1
R : Type u_1
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
⊢ IsNilpotent P

Tactic:
rw [← sum_monomial_eq P]

Result:
case refine_1
R : Type u_1
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
⊢ IsNilpotent (P.sum fun n a => (monomial n) a)