awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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])
⊢ IsNilpotent ((HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X])).coeff i)
have refine_2 : IsNilpotent ((HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X])).coeff 0)
Tactic: rcases i with - | i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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)
⊢ IsNilpotent ((HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X])).coeff i)
have refine_2₁ : ∀ (i : ℕ), IsNilpotent ((HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X])).coeff (i + 1))
Tactic: rcases i with - | i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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 ((HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) r : R[X])).coeff (i + 1))
have refine_2 : IsNilpotent (p.coeff (i + 1))
Tactic: simp only [coeff_add, coeff_C_succ, add_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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.coeff (i + 1))
have refine_2 : IsNilpotent p
Tactic: apply hp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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)
have refine_3 : IsNilpotent ((p * X).coeff 0)
Tactic: rcases i with - | i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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)
⊢ IsNilpotent ((p * X).coeff i)
have refine_3₁ : ∀ (i : ℕ), IsNilpotent ((p * X).coeff (i + 1))
Tactic: rcases i with - | i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
⊢ IsNilpotent (reflect N P) ↔ IsNilpotent P
have simp : (∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)) ↔ ∀ (i : ℕ), IsNilpotent (P.coeff i)
Tactic: simp only [Polynomial.isNilpotent_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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)
have refine_1 : ∀ (h : ∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)) (i : ℕ), IsNilpotent (P.coeff i)
Tactic: refine ⟨fun h i ↦ ?_, fun h i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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)
⊢ (∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)) ↔ ∀ (i : ℕ), IsNilpotent (P.coeff i)
have refine_2 : ∀ (h : ∀ (i : ℕ), IsNilpotent (P.coeff i)) (i : ℕ), IsNilpotent ((reflect N P).coeff i)
Tactic: refine ⟨fun h i ↦ ?_, fun h i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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 : ℕ
⊢ IsNilpotent (P.coeff i)
have refine_1 : ∀ (hi : i ≤ N), IsNilpotent (P.coeff i)
Tactic: rcases le_or_gt i N with hi | hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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)
⊢ IsNilpotent (P.coeff i)
have refine_1₁ : ∀ (hi : N < i), IsNilpotent (P.coeff i)
Tactic: rcases le_or_gt i N with hi | hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
⊢ IsNilpotent ((reflect N P).coeff i)
have refine_2 : ∀ (hi : i ≤ N), IsNilpotent ((reflect N P).coeff i)
Tactic: rcases le_or_gt i N with hi | hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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)
⊢ IsNilpotent ((reflect N P).coeff i)
have refine_2₁ : ∀ (hi : N < i), IsNilpotent ((reflect N P).coeff i)
Tactic: rcases le_or_gt i N with hi | hi
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
hunit : IsUnit (P.coeff 0)
hnil : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
⊢ IsUnit P
have 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
Tactic: induction h : P.natDegree using Nat.strong_induction_on generalizing P with | _ k hind
Cleared hypotheses: P, hunit, hnil
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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
⊢ IsUnit P
have pos : ∀ (hdeg : P.natDegree = 0), IsUnit P
Tactic: by_cases hdeg : P.natDegree = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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
⊢ IsUnit P
have neg : ∀ (hdeg : ¬P.natDegree = 0), IsUnit P
Tactic: by_cases hdeg : P.natDegree = 0
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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 P
have pos : IsUnit (M := R[X]) ((C : (a : R) → R[X]) (P.coeff 0) : R[X])
Tactic: rw [eq_C_of_natDegree_eq_zero hdeg]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (hypothesis)
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 P
have hP₁ : let P₁ := P.eraseLead;
P₁ = P.eraseLead
Tactic: set P₁ := P.eraseLead with hP₁
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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
have rw : IsUnit (P₁ + HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) P.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X P.natDegree))
Tactic: rw [← eraseLead_add_monomial_natDegree_leadingCoeff P, ← C_mul_X_pow_eq_monomial, ← hP₁]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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))
have refine : IsNilpotent (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 _ _)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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
⊢ IsUnit P
have neg : IsUnit P₁
Tactic: suffices IsUnit P₁ by
    rw [← eraseLead_add_monomial_natDegree_leadingCoeff P, ← C_mul_X_pow_eq_monomial, ← hP₁]
    refine IsNilpotent.isUnit_add_left_of_commute ?_ this (Commute.all _ _)
    exact isNilpotent_C_mul_pow_X_of_isNilpotent _ (hnil _ hdeg)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (hypothesis)
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
⊢ IsUnit P₁
have hdeg₂ : P.eraseLead.natDegree < P.natDegree
Tactic: have hdeg₂ := lt_of_le_of_lt P.eraseLead_natDegree_le (Nat.sub_lt
    (Nat.pos_of_ne_zero hdeg) zero_lt_one)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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
