awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
neg : IsUnit P₁
⊢ 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)
-- 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
⊢ 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)
-- 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
hdeg₂ : P.eraseLead.natDegree < P.natDegree
⊢ IsUnit P₁

Tactic:
hind P₁.natDegree ?_ ?_ (fun i hi => ?_) rfl

Premises used: Polynomial.natDegree, rfl
-- 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
hdeg₂ : P.eraseLead.natDegree < P.natDegree
neg : P₁.natDegree < k
neg₁ : IsUnit (P₁.coeff 0)
neg₂ : ∀ (i : ℕ) (hi : i ≠ 0), IsNilpotent (P₁.coeff i)
⊢ IsUnit P₁

Tactic:
refine hind P₁.natDegree ?_ ?_ (fun i hi => ?_) rfl

Premises used: Polynomial.natDegree, rfl
-- 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
hdeg₂ : P.eraseLead.natDegree < P.natDegree
neg : P.eraseLead.natDegree < k
neg₁ : P.eraseLead.natDegree < P.natDegree
⊢ P₁.natDegree < k

Tactic:
simp_rw [P₁, ← h, hdeg₂]
-- 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
hdeg₂ : P.eraseLead.natDegree < P.natDegree
neg : IsUnit (P.eraseLead.coeff 0)
neg₁ : IsUnit (P.coeff 0)
⊢ IsUnit (P₁.coeff 0)

Tactic:
simp_rw [P₁, eraseLead_coeff_of_ne _ (Ne.symm hdeg), hunit]

Premises used: Ne.symm, Polynomial.eraseLead_coeff_of_ne
-- 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
hdeg₂ : P.eraseLead.natDegree < P.natDegree
i : ℕ
hi : i ≠ 0
pos : ∀ (H : i ≤ P₁.natDegree), IsNilpotent (P₁.coeff i)
neg : ∀ (H : P₁.natDegree < i), IsNilpotent (P₁.coeff i)
⊢ IsNilpotent (P₁.coeff i)

Tactic:
by_cases! H : i ≤ P₁.natDegree

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
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)
pos₁ : IsNilpotent (P.coeff i)
⊢ 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]

Premises used: lt_of_le_of_lt, Polynomial.eraseLead_coeff_of_ne, ne_of_lt
-- 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
hdeg₂ : P.eraseLead.natDegree < P.natDegree
i : ℕ
hi : i ≠ 0
H : P₁.natDegree < i
neg : IsNilpotent.{u_1} (R := R) 0
⊢ IsNilpotent (P₁.coeff i)

Tactic:
simp_rw [coeff_eq_zero_of_natDegree_lt H, IsNilpotent.zero]

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt, IsNilpotent.zero
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
hunit : IsUnit P
obtain : ∀ (Q : R[X]) (hQ : P * Q = 1), IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
⊢ IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)

Tactic:
obtain ⟨Q, hQ⟩ := IsUnit.exists_right_inv hunit

Premises used: IsUnit.exists_right_inv
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
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)
right : ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)
⊢ IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)

Tactic:
constructor
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
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)

Tactic:
.of_mul_eq_one (Q.coeff 0) ?_

Premises used: IsUnit.of_mul_eq_one, Polynomial.coeff, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
hunit : IsUnit P
Q : R[X]
hQ : P * Q = 1
left : P.coeff 0 * Q.coeff 0 = 1
⊢ IsUnit (P.coeff 0)

Tactic:
refine .of_mul_eq_one (Q.coeff 0) ?_
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
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 = (P * Q).coeff 0

Tactic:
have h := (mul_coeff_zero P Q).symm
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
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
left₁ left₂ left₃ left₄ : ∀ (h : P.coeff 0 * Q.coeff 0 = 1), P.coeff 0 * Q.coeff 0 = 1
⊢ P.coeff 0 * Q.coeff 0 = 1

Tactic:
rwa [hQ, coeff_one_zero] at h

Premises used: Polynomial.coeff_one_zero
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
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
right : ∀ (J : Ideal R), J.IsPrime → P.coeff n ∈ J
⊢ IsNilpotent (P.coeff n)

Tactic:
rw [nilpotent_iff_mem_prime]

Premises used: nilpotent_iff_mem_prime
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
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
rw₅ rw₆ : Eq (α := WithBot ℕ) 0 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

