awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
r : R
inst : Semiring R
n m : ℕ
hm : r ^ m = 0
⊢ IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])

Tactic:
⟨m, ?_⟩

Premises used: Exists.intro, IsNilpotent
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
r : R
inst : Semiring R
n m : ℕ
hm : r ^ m = 0
refine : HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) m = 0
⊢ IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])

Tactic:
refine ⟨m, ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
r : R
inst : Semiring R
n m : ℕ
hm : r ^ m = 0
rw : Eq (α := R[X]) ((C : (a : R) → R[X]) (r ^ m) : R[X]) (0 : R[X])
rw₁ : Eq.{u_1 + 1} (α := R[X]) ((C : (a : R) → R[X]) 0) 0
rw₂ rw₃ : Eq.{u_1 + 1} (α := R[X]) 0 0
⊢ HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) m = 0

Tactic:
rw [← C_pow, hm, C_0]

Premises used: Polynomial.C_0, Polynomial.C_pow
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
r : R
inst : Semiring R
n : ℕ
hnil : IsNilpotent r
rw : IsNilpotent (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ IsNilpotent (HMul.hMul (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X]))

Tactic:
rw [commute_X_pow]

Premises used: Polynomial.commute_X_pow
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
r : R
inst : Semiring R
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))

Tactic:
isNilpotent_C_mul_pow_X_of_isNilpotent n hnil

Premises used: Polynomial.isNilpotent_C_mul_pow_X_of_isNilpotent
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
r : R
inst : Semiring R
n : ℕ
hnil : IsNilpotent r
⊢ IsNilpotent (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))

Tactic:
exact isNilpotent_C_mul_pow_X_of_isNilpotent n hnil

Premises used: Polynomial.isNilpotent_C_mul_pow_X_of_isNilpotent
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
r : R
inst : Semiring R
n k : ℕ
⊢ HPow.hPow (α := R[X]) ((monomial n : (a : R) → R[X]) r : R[X]) k = 0 ↔ r ^ k = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
r : R
inst : Semiring R
k : ℕ
⊢ HPow.hPow (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) k = 0 ↔ r ^ k = 0

Tactic:
simpa only [← C_pow] using C_eq_zero

Premises used: Polynomial.C_eq_zero, Polynomial.C_pow
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
⊢ IsNilpotent (X * P) ↔ IsNilpotent P

Tactic:
⟨fun h ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
refine_1 : ∀ (h : IsNilpotent (X * P)), IsNilpotent P
refine_2 : IsNilpotent P → IsNilpotent (X * P)
⊢ IsNilpotent (X * P) ↔ IsNilpotent P

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : IsNilpotent (X * P)
⊢ Membership.mem (γ := Submonoid R[X]) (nonZeroDivisorsLeft R[X]) X

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
h : IsNilpotent (X * P)
refine_1 refine_1₁ refine_1₂ refine_1₃ : ∀ (h : IsNilpotent P), IsNilpotent P
⊢ IsNilpotent P

Tactic:
rwa [Commute.isNilpotent_mul_left_iff (commute_X P) (by simp)] at h

Premises used: Commute.isNilpotent_mul_left_iff, Polynomial.commute_X
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
k : ℕ
hk : P ^ k = 0
⊢ (X * P) ^ k = 0

Tactic:
simp [(commute_X P).mul_pow, hk]

Premises used: Polynomial.commute_X, Commute.mul_pow
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
k : ℕ
hk : P ^ k = 0
⊢ IsNilpotent (X * P)

Tactic:
exact ⟨k, by simp [(commute_X P).mul_pow, hk]⟩
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
rw : IsNilpotent (X * P) ↔ IsNilpotent P
⊢ IsNilpotent (P * X) ↔ IsNilpotent P

Tactic:
rw [← commute_X P]

Premises used: Polynomial.commute_X
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
⊢ IsNilpotent (X * P) ↔ IsNilpotent P

Tactic:
isNilpotent_X_mul_iff

Premises used: Polynomial.isNilpotent_X_mul_iff
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : Semiring R
P : R[X]
⊢ IsNilpotent (X * P) ↔ IsNilpotent P

Tactic:
exact isNilpotent_X_mul_iff

Premises used: Polynomial.isNilpotent_X_mul_iff
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
⊢ IsNilpotent.{u_1} (R := R[X]) 0 → ∀ (i : ℕ), IsNilpotent.{u_1} (R := R) (coeff 0 i)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
refine_1 : ∀ (h : ∀ (i : ℕ), IsNilpotent (P.coeff i)), IsNilpotent P
refine_2 :
  ∀ (p : R[X]) (r : R) (hp₀ : p.coeff 0 = 0),
    r ≠ 0 →
      ∀ (hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i))
        (hpr : IsNilpotent (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]))) (i : ℕ),
        IsNilpotent ((HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X])).coeff i)
