[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (↑C r * X ^ n)
[PROOFSTEP]
refine' Commute.isNilpotent_mul_left (commute_X_pow _ _).symm _
[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (↑C r)
[PROOFSTEP]
obtain ⟨m, hm⟩ := hnil
[GOAL]
case intro
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
n m : ℕ
hm : r ^ m = 0
⊢ IsNilpotent (↑C r)
[PROOFSTEP]
refine' ⟨m, _⟩
[GOAL]
case intro
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
n m : ℕ
hm : r ^ m = 0
⊢ ↑C r ^ m = 0
[PROOFSTEP]
rw [← C_pow, hm, C_0]
[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (X ^ n * ↑C r)
[PROOFSTEP]
rw [commute_X_pow]
[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (↑C r * X ^ n)
[PROOFSTEP]
exact isNilpotent_C_mul_pow_X_of_isNilpotent n hnil
[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
n k : ℕ
⊢ ↑(monomial n) r ^ k = 0 ↔ r ^ k = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
k : ℕ
⊢ ↑C r ^ k = 0 ↔ r ^ k = 0
[PROOFSTEP]
simpa only [← C_pow] using C_eq_zero
[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent (X * P) ↔ IsNilpotent P
[PROOFSTEP]
refine' ⟨fun h ↦ _, _⟩
[GOAL]
case refine'_1
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
h : IsNilpotent (X * P)
⊢ IsNilpotent P
[PROOFSTEP]
rwa [Commute.isNilpotent_mul_right_iff (commute_X P) (by simp)] at h 
[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
h : IsNilpotent (X * P)
⊢ X ∈ nonZeroDivisorsRight R[X]
[PROOFSTEP]
simp
[GOAL]
case refine'_2
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent P → IsNilpotent (X * P)
[PROOFSTEP]
rintro ⟨k, hk⟩
[GOAL]
case refine'_2.intro
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
k : ℕ
hk : P ^ k = 0
⊢ IsNilpotent (X * P)
[PROOFSTEP]
exact ⟨k, by simp [(commute_X P).mul_pow, hk]⟩
[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
k : ℕ
hk : P ^ k = 0
⊢ (X * P) ^ k = 0
[PROOFSTEP]
simp [(commute_X P).mul_pow, hk]
[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent (P * X) ↔ IsNilpotent P
[PROOFSTEP]
rw [← commute_X P]
[GOAL]
R : Type u_1
r : R
inst✝ : Semiring R
P : R[X]
⊢ IsNilpotent (X * P) ↔ IsNilpotent P
[PROOFSTEP]
exact isNilpotent_X_mul_iff
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ IsNilpotent P ↔ ∀ (i : ℕ), IsNilpotent (coeff P i)
[PROOFSTEP]
refine' ⟨P.recOnHorner (by simp) (fun p r hp₀ _ hp hpr i ↦ _) (fun p _ hnp hpX i ↦ _), fun h ↦ _⟩
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ IsNilpotent 0 → ∀ (i : ℕ), IsNilpotent (coeff 0 i)
[PROOFSTEP]
simp
[GOAL]
case refine'_1
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (coeff P i)
⊢ IsNilpotent P
[PROOFSTEP]
rw [← sum_monomial_eq P]
[GOAL]
case refine'_1
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (coeff P i)
⊢ IsNilpotent (sum P fun n a => ↑(monomial n) a)
[PROOFSTEP]
exact isNilpotent_sum (fun i _ ↦ by simpa only [isNilpotent_monomial_iff] using h i)
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (coeff P i)
i : ℕ
x✝ : i ∈ support P
⊢ IsNilpotent ((fun n a => ↑(monomial n) a) i (coeff P i))
[PROOFSTEP]
simpa only [isNilpotent_monomial_iff] using h i
[GOAL]
case refine'_2
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpr : IsNilpotent (p + ↑C r)
i : ℕ
⊢ IsNilpotent (coeff (p + ↑C r) i)
[PROOFSTEP]
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
[GOAL]
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpr : IsNilpotent (p + ↑C r)
i : ℕ
⊢ IsNilpotent (↑C r)
[PROOFSTEP]
obtain ⟨k, hk⟩ := hpr
[GOAL]
case intro
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
i k : ℕ
hk : (p + ↑C r) ^ k = 0
⊢ IsNilpotent (↑C r)
[PROOFSTEP]
replace hp : eval 0 p = 0 := by rwa [coeff_zero_eq_aeval_zero] at hp₀ 
[GOAL]
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
i k : ℕ
hk : (p + ↑C r) ^ k = 0
⊢ eval 0 p = 0
[PROOFSTEP]
rwa [coeff_zero_eq_aeval_zero] at hp₀ 
[GOAL]
case intro
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
i k : ℕ
hk : (p + ↑C r) ^ k = 0
hp : eval 0 p = 0
⊢ IsNilpotent (↑C r)
[PROOFSTEP]
refine' isNilpotent_C_iff.mpr ⟨k, _⟩
[GOAL]
case intro
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
i k : ℕ
hk : (p + ↑C r) ^ k = 0
hp : eval 0 p = 0
⊢ r ^ k = 0
[PROOFSTEP]
simpa [coeff_zero_eq_aeval_zero, hp] using congr_arg (fun q ↦ coeff q 0) hk
[GOAL]
case refine'_2
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpr : IsNilpotent (p + ↑C r)
i : ℕ
hr : IsNilpotent (↑C r)
⊢ IsNilpotent (coeff (p + ↑C r) i)
[PROOFSTEP]
cases' i with i
[GOAL]
case refine'_2.zero
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpr : IsNilpotent (p + ↑C r)
hr : IsNilpotent (↑C r)
⊢ IsNilpotent (coeff (p + ↑C r) Nat.zero)
case refine'_2.succ
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpr : IsNilpotent (p + ↑C r)
hr : IsNilpotent (↑C r)
i : ℕ
⊢ IsNilpotent (coeff (p + ↑C r) (Nat.succ i))
[PROOFSTEP]
simpa [hp₀] using hr
[GOAL]
case refine'_2.succ
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpr : IsNilpotent (p + ↑C r)
hr : IsNilpotent (↑C r)
i : ℕ
⊢ IsNilpotent (coeff (p + ↑C r) (Nat.succ i))
[PROOFSTEP]
simp only [coeff_add, coeff_C_succ, add_zero]
[GOAL]
case refine'_2.succ
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpr : IsNilpotent (p + ↑C r)
hr : IsNilpotent (↑C r)
i : ℕ
⊢ IsNilpotent (coeff p (Nat.succ i))
[PROOFSTEP]
apply hp
[GOAL]
case refine'_2.succ.a
R : Type u_1
r✝ : R
inst✝ : CommRing R
P p : R[X]
r : R
hp₀ : coeff p 0 = 0
x✝ : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpr : IsNilpotent (p + ↑C r)
hr : IsNilpotent (↑C r)
i : ℕ
⊢ IsNilpotent p
[PROOFSTEP]
simpa using Commute.isNilpotent_sub (Commute.all _ _) hpr hr
[GOAL]
case refine'_3
R : Type u_1
r : R
inst✝ : CommRing R
P p : R[X]
x✝ : p ≠ 0
hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpX : IsNilpotent (p * X)
i : ℕ
⊢ IsNilpotent (coeff (p * X) i)
[PROOFSTEP]
cases' i with i
[GOAL]
case refine'_3.zero
R : Type u_1
r : R
inst✝ : CommRing R
P p : R[X]
x✝ : p ≠ 0
hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpX : IsNilpotent (p * X)
⊢ IsNilpotent (coeff (p * X) Nat.zero)
case refine'_3.succ
R : Type u_1
r : R
inst✝ : CommRing R
P p : R[X]
x✝ : p ≠ 0
hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpX : IsNilpotent (p * X)
i : ℕ
⊢ IsNilpotent (coeff (p * X) (Nat.succ i))
[PROOFSTEP]
simp
[GOAL]
case refine'_3.succ
R : Type u_1
r : R
inst✝ : CommRing R
P p : R[X]
x✝ : p ≠ 0
hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (coeff p i)
hpX : IsNilpotent (p * X)
i : ℕ
⊢ IsNilpotent (coeff (p * X) (Nat.succ i))
[PROOFSTEP]
simpa using hnp (isNilpotent_mul_X_iff.mp hpX) i
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ IsNilpotent (reverse P) ↔ IsNilpotent P
[PROOFSTEP]
simp only [Polynomial.isNilpotent_iff, coeff_reverse]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ (∀ (i : ℕ), IsNilpotent (coeff P (↑(revAt (natDegree P)) i))) ↔ ∀ (i : ℕ), IsNilpotent (coeff P i)
[PROOFSTEP]
refine' ⟨fun h i ↦ _, fun h i ↦ _⟩
[GOAL]
case refine'_1
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (coeff P (↑(revAt (natDegree P)) i))
i : ℕ
⊢ IsNilpotent (coeff P i)
[PROOFSTEP]
cases' le_or_lt i P.natDegree with hi hi
[GOAL]
case refine'_2
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (coeff P i)
i : ℕ
⊢ IsNilpotent (coeff P (↑(revAt (natDegree P)) i))
[PROOFSTEP]
cases' le_or_lt i P.natDegree with hi hi
[GOAL]
case refine'_1.inl
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (coeff P (↑(revAt (natDegree P)) i))
i : ℕ
hi : i ≤ natDegree P
⊢ IsNilpotent (coeff P i)
[PROOFSTEP]
simpa [tsub_tsub_cancel_of_le hi] using h (P.natDegree - i)
[GOAL]
case refine'_1.inr
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (coeff P (↑(revAt (natDegree P)) i))
i : ℕ
hi : natDegree P < i
⊢ IsNilpotent (coeff P i)
[PROOFSTEP]
simp [coeff_eq_zero_of_natDegree_lt hi]
[GOAL]
case refine'_2.inl
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (coeff P i)
i : ℕ
hi : i ≤ natDegree P
⊢ IsNilpotent (coeff P (↑(revAt (natDegree P)) i))
[PROOFSTEP]
simpa only [hi, revAt_le] using h (P.natDegree - i)
[GOAL]
case refine'_2.inr
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (coeff P i)
i : ℕ
hi : natDegree P < i
⊢ IsNilpotent (coeff P (↑(revAt (natDegree P)) i))
[PROOFSTEP]
simpa only [revAt_eq_self_of_lt hi] using h i
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
⊢ IsUnit P
[PROOFSTEP]
induction' h : P.natDegree using Nat.strong_induction_on with k hind generalizing P
[GOAL]
case h
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
⊢ IsUnit P
[PROOFSTEP]
by_cases hdeg : P.natDegree = 0
[GOAL]
case pos
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : natDegree P = 0
⊢ IsUnit P
case neg
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
⊢ IsUnit P
[PROOFSTEP]
{ rw [eq_C_of_natDegree_eq_zero hdeg]
  exact hunit.map C
}
[GOAL]
case pos
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : natDegree P = 0
⊢ IsUnit P
[PROOFSTEP]
rw [eq_C_of_natDegree_eq_zero hdeg]
[GOAL]
case pos
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : natDegree P = 0
⊢ IsUnit (↑C (coeff P 0))
[PROOFSTEP]
exact hunit.map C
[GOAL]
case neg
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
⊢ IsUnit P
[PROOFSTEP]
set P₁ := P.eraseLead with hP₁
[GOAL]
case neg
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
⊢ IsUnit P
[PROOFSTEP]
suffices IsUnit P₁ by
  rw [← eraseLead_add_monomial_natDegree_leadingCoeff P, ← C_mul_X_pow_eq_monomial]
  obtain ⟨Q, hQ⟩ := this
  rw [← hP₁, ← hQ]
  refine'
    Commute.IsNilpotent.add_isUnit (isNilpotent_C_mul_pow_X_of_isNilpotent _ (hnil _ hdeg))
      ((Commute.all _ _).mul_left (Commute.all _ _))
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
this : IsUnit P₁
⊢ IsUnit P
[PROOFSTEP]
rw [← eraseLead_add_monomial_natDegree_leadingCoeff P, ← C_mul_X_pow_eq_monomial]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
this : IsUnit P₁
⊢ IsUnit (eraseLead P + ↑C (leadingCoeff P) * X ^ natDegree P)
[PROOFSTEP]
obtain ⟨Q, hQ⟩ := this
[GOAL]
case intro
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
Q : R[X]ˣ
hQ : ↑Q = P₁
⊢ IsUnit (eraseLead P + ↑C (leadingCoeff P) * X ^ natDegree P)
[PROOFSTEP]
rw [← hP₁, ← hQ]
[GOAL]
case intro
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
Q : R[X]ˣ
hQ : ↑Q = P₁
⊢ IsUnit (↑Q + ↑C (leadingCoeff P) * X ^ natDegree P)
[PROOFSTEP]
refine'
  Commute.IsNilpotent.add_isUnit (isNilpotent_C_mul_pow_X_of_isNilpotent _ (hnil _ hdeg))
    ((Commute.all _ _).mul_left (Commute.all _ _))
[GOAL]
case neg
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
⊢ IsUnit P₁
[PROOFSTEP]
have hdeg₂ := lt_of_le_of_lt P.eraseLead_natDegree_le (Nat.sub_lt (Nat.pos_of_ne_zero hdeg) zero_lt_one)
[GOAL]
case neg
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
hdeg₂ : natDegree (eraseLead P) < natDegree P
⊢ IsUnit P₁
[PROOFSTEP]
refine' hind P₁.natDegree _ _ (fun i hi => _) rfl
[GOAL]
case neg.refine'_1
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
hdeg₂ : natDegree (eraseLead P) < natDegree P
⊢ natDegree P₁ < k
[PROOFSTEP]
simp_rw [← h, hdeg₂]
[GOAL]
case neg.refine'_2
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
hdeg₂ : natDegree (eraseLead P) < natDegree P
⊢ IsUnit (coeff P₁ 0)
[PROOFSTEP]
simp_rw [eraseLead_coeff_of_ne _ (Ne.symm hdeg), hunit]
[GOAL]
case neg.refine'_3
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
hdeg₂ : natDegree (eraseLead P) < natDegree P
i : ℕ
hi : i ≠ 0
⊢ IsNilpotent (coeff P₁ i)
[PROOFSTEP]
by_cases H : i ≤ P₁.natDegree
[GOAL]
case pos
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
hdeg₂ : natDegree (eraseLead P) < natDegree P
i : ℕ
hi : i ≠ 0
H : i ≤ natDegree P₁
⊢ IsNilpotent (coeff P₁ i)
case neg
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
hdeg₂ : natDegree (eraseLead P) < natDegree P
i : ℕ
hi : i ≠ 0
H : ¬i ≤ natDegree P₁
⊢ IsNilpotent (coeff P₁ i)
[PROOFSTEP]
simp_rw [eraseLead_coeff_of_ne _ (ne_of_lt (lt_of_le_of_lt H hdeg₂)), hnil i hi]
[GOAL]
case neg
R : Type u_1
r : R
inst✝ : CommRing R
P✝ : R[X]
hunit✝ : IsUnit (coeff P✝ 0)
hnil✝ : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P✝ i)
x✝ : ℕ
h✝ : natDegree P✝ = x✝
k : ℕ
hind :
  ∀ (m : ℕ),
    m < k → ∀ {P : R[X]}, IsUnit (coeff P 0) → (∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)) → natDegree P = m → IsUnit P
P : R[X]
hunit : IsUnit (coeff P 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
h : natDegree P = k
hdeg : ¬natDegree P = 0
P₁ : R[X] := eraseLead P
hP₁ : P₁ = eraseLead P
hdeg₂ : natDegree (eraseLead P) < natDegree P
i : ℕ
hi : i ≠ 0
H : ¬i ≤ natDegree P₁
⊢ IsNilpotent (coeff P₁ i)
[PROOFSTEP]
simp_rw [coeff_eq_zero_of_natDegree_lt (lt_of_not_ge H), IsNilpotent.zero]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
⊢ IsUnit (coeff P 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
[PROOFSTEP]
obtain ⟨Q, hQ⟩ := IsUnit.exists_right_inv hunit
[GOAL]
case intro
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
⊢ IsUnit (coeff P 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
[PROOFSTEP]
constructor
[GOAL]
case intro.left
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
⊢ IsUnit (coeff P 0)
[PROOFSTEP]
refine' isUnit_of_mul_eq_one _ (Q.coeff 0) _
[GOAL]
case intro.left
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
⊢ coeff P 0 * coeff Q 0 = 1
[PROOFSTEP]
have h := (mul_coeff_zero P Q).symm
[GOAL]
case intro.left
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
h : coeff P 0 * coeff Q 0 = coeff (P * Q) 0
⊢ coeff P 0 * coeff Q 0 = 1
[PROOFSTEP]
rwa [hQ, coeff_one_zero] at h 
[GOAL]
case intro.right
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
⊢ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (coeff P i)
[PROOFSTEP]
intros n hn
[GOAL]
case intro.right
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
⊢ IsNilpotent (coeff P n)
[PROOFSTEP]
rw [nilpotent_iff_mem_prime]
[GOAL]
case intro.right
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
⊢ ∀ (J : Ideal R), Ideal.IsPrime J → coeff P n ∈ J
[PROOFSTEP]
intros I hI
[GOAL]
case intro.right
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : Ideal.IsPrime I
⊢ coeff P n ∈ I
[PROOFSTEP]
let f := mapRingHom (Ideal.Quotient.mk I)
[GOAL]
case intro.right
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : Ideal.IsPrime I
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
⊢ coeff P n ∈ I
[PROOFSTEP]
have hPQ : degree (f P) = 0 ∧ degree (f Q) = 0 := by
  rw [← Nat.WithBot.add_eq_zero_iff, ← degree_mul, ← _root_.map_mul, hQ, map_one, degree_one]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : Ideal.IsPrime I
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
⊢ degree (↑f P) = 0 ∧ degree (↑f Q) = 0
[PROOFSTEP]
rw [← Nat.WithBot.add_eq_zero_iff, ← degree_mul, ← _root_.map_mul, hQ, map_one, degree_one]
[GOAL]
case intro.right
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : Ideal.IsPrime I
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
hPQ : degree (↑f P) = 0 ∧ degree (↑f Q) = 0
⊢ coeff P n ∈ I
[PROOFSTEP]
have hcoeff : (f P).coeff n = 0 := by
  refine' coeff_eq_zero_of_degree_lt _
  rw [hPQ.1]
  exact (@WithBot.coe_pos _ _ _ n).2 (Ne.bot_lt hn)
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : Ideal.IsPrime I
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
hPQ : degree (↑f P) = 0 ∧ degree (↑f Q) = 0
⊢ coeff (↑f P) n = 0
[PROOFSTEP]
refine' coeff_eq_zero_of_degree_lt _
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : Ideal.IsPrime I
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
hPQ : degree (↑f P) = 0 ∧ degree (↑f Q) = 0
⊢ degree (↑f P) < ↑n
[PROOFSTEP]
rw [hPQ.1]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : Ideal.IsPrime I
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
hPQ : degree (↑f P) = 0 ∧ degree (↑f Q) = 0
⊢ 0 < ↑n
[PROOFSTEP]
exact (@WithBot.coe_pos _ _ _ n).2 (Ne.bot_lt hn)
[GOAL]
case intro.right
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : Ideal.IsPrime I
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
hPQ : degree (↑f P) = 0 ∧ degree (↑f Q) = 0
hcoeff : coeff (↑f P) n = 0
⊢ coeff P n ∈ I
[PROOFSTEP]
rw [coe_mapRingHom, coeff_map, ← RingHom.mem_ker, Ideal.mk_ker] at hcoeff 
[GOAL]
case intro.right
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : Ideal.IsPrime I
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
hPQ : degree (↑f P) = 0 ∧ degree (↑f Q) = 0
hcoeff : coeff P n ∈ I
⊢ coeff P n ∈ I
[PROOFSTEP]
exact hcoeff
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ IsUnit (↑C r + X * P) ↔ IsUnit r ∧ IsNilpotent P
[PROOFSTEP]
have : ∀ i, coeff (C r + X * P) (i + 1) = coeff P i := by simp
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ ∀ (i : ℕ), coeff (↑C r + X * P) (i + 1) = coeff P i
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
this : ∀ (i : ℕ), coeff (↑C r + X * P) (i + 1) = coeff P i
⊢ IsUnit (↑C r + X * P) ↔ IsUnit r ∧ IsNilpotent P
[PROOFSTEP]
simp_rw [isUnit_iff_coeff_isUnit_isNilpotent, Nat.forall_ne_zero_iff, this]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
this : ∀ (i : ℕ), coeff (↑C r + X * P) (i + 1) = coeff P i
⊢ (IsUnit (coeff (↑C r + X * P) 0) ∧ ∀ (i : ℕ), IsNilpotent (coeff P i)) ↔ IsUnit r ∧ IsNilpotent P
[PROOFSTEP]
simp only [coeff_add, coeff_C_zero, mul_coeff_zero, coeff_X_zero, zero_mul, add_zero, and_congr_right_iff, ←
  Polynomial.isNilpotent_iff]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ IsUnit P ↔ IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)
[PROOFSTEP]
suffices : P = C (eval 0 P) + X * (P /ₘ X)
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
this : P = ↑C (eval 0 P) + X * (P /ₘ X)
⊢ IsUnit P ↔ IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)
[PROOFSTEP]
conv_lhs => rw [this]; simp
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
this : P = ↑C (eval 0 P) + X * (P /ₘ X)
| IsUnit P
[PROOFSTEP]
rw [this]; simp
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
this : P = ↑C (eval 0 P) + X * (P /ₘ X)
| IsUnit P
[PROOFSTEP]
rw [this]; simp
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
this : P = ↑C (eval 0 P) + X * (P /ₘ X)
| IsUnit P
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
this : P = ↑C (eval 0 P) + X * (P /ₘ X)
| IsUnit (↑C (eval 0 P) + X * (P /ₘ X))
[PROOFSTEP]
simp
[GOAL]
case this
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ P = ↑C (eval 0 P) + X * (P /ₘ X)
[PROOFSTEP]
conv_lhs => rw [← modByMonic_add_div P monic_X]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
| P
[PROOFSTEP]
rw [← modByMonic_add_div P monic_X]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
| P
[PROOFSTEP]
rw [← modByMonic_add_div P monic_X]
[GOAL]
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
| P
[PROOFSTEP]
rw [← modByMonic_add_div P monic_X]
[GOAL]
case this
R : Type u_1
r : R
inst✝ : CommRing R
P : R[X]
⊢ P %ₘ X + X * (P /ₘ X) = ↑C (eval 0 P) + X * (P /ₘ X)
[PROOFSTEP]
simp [modByMonic_X]