Tactic:
rw [← Nat.WithBot.add_eq_zero_iff, ← degree_mul, ← map_mul, hQ, map_one, degree_one]

Premises used: map_mul, Polynomial.degree_one, map_one, Nat.WithBot.add_eq_zero_iff, Polynomial.degree_mul
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
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

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]
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
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)
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
⊢ Eq.{u_1 + 1} (α := R ⧸ I) (coeff ((f : (a : R[X]) → (R ⧸ I)[X]) P) n) 0

Tactic:
coeff_eq_zero_of_degree_lt ?_

Premises used: Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
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)
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
refine : degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) P) < (↑n : WithBot ℕ)
⊢ Eq.{u_1 + 1} (α := R ⧸ I) (coeff ((f : (a : R[X]) → (R ⧸ I)[X]) P) n) 0

Tactic:
refine coeff_eq_zero_of_degree_lt ?_

Premises used: Polynomial.coeff_eq_zero_of_degree_lt
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
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)
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
rw : LT.lt (α := WithBot ℕ) 0 (↑n : WithBot ℕ)
⊢ degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) P) < (↑n : WithBot ℕ)

Tactic:
rw [hPQ.1]

Premises used: And.left
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
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)
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
⊢ LT.lt (α := WithBot ℕ) 0 (↑n : WithBot ℕ)

Tactic:
WithBot.coe_pos.2 hn.bot_lt

Premises used: Iff.mpr, WithBot.coe_pos, Ne.bot_lt
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
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)
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
⊢ LT.lt (α := WithBot ℕ) 0 (↑n : WithBot ℕ)

Tactic:
exact WithBot.coe_pos.2 hn.bot_lt

Premises used: Iff.mpr, WithBot.coe_pos, Ne.bot_lt
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
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)
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
⊢ Eq.{u_1 + 1} (α := R ⧸ I) (coeff ((f : (a : R[X]) → (R ⧸ I)[X]) P) n) 0

Tactic:
have hcoeff : (f P).coeff n = 0 := by
      refine coeff_eq_zero_of_degree_lt ?_
      rw [hPQ.1]
      exact WithBot.coe_pos.2 hn.bot_lt
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
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)
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
hcoeff : Eq.{u_1 + 1} (α := R ⧸ I) (coeff ((f : (a : R[X]) → (R ⧸ I)[X]) P) n) 0
⊢ P.coeff n ∈ I

Tactic:
rw [coe_mapRingHom, coeff_map, ← RingHom.mem_ker, Ideal.mk_ker] at hcoeff

Premises used: Polynomial.coeff_map, RingHom.mem_ker, Polynomial.coe_mapRingHom, Ideal.mk_ker
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
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)
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
hcoeff : P.coeff n ∈ I
⊢ P.coeff n ∈ I

Tactic:
hcoeff
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
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)
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
hcoeff : P.coeff n ∈ I
⊢ P.coeff n ∈ I

Tactic:
exact hcoeff
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
⊢ IsUnit P ↔ IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)

Tactic:
⟨coeff_isUnit_isNilpotent_of_isUnit, fun H => isUnit_of_coeff_isUnit_isNilpotent H.1 H.2⟩

Premises used: Polynomial.coeff_isUnit_isNilpotent_of_isUnit, Polynomial.isUnit_of_coeff_isUnit_isNilpotent, And.right, And.left, Iff.intro
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
r : R
inst : CommRing R
P : R[X]
⊢ ∀ (i : ℕ), (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (X * P)).coeff (i + 1) = P.coeff i

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
r : R
inst : CommRing R
P : R[X]
⊢ ∀ (i : ℕ), (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (X * P)).coeff (i + 1) = P.coeff i

Tactic:
have : ∀ i, coeff (C r + X * P) (i + 1) = coeff P i := by simp
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
r : R
inst : CommRing R
P : R[X]
this : ∀ (i : ℕ), (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (X * P)).coeff (i + 1) = P.coeff i
simp_rw :
  (IsUnit ((HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (X * P)).coeff 0) ∧
      ∀ (i : ℕ), IsNilpotent (P.coeff i)) ↔
    IsUnit r ∧ IsNilpotent P