refine_3 :
  ∀ (p : R[X]),
    p ≠ 0 →
      ∀ (hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)) (hpX : IsNilpotent (p * X)) (i : ℕ),
        IsNilpotent ((p * X).coeff i)
⊢ 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 ↦ ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
refine_1 : IsNilpotent (R := R[X]) (P.sum fun (n : ℕ) (a : R) ↦ (monomial n : (a : R) → R[X]) a)
⊢ IsNilpotent P

Tactic:
rw [← sum_monomial_eq P]

Premises used: Polynomial.sum_monomial_eq
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
h_1 : i ∈ P.support
⊢ IsNilpotent.{u_1} (R := R[X]) ((fun (n : ℕ) (a : R) ↦ ((monomial n : (a : R) → R[X]) a : R[X])) i (P.coeff i))

Tactic:
simpa only [isNilpotent_monomial_iff] using h i

Premises used: Polynomial.isNilpotent_monomial_iff
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
⊢ IsNilpotent (R := R[X]) (P.sum fun (n : ℕ) (a : R) ↦ (monomial n : (a : R) → R[X]) a)

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

Premises used: isNilpotent_sum
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
h : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]))
i : ℕ
obtain :
  ∀ (k : ℕ) (hk : HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]) ^ k = 0),
    IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])
⊢ IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])

Tactic:
obtain ⟨k, hk⟩ := hpr
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
h : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
i k : ℕ
hk : HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]) ^ k = 0
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hp₀ : Eq (α := R) ((aeval 0 : (a : R[X]) → R) p : R) (0 : R)),
    r ≠ 0 →
      ∀ (hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)) (i k : ℕ)
        (hk : HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]) ^ k = 0), eval 0 p = 0
⊢ eval 0 p = 0

Tactic:
rwa [coeff_zero_eq_aeval_zero] at hp₀

Premises used: Polynomial.coeff_zero_eq_aeval_zero
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
h : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
i k : ℕ
hk : HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]) ^ k = 0
⊢ eval 0 p = 0

Tactic:
replace hp : eval 0 p = 0 := by rwa [coeff_zero_eq_aeval_zero] at hp₀
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
h : r ≠ 0
i k : ℕ
hk : HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]) ^ k = 0
hp : eval 0 p = 0
⊢ IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])

Tactic:
isNilpotent_C_iff.mpr ⟨k, ?_⟩

Premises used: Iff.mpr, Polynomial.isNilpotent_C_iff, Exists.intro
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
h : r ≠ 0
i k : ℕ
hk : HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]) ^ k = 0
hp : eval 0 p = 0
refine : r ^ k = 0
⊢ IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])

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

Premises used: Iff.mpr, Polynomial.isNilpotent_C_iff, Exists.intro
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
h : r ≠ 0
i k : ℕ
hk : HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]) ^ 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

Premises used: Polynomial.coeff, congr_arg, Polynomial.coeff_zero_eq_aeval_zero, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
h : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]))
i : ℕ
⊢ IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])

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
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
h : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]))
i : ℕ
hr : IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])
refine_2 : IsNilpotent ((HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X])).coeff 0)
refine_2₁ : ∀ (i : ℕ), IsNilpotent ((HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X])).coeff (i + 1))
⊢ IsNilpotent ((HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X])).coeff i)

Tactic:
rcases i with - | i
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
h : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]))
hr : IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])
⊢ IsNilpotent ((HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X])).coeff 0)

Tactic:
simpa [hp₀] using hr
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
h : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]))
hr : IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])
i : ℕ
refine_2 : IsNilpotent (p.coeff (i + 1))
⊢ IsNilpotent ((HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X])).coeff (i + 1))

Tactic:
simp only [coeff_add, coeff_C_succ, add_zero]

Premises used: Polynomial.coeff_add, Polynomial.coeff_C_succ, add_zero
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
h : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]))
hr : IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])
i : ℕ
refine_2 : IsNilpotent p
⊢ IsNilpotent (p.coeff (i + 1))

Tactic:
apply hp
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P p : R[X]
r : R
hp₀ : p.coeff 0 = 0
h : r ≠ 0
hp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpr : IsNilpotent (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X]))
hr : IsNilpotent (R := R[X]) ((C : (a : R) → R[X]) r : R[X])
i : ℕ
⊢ IsNilpotent p

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

Premises used: Commute.isNilpotent_sub
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P p : R[X]
h : p ≠ 0
hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpX : IsNilpotent (p * X)
i : ℕ
refine_3 : IsNilpotent ((p * X).coeff 0)
refine_3₁ : ∀ (i : ℕ), IsNilpotent ((p * X).coeff (i + 1))
⊢ IsNilpotent ((p * X).coeff i)