hdeg₂ : P.eraseLead.natDegree < P.natDegree
⊢ IsUnit P₁
have neg : P₁.natDegree < k
Tactic: refine hind P₁.natDegree ?_ ?_ (fun i hi => ?_) rfl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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
hdeg₂ : P.eraseLead.natDegree < P.natDegree
neg : P₁.natDegree < k
⊢ IsUnit P₁
have neg₁ : IsUnit (P₁.coeff 0)
Tactic: refine hind P₁.natDegree ?_ ?_ (fun i hi => ?_) rfl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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
hdeg₂ : P.eraseLead.natDegree < P.natDegree
neg : P₁.natDegree < k
neg₁ : IsUnit (P₁.coeff 0)
⊢ IsUnit P₁
have neg₂ : ∀ (i : ℕ) (hi : i ≠ 0), IsNilpotent (P₁.coeff i)
Tactic: refine hind P₁.natDegree ?_ ?_ (fun i hi => ?_) rfl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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
hdeg₂ : P.eraseLead.natDegree < P.natDegree
i : ℕ
hi : i ≠ 0
⊢ IsNilpotent (P₁.coeff i)
have pos : ∀ (H : i ≤ P₁.natDegree), IsNilpotent (P₁.coeff i)
Tactic: by_cases! H : i ≤ P₁.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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
hdeg₂ : P.eraseLead.natDegree < P.natDegree
i : ℕ
hi : i ≠ 0
pos : ∀ (H : i ≤ P₁.natDegree), IsNilpotent (P₁.coeff i)
⊢ IsNilpotent (P₁.coeff i)
have neg : ∀ (H : P₁.natDegree < i), IsNilpotent (P₁.coeff i)
Tactic: by_cases! H : i ≤ P₁.natDegree
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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
hdeg₂ : P.eraseLead.natDegree < P.natDegree
i : ℕ
hi : i ≠ 0
H : i ≤ P₁.natDegree
pos : IsNilpotent (P.eraseLead.coeff i)
⊢ IsNilpotent (P₁.coeff i)
have pos₁ : IsNilpotent (P.coeff i)
Tactic: simp_rw [P₁, eraseLead_coeff_of_ne _ (ne_of_lt (lt_of_le_of_lt H hdeg₂)), hnil i hi]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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
hdeg₂ : P.eraseLead.natDegree < P.natDegree
i : ℕ
hi : i ≠ 0
H : P₁.natDegree < i
⊢ IsNilpotent (P₁.coeff i)
have neg : IsNilpotent.{u_1} (R := R) 0
Tactic: simp_rw [coeff_eq_zero_of_natDegree_lt H, IsNilpotent.zero]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
hunit : IsUnit P
⊢ IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
have obtain : ∀ (Q : R[X]) (hQ : P * Q = 1), IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
Tactic: obtain ⟨Q, hQ⟩ := IsUnit.exists_right_inv hunit
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
⊢ IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
have left : IsUnit (P.coeff 0)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
left : IsUnit (P.coeff 0)
⊢ IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
have right : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
⊢ IsUnit (P.coeff 0)
have left : P.coeff 0 * Q.coeff 0 = 1
Tactic: refine .of_mul_eq_one (Q.coeff 0) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
⊢ P.coeff 0 * Q.coeff 0 = 1
have h : P.coeff 0 * Q.coeff 0 = (P * Q).coeff 0
Tactic: have h := (mul_coeff_zero P Q).symm
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
h : P.coeff 0 * Q.coeff 0 = (P * Q).coeff 0
⊢ P.coeff 0 * Q.coeff 0 = 1
have left : ∀ (h : P.coeff 0 * Q.coeff 0 = coeff 1 0), P.coeff 0 * Q.coeff 0 = 1
Tactic: rwa [hQ, coeff_one_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
h : P.coeff 0 * Q.coeff 0 = (P * Q).coeff 0
left : ∀ (h : P.coeff 0 * Q.coeff 0 = coeff 1 0), P.coeff 0 * Q.coeff 0 = 1
⊢ P.coeff 0 * Q.coeff 0 = 1
have left₁ : ∀ (h : P.coeff 0 * Q.coeff 0 = 1), P.coeff 0 * Q.coeff 0 = 1
Tactic: rwa [hQ, coeff_one_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
⊢ IsNilpotent (P.coeff n)
have right : ∀ (J : Ideal R), J.IsPrime → P.coeff n ∈ J
Tactic: rw [nilpotent_iff_mem_prime]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : I.IsPrime
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
⊢ degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) P) = 0 ∧
    degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) Q) = 0