⊢ IsUnit (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (X * P)) ↔ IsUnit r ∧ IsNilpotent P

Tactic:
simp_rw [isUnit_iff_coeff_isUnit_isNilpotent, Nat.forall_ne_zero_iff, this]

Premises used: Polynomial.isUnit_iff_coeff_isUnit_isNilpotent, Nat.forall_ne_zero_iff
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
r : R
inst : CommRing R
P : R[X]
this : ∀ (i : ℕ), (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (X * P)).coeff (i + 1) = P.coeff i
⊢ (IsUnit ((HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (X * P)).coeff 0) ∧
      ∀ (i : ℕ), IsNilpotent (P.coeff i)) ↔
    IsUnit r ∧ IsNilpotent P

Tactic:
simp only [coeff_add, coeff_C_zero, mul_coeff_zero, coeff_X_zero, zero_mul, add_zero,
    ← Polynomial.isNilpotent_iff]

Premises used: MulZeroClass.zero_mul, Polynomial.coeff_X_zero, Polynomial.coeff_add, Polynomial.isNilpotent_iff, Polynomial.mul_coeff_zero, Polynomial.coeff_C_zero, add_zero
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
this : P = HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (eval 0 P) : R[X]) (X * (P /ₘ X))
rw : IsUnit (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (eval 0 P) : R[X]) (X * (P /ₘ X)))
| IsUnit P

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
this : P = HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (eval 0 P) : R[X]) (X * (P /ₘ X))
simp : IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)
| IsUnit (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (eval 0 P) : R[X]) (X * (P /ₘ X)))

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
this : P = HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (eval 0 P) : R[X]) (X * (P /ₘ X))
rw : IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)
| IsUnit P

Tactic:
rw [this]; simp
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
this : P = HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (eval 0 P) : R[X]) (X * (P /ₘ X))
conv_lhs : IsUnit P ↔ IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)
conv_lhs₁ : IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X) ↔ IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)
⊢ IsUnit P ↔ IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)

Tactic:
conv_lhs => rw [this]; simp
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
suffices : P = HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (eval 0 P) : R[X]) (X * (P /ₘ X))
⊢ IsUnit P ↔ IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)

Tactic:
suffices P = C (eval 0 P) + X * (P /ₘ X) by
    conv_lhs => rw [this]; simp
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
rw : P %ₘ X + X * (P /ₘ X)
| P

Tactic:
rw [← modByMonic_add_div P X]

Premises used: Polynomial.modByMonic_add_div, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
conv_lhs : P %ₘ X + X * (P /ₘ X) = HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (eval 0 P) : R[X]) (X * (P /ₘ X))
⊢ P = HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (eval 0 P) : R[X]) (X * (P /ₘ X))

Tactic:
conv_lhs => rw [← modByMonic_add_div P X]

Premises used: Polynomial.modByMonic_add_div, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
⊢ P %ₘ X + X * (P /ₘ X) = HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (eval 0 P) : R[X]) (X * (P /ₘ X))

Tactic:
simp [modByMonic_X]

Premises used: Polynomial.modByMonic_X
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsReduced R
p : R[X]
hpl : 0 < p.natDegree
simp : IsUnit (p.coeff 0) → ∃ (x : ℕ), ¬x = 0 ∧ ¬p.coeff x = 0
⊢ ¬IsUnit p

Tactic:
simp only [ne_eq, isNilpotent_iff_eq_zero, not_and, not_forall, exists_prop,
    Polynomial.isUnit_iff_coeff_isUnit_isNilpotent]

Premises used: isNilpotent_iff_eq_zero, Polynomial.isUnit_iff_coeff_isUnit_isNilpotent, exists_prop, ne_eq, not_and, Classical.not_forall
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsReduced R
p : R[X]
hpl : 0 < p.natDegree
h : IsUnit (p.coeff 0)
⊢ ∃ (x : ℕ), ¬x = 0 ∧ ¬p.coeff x = 0

Tactic:
⟨p.natDegree, hpl.ne', ?_⟩

Premises used: LT.lt.ne', And.intro, Exists.intro, Polynomial.natDegree
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsReduced R
p : R[X]
hpl : 0 < p.natDegree
h : IsUnit (p.coeff 0)
refine : ¬p.coeff p.natDegree = 0
⊢ ∃ (x : ℕ), ¬x = 0 ∧ ¬p.coeff x = 0