Tactic:
rcases i with - | i
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P p : R[X]
h : p ≠ 0
hnp : IsNilpotent p → ∀ (i : ℕ), IsNilpotent (p.coeff i)
hpX : IsNilpotent (p * X)
⊢ IsNilpotent ((p * X).coeff 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P p : R[X]
h : 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

Premises used: Iff.mp, Polynomial.isNilpotent_mul_X_iff
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
simp : (∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)) ↔ ∀ (i : ℕ), IsNilpotent (P.coeff i)
⊢ IsNilpotent (reflect N P) ↔ IsNilpotent P

Tactic:
simp only [Polynomial.isNilpotent_iff]

Premises used: Polynomial.isNilpotent_iff
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
⊢ (∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)) ↔ ∀ (i : ℕ), IsNilpotent (P.coeff i)

Tactic:
⟨fun h i ↦ ?_, fun h i ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
refine_1 : ∀ (h : ∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)) (i : ℕ), IsNilpotent (P.coeff i)
refine_2 : ∀ (h : ∀ (i : ℕ), IsNilpotent (P.coeff i)) (i : ℕ), IsNilpotent ((reflect N P).coeff i)
⊢ (∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)) ↔ ∀ (i : ℕ), IsNilpotent (P.coeff i)

Tactic:
refine ⟨fun h i ↦ ?_, fun h i ↦ ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)
i : ℕ
refine_1 : ∀ (hi : i ≤ N), IsNilpotent (P.coeff i)
refine_1₁ : ∀ (hi : N < i), IsNilpotent (P.coeff i)
⊢ IsNilpotent (P.coeff i)

Tactic:
rcases le_or_gt i N with hi | hi

Premises used: le_or_gt
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
refine_2 : ∀ (hi : i ≤ N), IsNilpotent ((reflect N P).coeff i)
refine_2₁ : ∀ (hi : N < i), IsNilpotent ((reflect N P).coeff i)
⊢ IsNilpotent ((reflect N P).coeff i)

Tactic:
rcases le_or_gt i N with hi | hi

Premises used: le_or_gt
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)
i : ℕ
hi : i ≤ N
⊢ IsNilpotent (P.coeff i)

Tactic:
simpa [tsub_tsub_cancel_of_le hi] using h (N - i)

Premises used: HSub.hSub, tsub_tsub_cancel_of_le
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)
i : ℕ
hi : N < i
⊢ IsNilpotent (P.coeff i)

Tactic:
simp [coeff_eq_zero_of_natDegree_lt <| lt_of_le_of_lt hN hi]

Premises used: lt_of_le_of_lt, Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
hi : i ≤ N
⊢ IsNilpotent ((reflect N P).coeff i)

Tactic:
simpa [hi, revAt_le] using h (N - i)

Premises used: HSub.hSub, Polynomial.revAt_le
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
hi : N < i
⊢ IsNilpotent ((reflect N P).coeff i)

Tactic:
simpa [revAt_eq_self_of_lt hi] using h i

Premises used: Polynomial.revAt_eq_self_of_lt
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
⊢ IsNilpotent P.reverse ↔ IsNilpotent P

Tactic:
isNilpotent_reflect_iff (le_refl _)

Premises used: le_refl, Polynomial.isNilpotent_reflect_iff, Polynomial.reverse
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h :
  ∀ (k : ℕ)
    (hind :
      ∀ m < k,
        ∀ {P : R[X]} (hunit : IsUnit (P.coeff 0)) (hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i))
          (h : P.natDegree = m), IsUnit P)
    {P : R[X]} (hunit : IsUnit (P.coeff 0)) (hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) (h : P.natDegree = k),
    IsUnit P
⊢ IsUnit P

Tactic:
induction h : P.natDegree using Nat.strong_induction_on generalizing P with | _ k hind

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
hind :
  ∀ m < k,
    ∀ {P : R[X]} (hunit : IsUnit (P.coeff 0)) (hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) (h : P.natDegree = m),
      IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
pos : ∀ (hdeg : P.natDegree = 0), IsUnit P
neg : ∀ (hdeg : ¬P.natDegree = 0), IsUnit P
⊢ IsUnit P

Tactic:
by_cases hdeg : P.natDegree = 0

Premises used: Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
hind :
  ∀ m < k,
    ∀ {P : R[X]} (hunit : IsUnit (P.coeff 0)) (hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) (h : P.natDegree = m),
      IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
hdeg : P.natDegree = 0
pos : IsUnit (M := R[X]) ((C : (a : R) → R[X]) (P.coeff 0) : R[X])
⊢ IsUnit P