have rw : degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) P) +
    degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) Q) =
  0
Tactic: rw [← Nat.WithBot.add_eq_zero_iff, ← degree_mul, ← map_mul, hQ, map_one, degree_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : I.IsPrime
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
rw :
  degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) P) +
      degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) Q) =
    0
⊢ degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) P) = 0 ∧
    degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) Q) = 0
have rw₁ : (HMul.hMul (α := (R ⧸ I)[X]) (β := (R ⧸ I)[X]) ((f : (a : R[X]) → (R ⧸ I)[X]) P : (R ⧸ I)[X])
      ((f : (a : R[X]) → (R ⧸ I)[X]) Q : (R ⧸ I)[X])).degree =
  0
Tactic: rw [← Nat.WithBot.add_eq_zero_iff, ← degree_mul, ← map_mul, hQ, map_one, degree_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : I.IsPrime
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
rw :
  degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) P) +
      degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) Q) =
    0
rw₁ :
  (HMul.hMul (α := (R ⧸ I)[X]) (β := (R ⧸ I)[X]) ((f : (a : R[X]) → (R ⧸ I)[X]) P : (R ⧸ I)[X])
        ((f : (a : R[X]) → (R ⧸ I)[X]) Q : (R ⧸ I)[X])).degree =
    0
⊢ degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) P) = 0 ∧
    degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) Q) = 0
have rw₂ : degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) (P * Q)) = 0
Tactic: rw [← Nat.WithBot.add_eq_zero_iff, ← degree_mul, ← map_mul, hQ, map_one, degree_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : I.IsPrime
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
rw :
  degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) P) +
      degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) Q) =
    0
rw₁ :
  (HMul.hMul (α := (R ⧸ I)[X]) (β := (R ⧸ I)[X]) ((f : (a : R[X]) → (R ⧸ I)[X]) P : (R ⧸ I)[X])
        ((f : (a : R[X]) → (R ⧸ I)[X]) Q : (R ⧸ I)[X])).degree =
    0
rw₂ : degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) (P * Q)) = 0
⊢ degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) P) = 0 ∧
    degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) Q) = 0
have rw₃ : degree (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) 1) = 0
Tactic: rw [← Nat.WithBot.add_eq_zero_iff, ← degree_mul, ← map_mul, hQ, map_one, degree_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : I.IsPrime
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
rw :
  degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) P) +
      degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) Q) =
    0
rw₁ :
  (HMul.hMul (α := (R ⧸ I)[X]) (β := (R ⧸ I)[X]) ((f : (a : R[X]) → (R ⧸ I)[X]) P : (R ⧸ I)[X])
        ((f : (a : R[X]) → (R ⧸ I)[X]) Q : (R ⧸ I)[X])).degree =
    0
rw₂ : degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) (P * Q)) = 0
rw₃ : degree (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) 1) = 0
⊢ degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) P) = 0 ∧
    degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) Q) = 0
have rw₄ : degree.{u_1} (R := R ⧸ I) 1 = 0
Tactic: rw [← Nat.WithBot.add_eq_zero_iff, ← degree_mul, ← map_mul, hQ, map_one, degree_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : I.IsPrime
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
rw :
  degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) P) +
      degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) Q) =
    0
rw₁ :
  (HMul.hMul (α := (R ⧸ I)[X]) (β := (R ⧸ I)[X]) ((f : (a : R[X]) → (R ⧸ I)[X]) P : (R ⧸ I)[X])
        ((f : (a : R[X]) → (R ⧸ I)[X]) Q : (R ⧸ I)[X])).degree =
    0
rw₂ : degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) (P * Q)) = 0
rw₃ : degree (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) 1) = 0
rw₄ : degree.{u_1} (R := R ⧸ I) 1 = 0
⊢ degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) P) = 0 ∧
    degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) Q) = 0
have rw₅ : Eq (α := WithBot ℕ) 0 0
Tactic: rw [← Nat.WithBot.add_eq_zero_iff, ← degree_mul, ← map_mul, hQ, map_one, degree_one]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
n : ℕ
hn : n ≠ 0
I : Ideal R
hI : I.IsPrime
f : R[X] →+* (R ⧸ I)[X] := mapRingHom (Ideal.Quotient.mk I)
⊢ P.coeff n ∈ I
have hPQ : degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) P) = 0 ∧
  degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) Q) = 0
Tactic: have hPQ : degree (f P) = 0 ∧ degree (f Q) = 0 := by
      rw [← Nat.WithBot.add_eq_zero_iff, ← degree_mul, ← map_mul, hQ, map_one, degree_one]