Tactic:
refine ⟨p.natDegree, hpl.ne', ?_⟩
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsReduced R
p : R[X]
hpl : 0 < p.natDegree
h : IsUnit (p.coeff 0)
contrapose! : ∀ (hpl : p.coeff p.natDegree = 0), p.natDegree ≤ 0
⊢ ¬p.coeff p.natDegree = 0

Tactic:
contrapose! hpl
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsReduced R
p : R[X]
h : IsUnit (p.coeff 0)
hpl : p.coeff p.natDegree = 0
⊢ p = 0

Tactic:
simp only [coeff_natDegree, leadingCoeff_eq_zero] at hpl

Premises used: Polynomial.coeff_natDegree, Polynomial.leadingCoeff_eq_zero
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsReduced R
p : R[X]
h : IsUnit (p.coeff 0)
hpl : p = 0
⊢ p.natDegree ≤ 0

Tactic:
simp [hpl]
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsReduced R
p : R[X]
hpl : 0 < p.degree
⊢ ¬IsUnit p

Tactic:
not_isUnit_of_natDegree_pos_of_isReduced _ (natDegree_pos_iff_degree_pos.mpr hpl)

Premises used: Iff.mpr, Polynomial.not_isUnit_of_natDegree_pos_of_isReduced, Polynomial.natDegree_pos_iff_degree_pos
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
r : R
inst : CommRing R
P : R[X]
⊢ ∀ (a : R), IsUnit (M := R[X]) ((C : (a : R) → R[X]) a : R[X]) → IsUnit a

Tactic:
simp +contextual [isUnit_iff_coeff_isUnit_isNilpotent, coeff_C]

Premises used: Polynomial.isUnit_iff_coeff_isUnit_isNilpotent, Polynomial.coeff_C
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
r : R
inst : CommRing R
P : R[X]
⊢ ∀ (a : R), IsUnit (M := R[X]) ((C : (a : R) → R[X]) a : R[X]) → IsUnit a

Tactic:
classical simp +contextual [isUnit_iff_coeff_isUnit_isNilpotent, coeff_C]

Premises used: Polynomial.isUnit_iff_coeff_isUnit_isNilpotent, Polynomial.coeff_C
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_1
r : R
inst : CommRing R
P : R[X]
⊢ IsLocalHom (R := R) (S := R[X]) (F := R →+* R[X]) (algebraMap R R[X])

Tactic:
inferInstanceAs (IsLocalHom C)

Premises used: _private.0.Polynomial.instIsLocalHomRingHomAlgebraMap._proof_1
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : R[X]
a b : S
h : IsNilpotent (a - b)
simp : IsNilpotent (eval a (map (algebraMap R S) P) - eval b (map (algebraMap R S) P))
⊢ IsNilpotent (HSub.hSub (α := S) (β := S) ((aeval a : (a : R[X]) → S) P : S) ((aeval b : (a : R[X]) → S) P : S))

Tactic:
simp only [← eval_map_algebraMap]

Premises used: Polynomial.eval_map_algebraMap
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : R[X]
a b : S
h : IsNilpotent (a - b)
have :
  ∀ (c : S) (hc : eval a (map (algebraMap R S) P) - eval b (map (algebraMap R S) P) = c * (a - b)),
    IsNilpotent (eval a (map (algebraMap R S) P) - eval b (map (algebraMap R S) P))
⊢ IsNilpotent (eval a (map (algebraMap R S) P) - eval b (map (algebraMap R S) P))

Tactic:
have ⟨c, hc⟩ := evalSubFactor (map (algebraMap R S) P) a b
-- Module: Mathlib.RingTheory.Polynomial.Nilpotent
Goal:
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : R[X]
a b : S
h : IsNilpotent (a - b)
c : S
hc : eval a (map (algebraMap R S) P) - eval b (map (algebraMap R S) P) = c * (a - b)
⊢ IsNilpotent (eval a (map (algebraMap R S) P) - eval b (map (algebraMap R S) P))

Tactic:
hc ▸ (Commute.all _ _).isNilpotent_mul_left h

Premises used: Commute.isNilpotent_mul_left, Eq.rec, Eq.symm