Tactic:
rw [eq_C_of_natDegree_eq_zero hdeg]

Premises used: Polynomial.eq_C_of_natDegree_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
hind :
  ∀ m < k,
    ∀ {P : R[X]} (hunit : IsUnit (P.coeff 0)) (hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) (h : P.natDegree = m),
      IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
hdeg : P.natDegree = 0
⊢ IsUnit (M := R[X]) ((C : (a : R) → R[X]) (P.coeff 0) : R[X])

Tactic:
hunit.map C

Premises used: Polynomial.C, IsUnit.map
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
hind :
  ∀ m < k,
    ∀ {P : R[X]} (hunit : IsUnit (P.coeff 0)) (hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) (h : P.natDegree = m),
      IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
hdeg : P.natDegree = 0
⊢ IsUnit (M := R[X]) ((C : (a : R) → R[X]) (P.coeff 0) : R[X])

Tactic:
exact hunit.map C

Premises used: Polynomial.C, IsUnit.map
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
hind :
  ∀ m < k,
    ∀ {P : R[X]} (hunit : IsUnit (P.coeff 0)) (hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) (h : P.natDegree = m),
      IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
hdeg : ¬P.natDegree = 0
⊢ let P₁ := P.eraseLead;
  P₁ = P.eraseLead

Tactic:
set P₁ := P.eraseLead with hP₁

Premises used: Polynomial.eraseLead
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
hind :
  ∀ m < k,
    ∀ {P : R[X]} (hunit : IsUnit (P.coeff 0)) (hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) (h : P.natDegree = m),
      IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
hdeg : ¬P.natDegree = 0
P₁ : R[X] := P.eraseLead
hP₁ : P₁ = P.eraseLead
this : IsUnit P₁
rw :
  IsUnit (P₁ + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) P.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X P.natDegree))
⊢ IsUnit P

Tactic:
rw [← eraseLead_add_monomial_natDegree_leadingCoeff P, ← C_mul_X_pow_eq_monomial, ← hP₁]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, Polynomial.eraseLead_add_monomial_natDegree_leadingCoeff
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
hind :
  ∀ m < k,
    ∀ {P : R[X]} (hunit : IsUnit (P.coeff 0)) (hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) (h : P.natDegree = m),
      IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
hdeg : ¬P.natDegree = 0
P₁ : R[X] := P.eraseLead
hP₁ : P₁ = P.eraseLead
this : IsUnit P₁
⊢ IsUnit (P₁ + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) P.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X P.natDegree))

Tactic:
IsNilpotent.isUnit_add_left_of_commute ?_ this (Commute.all _ _)

Premises used: IsNilpotent.isUnit_add_left_of_commute, Commute.all
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
hind :
  ∀ m < k,
    ∀ {P : R[X]} (hunit : IsUnit (P.coeff 0)) (hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) (h : P.natDegree = m),
      IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
hdeg : ¬P.natDegree = 0
P₁ : R[X] := P.eraseLead
hP₁ : P₁ = P.eraseLead
this : IsUnit P₁
refine :
  IsNilpotent (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) P.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X P.natDegree))
⊢ IsUnit (P₁ + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) P.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X P.natDegree))

Tactic:
refine IsNilpotent.isUnit_add_left_of_commute ?_ this (Commute.all _ _)

Premises used: IsNilpotent.isUnit_add_left_of_commute, Commute.all
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
hind :
  ∀ m < k,
    ∀ {P : R[X]} (hunit : IsUnit (P.coeff 0)) (hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) (h : P.natDegree = m),
      IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
hdeg : ¬P.natDegree = 0
P₁ : R[X] := P.eraseLead
hP₁ : P₁ = P.eraseLead
this : IsUnit P₁
⊢ IsNilpotent (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) P.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X P.natDegree))

Tactic:
isNilpotent_C_mul_pow_X_of_isNilpotent _ (hnil _ hdeg)

Premises used: Polynomial.isNilpotent_C_mul_pow_X_of_isNilpotent
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
k : ℕ
hind :
  ∀ m < k,
    ∀ {P : R[X]} (hunit : IsUnit (P.coeff 0)) (hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)) (h : P.natDegree = m),
      IsUnit P
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
h : P.natDegree = k
hdeg : ¬P.natDegree = 0
P₁ : R[X] := P.eraseLead
hP₁ : P₁ = P.eraseLead
this : IsUnit P₁
⊢ IsNilpotent (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) P.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X P.natDegree))

Tactic:
exact isNilpotent_C_mul_pow_X_of_isNilpotent _ (hnil _ hdeg)

Premises used: Polynomial.isNilpotent_C_mul_pow_X_of_isNilpotent