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 : 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
have refine : degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) P) < (↑n : WithBot ℕ)
Tactic: refine coeff_eq_zero_of_degree_lt ?_
-- 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)
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
⊢ degree.{u_1} (R := R ⧸ I) ((f : (a : R[X]) → (R ⧸ I)[X]) P) < (↑n : WithBot ℕ)
have rw : LT.lt (α := WithBot ℕ) 0 (↑n : WithBot ℕ)
Tactic: rw [hPQ.1]
-- 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)
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
⊢ P.coeff n ∈ I
have hcoeff : 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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (hypothesis)
Goal:
R : Type u_1
r : R
inst : CommRing R
P : R[X]
⊢ IsUnit (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (X * P)) ↔ IsUnit r ∧ IsNilpotent P
have this : ∀ (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
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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)) ↔ IsUnit r ∧ IsNilpotent P
have 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
Tactic: simp_rw [isUnit_iff_coeff_isUnit_isNilpotent, Nat.forall_ne_zero_iff, this]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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))
| IsUnit P
have rw : IsUnit (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (eval 0 P) : R[X]) (X * (P /ₘ X)))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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))
| IsUnit (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (eval 0 P) : R[X]) (X * (P /ₘ X)))
have simp : IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)
Tactic: simp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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))
| IsUnit P
have rw : IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)
Tactic: rw [this]; simp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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))
⊢ IsUnit P ↔ IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)
have conv_lhs : IsUnit P ↔ IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)
Tactic: conv_lhs => rw [this]; simp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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)
⊢ IsUnit P ↔ IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)
have conv_lhs₁ : IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X) ↔ IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)
Tactic: conv_lhs => rw [this]; simp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
⊢ IsUnit P ↔ IsUnit (eval 0 P) ∧ IsNilpotent (P /ₘ X)
have suffices : P = HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (eval 0 P) : R[X]) (X * (P /ₘ X))
Tactic: suffices P = C (eval 0 P) + X * (P /ₘ X) by
    conv_lhs => rw [this]; simp
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
| P
have rw : P %ₘ X + X * (P /ₘ X)
Tactic: rw [← modByMonic_add_div P X]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
P : R[X]
⊢ P = HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) (eval 0 P) : R[X]) (X * (P /ₘ X))
have conv_lhs : P %ₘ X + X * (P /ₘ X) = 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]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsReduced R
p : R[X]
hpl : 0 < p.natDegree
⊢ ¬IsUnit p
have simp : IsUnit (p.coeff 0) → ∃ (x : ℕ), ¬x = 0 ∧ ¬p.coeff x = 0
Tactic: simp only [ne_eq, isNilpotent_iff_eq_zero, not_and, not_forall, exists_prop,
    Polynomial.isUnit_iff_coeff_isUnit_isNilpotent]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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
have refine : ¬p.coeff p.natDegree = 0
Tactic: refine ⟨p.natDegree, hpl.ne', ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsReduced R
p : R[X]
hpl : 0 < p.natDegree
h : IsUnit (p.coeff 0)
⊢ ¬p.coeff p.natDegree = 0
have contrapose! : ∀ (hpl : p.coeff p.natDegree = 0), p.natDegree ≤ 0
Tactic: contrapose! hpl
Cleared hypotheses: hpl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (hypothesis)
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.natDegree ≤ 0
have hpl₁ : p = 0
Tactic: simp only [coeff_natDegree, leadingCoeff_eq_zero] at hpl
Cleared hypotheses: hpl
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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)
⊢ IsNilpotent (HSub.hSub (α := S) (β := S) ((aeval a : (a : R[X]) → S) P : S) ((aeval b : (a : R[X]) → S) P : S))
have simp : IsNilpotent (eval a (map (algebraMap R S) P) - eval b (map (algebraMap R S) P))
Tactic: simp only [← eval_map_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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)
⊢ IsNilpotent (eval a (map (algebraMap R S) P) - eval b (map (algebraMap R S) P))
have 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))
Tactic: have ⟨c, hc⟩ := evalSubFactor (map (algebraMap R S) P) a b
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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
hb : IsUnit.{u_3} (M := S) ((aeval b : (a : R[X]) → S) P : S)
hab : IsNilpotent (a - b)
⊢ IsUnit.{u_3} (M := S) ((aeval a : (a : R[X]) → S) P : S)
have rw : IsUnit
  (HAdd.hAdd (α := S) ((aeval b : (a : R[X]) → S) P : S)
    (HSub.hSub (α := S) (β := S) ((aeval a : (a : R[X]) → S) P : S) ((aeval b : (a : R[X]) → S) P : S)))
Tactic: rw [← add_sub_cancel (aeval b P) (aeval a P)]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Nilpotent (goal)
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
hb : IsUnit.{u_3} (M := S) ((aeval b : (a : R[X]) → S) P : S)
hab : IsNilpotent (a - b)
⊢ IsUnit
    (HAdd.hAdd (α := S) ((aeval b : (a : R[X]) → S) P : S)
      (HSub.hSub (α := S) (β := S) ((aeval a : (a : R[X]) → S) P : S) ((aeval b : (a : R[X]) → S) P : S)))
have refine : IsNilpotent (HSub.hSub (α := S) (β := S) ((aeval a : (a : R[X]) → S) P : S) ((aeval b : (a : R[X]) → S) P : S))
Tactic: refine IsNilpotent.isUnit_add_left_of_commute ?_ hb (Commute.all _ _)
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
r : Rᵐᵒᵖ
n : ℕ
⊢ (RingEquiv.symm (opRingEquiv R) : (a : Rᵐᵒᵖ[X]) → R[X]ᵐᵒᵖ)
      (HMul.hMul (α := Rᵐᵒᵖ[X]) ((C : (a : Rᵐᵒᵖ) → Rᵐᵒᵖ[X]) r : Rᵐᵒᵖ[X]) (HPow.hPow (α := Rᵐᵒᵖ[X]) X n)) =
    op (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (unop r) : R[X]) (HPow.hPow (α := R[X]) X n))
have rw : (RingEquiv.symm (opRingEquiv R) : (a : Rᵐᵒᵖ[X]) → R[X]ᵐᵒᵖ) ((monomial n : (a : Rᵐᵒᵖ) → Rᵐᵒᵖ[X]) r : Rᵐᵒᵖ[X]) =
  op (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (unop r) : R[X]) (HPow.hPow (α := R[X]) X n))
Tactic: rw [C_mul_X_pow_eq_monomial, opRingEquiv_symm_monomial, C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
r : Rᵐᵒᵖ
n : ℕ
rw :
  (RingEquiv.symm (opRingEquiv R) : (a : Rᵐᵒᵖ[X]) → R[X]ᵐᵒᵖ) ((monomial n : (a : Rᵐᵒᵖ) → Rᵐᵒᵖ[X]) r : Rᵐᵒᵖ[X]) =
    op (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (unop r) : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ (RingEquiv.symm (opRingEquiv R) : (a : Rᵐᵒᵖ[X]) → R[X]ᵐᵒᵖ)
      (HMul.hMul (α := Rᵐᵒᵖ[X]) ((C : (a : Rᵐᵒᵖ) → Rᵐᵒᵖ[X]) r : Rᵐᵒᵖ[X]) (HPow.hPow (α := Rᵐᵒᵖ[X]) X n)) =
    op (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (unop r) : R[X]) (HPow.hPow (α := R[X]) X n))
have rw₁ : op ((monomial n : (a : R) → R[X]) (unop r)) =
  op (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (unop r) : R[X]) (HPow.hPow (α := R[X]) X n))
Tactic: rw [C_mul_X_pow_eq_monomial, opRingEquiv_symm_monomial, C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
r : Rᵐᵒᵖ
n : ℕ
rw :
  (RingEquiv.symm (opRingEquiv R) : (a : Rᵐᵒᵖ[X]) → R[X]ᵐᵒᵖ) ((monomial n : (a : Rᵐᵒᵖ) → Rᵐᵒᵖ[X]) r : Rᵐᵒᵖ[X]) =
    op (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (unop r) : R[X]) (HPow.hPow (α := R[X]) X n))
rw₁ :
  op ((monomial n : (a : R) → R[X]) (unop r)) =
    op (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (unop r) : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ (RingEquiv.symm (opRingEquiv R) : (a : Rᵐᵒᵖ[X]) → R[X]ᵐᵒᵖ)
      (HMul.hMul (α := Rᵐᵒᵖ[X]) ((C : (a : Rᵐᵒᵖ) → Rᵐᵒᵖ[X]) r : Rᵐᵒᵖ[X]) (HPow.hPow (α := Rᵐᵒᵖ[X]) X n)) =
    op (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (unop r) : R[X]) (HPow.hPow (α := R[X]) X n))
have rw₂ : Eq (α := R[X]ᵐᵒᵖ) (op ((monomial n : (a : R) → R[X]) (unop r)) : R[X]ᵐᵒᵖ)
  (op ((monomial n : (a : R) → R[X]) (unop r)) : R[X]ᵐᵒᵖ)
Tactic: rw [C_mul_X_pow_eq_monomial, opRingEquiv_symm_monomial, C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]ᵐᵒᵖ
⊢ support.{u_1} (R := Rᵐᵒᵖ) ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p) = (unop p).support
have h : ∀ (a : ℕ), a ∈ support.{u_1} (R := Rᵐᵒᵖ) ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p) ↔ a ∈ (unop p).support
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]ᵐᵒᵖ
⊢ leadingCoeff ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p) = op (unop p).leadingCoeff
have rw : coeff ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p)
    (natDegree.{u_1} (R := Rᵐᵒᵖ) ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p)) =
  op (unop p).leadingCoeff
Tactic: rw [leadingCoeff, coeff_opRingEquiv, natDegree_opRingEquiv, leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]ᵐᵒᵖ
rw :
  coeff ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p)
      (natDegree.{u_1} (R := Rᵐᵒᵖ) ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p)) =
    op (unop p).leadingCoeff
⊢ leadingCoeff ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p) = op (unop p).leadingCoeff
have rw₁ : op ((unop p).coeff (natDegree.{u_1} (R := Rᵐᵒᵖ) ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p))) =
  op (unop p).leadingCoeff
Tactic: rw [leadingCoeff, coeff_opRingEquiv, natDegree_opRingEquiv, leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]ᵐᵒᵖ
rw :
  coeff ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p)
      (natDegree.{u_1} (R := Rᵐᵒᵖ) ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p)) =
    op (unop p).leadingCoeff
rw₁ :
  op ((unop p).coeff (natDegree.{u_1} (R := Rᵐᵒᵖ) ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p))) =
    op (unop p).leadingCoeff
⊢ leadingCoeff ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p) = op (unop p).leadingCoeff
have rw₂ : op ((unop p).coeff (unop p).natDegree) = op (unop p).leadingCoeff
Tactic: rw [leadingCoeff, coeff_opRingEquiv, natDegree_opRingEquiv, leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
p : R[X]ᵐᵒᵖ
rw :
  coeff ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p)
      (natDegree.{u_1} (R := Rᵐᵒᵖ) ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p)) =
    op (unop p).leadingCoeff
rw₁ :
  op ((unop p).coeff (natDegree.{u_1} (R := Rᵐᵒᵖ) ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p))) =
    op (unop p).leadingCoeff
rw₂ : op ((unop p).coeff (unop p).natDegree) = op (unop p).leadingCoeff
⊢ leadingCoeff ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p) = op (unop p).leadingCoeff
have rw₃ : op ((unop p).coeff (unop p).natDegree) = op ((unop p).coeff (unop p).natDegree)
Tactic: rw [leadingCoeff, coeff_opRingEquiv, natDegree_opRingEquiv, leadingCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
h : IsLeftCancelMulZero.{u_1} R[X]
a b c : R
eq : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ a + x) b) ((fun (x : R) ↦ a + x) c)
⊢ b = c
have a₁ : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
h : IsLeftCancelMulZero.{u_1} R[X]
a b c : R
eq : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ a + x) b) ((fun (x : R) ↦ a + x) c)
h_1 : Nontrivial R
trinomial : (r : R) → R[X] :=
  fun (r : R) ↦
    HAdd.hAdd (β := R[X]) (a • HPow.hPow (α := R[X]) (β := ℕ) X 2 + HSMul.hSMul (β := R[X]) r X)
      ((C : (a : R) → R[X]) a : R[X])
r : R
⊢ HAdd.hAdd (α := R[X]) X ((C : (a : R) → R[X]) 1) * trinomial r =
    HAdd.hAdd (β := R[X])
      (a • HPow.hPow (α := R[X]) (β := ℕ) X 3 + (a + r) • HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        HSMul.hSMul (β := R[X]) (a + r) X)
      ((C : (a : R) → R[X]) a : R[X])
have simp : HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X * X +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X) +
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
      ((C : (a : R) → R[X]) a : R[X]) =
  HAdd.hAdd (β := R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2)) +
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X))
    ((C : (a : R) → R[X]) a : R[X])
Tactic: simp only [trinomial, mul_add, add_mul, ← C_mul', C_1, one_mul, ← mul_assoc, X_mul_C, C_add]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
h : IsLeftCancelMulZero.{u_1} R[X]
a b c : R
eq : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ a + x) b) ((fun (x : R) ↦ a + x) c)
h_1 : Nontrivial R
trinomial : (r : R) → R[X] :=
  fun (r : R) ↦
    HAdd.hAdd (β := R[X]) (a • HPow.hPow (α := R[X]) (β := ℕ) X 2 + HSMul.hSMul (β := R[X]) r X)
      ((C : (a : R) → R[X]) a : R[X])
r : R
⊢ HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X * HPow.hPow (α := R[X]) (β := ℕ) X 2 +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X * X +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X) +
      HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) a : R[X]) =
    HAdd.hAdd (β := R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 3) +
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2)) +
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X +
          HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X))
      ((C : (a : R) → R[X]) a : R[X])
have noncomm_ring : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (X * HMul.hMul (α := R[X]) X X) +
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HMul.hMul (α := R[X]) X X) +
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HMul.hMul (α := R[X]) X X) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X) +
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
      ((C : (a : R) → R[X]) a : R[X]) =
  HAdd.hAdd (β := R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (X * HMul.hMul (α := R[X]) X X) +
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HMul.hMul (α := R[X]) X X) +
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HMul.hMul (α := R[X]) X X)) +
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X))
    ((C : (a : R) → R[X]) a : R[X])
Tactic: noncomm_ring
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
h : IsLeftCancelMulZero.{u_1} R[X]
a b c : R
eq : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ a + x) b) ((fun (x : R) ↦ a + x) c)
h_1 : Nontrivial R
trinomial : (r : R) → R[X] :=
  fun (r : R) ↦
    HAdd.hAdd (β := R[X]) (a • HPow.hPow (α := R[X]) (β := ℕ) X 2 + HSMul.hSMul (β := R[X]) r X)
      ((C : (a : R) → R[X]) a : R[X])
⊢ b = c
have ht : ∀ (r : R),
  HAdd.hAdd (α := R[X]) X ((C : (a : R) → R[X]) 1) * trinomial r =
    HAdd.hAdd (β := R[X])
      (a • HPow.hPow (α := R[X]) (β := ℕ) X 3 + (a + r) • HPow.hPow (α := R[X]) (β := ℕ) X 2 +
        HSMul.hSMul (β := R[X]) (a + r) X)
      ((C : (a : R) → R[X]) a : R[X])
Tactic: have ht r : (X + C 1) * trinomial r = a • X ^ 3 + (a + r) • X ^ 2 + (a + r) • X + C a := by
        simp only [trinomial, mul_add, add_mul, ← C_mul', C_1, one_mul, ← mul_assoc, X_mul_C, C_add]
        noncomm_ring
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
h : IsLeftCancelMulZero.{u_1} R[X]
a b c : R
eq : Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ a + x) b) ((fun (x : R) ↦ a + x) c)
h_1 : Nontrivial R
trinomial : (r : R) → R[X] :=
  fun (r : R) ↦
    HAdd.hAdd (β := R[X]) (a • HPow.hPow (α := R[X]) (β := ℕ) X 2 + HSMul.hSMul (β := R[X]) r X)
      ((C : (a : R) → R[X]) a : R[X])
ht :
  ∀ (r : R),
    HAdd.hAdd (α := R[X]) X ((C : (a : R) → R[X]) 1) * trinomial r =
      HAdd.hAdd (β := R[X])
        (a • HPow.hPow (α := R[X]) (β := ℕ) X 3 + (a + r) • HPow.hPow (α := R[X]) (β := ℕ) X 2 +
          HSMul.hSMul (β := R[X]) (a + r) X)
        ((C : (a : R) → R[X]) a : R[X])
simp_rw simp_rw₁ :
  HAdd.hAdd (α := R[X]) X ((C : (a : R) → R[X]) 1) * trinomial b =
    HAdd.hAdd (α := R[X]) X ((C : (a : R) → R[X]) 1) * trinomial c
⊢ Eq.{u_1 + 1} (α := R[X]) ((fun (x : R[X]) ↦ HAdd.hAdd (α := R[X]) X ((C : (a : R) → R[X]) 1) * x) (trinomial b))
    ((fun (x : R[X]) ↦ HAdd.hAdd (α := R[X]) X ((C : (a : R) → R[X]) 1) * x) (trinomial c))
have simp_rw₂ : HAdd.hAdd (β := R[X])
    (a • HPow.hPow (α := R[X]) (β := ℕ) X 3 + (a + b) • HPow.hPow (α := R[X]) (β := ℕ) X 2 +
      HSMul.hSMul (β := R[X]) (a + b) X)
    ((C : (a : R) → R[X]) a : R[X]) =
  HAdd.hAdd (β := R[X])
    (a • HPow.hPow (α := R[X]) (β := ℕ) X 3 + (a + c) • HPow.hPow (α := R[X]) (β := ℕ) X 2 +
      HSMul.hSMul (β := R[X]) (a + c) X)
    ((C : (a : R) → R[X]) a : R[X])
Tactic: simp_rw [ht, eq]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
⊢ IsRightCancelMulZero.{u_1} R[X] ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
have rw : IsLeftCancelMulZero.{u_1} R[X]ᵐᵒᵖ ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
Tactic: rw [← MulOpposite.isLeftCancelMulZero_iff, (opRingEquiv R).isLeftCancelMulZero_iff,
    isLeftCancelMulZero_iff, MulOpposite.isLeftCancelMulZero_iff, MulOpposite.isCancelAdd_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
rw : IsLeftCancelMulZero.{u_1} R[X]ᵐᵒᵖ ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
⊢ IsRightCancelMulZero.{u_1} R[X] ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
have rw₁ : IsLeftCancelMulZero.{u_1} Rᵐᵒᵖ[X] ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
Tactic: rw [← MulOpposite.isLeftCancelMulZero_iff, (opRingEquiv R).isLeftCancelMulZero_iff,
    isLeftCancelMulZero_iff, MulOpposite.isLeftCancelMulZero_iff, MulOpposite.isCancelAdd_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
rw : IsLeftCancelMulZero.{u_1} R[X]ᵐᵒᵖ ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
rw₁ : IsLeftCancelMulZero.{u_1} Rᵐᵒᵖ[X] ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
⊢ IsRightCancelMulZero.{u_1} R[X] ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
have rw₂ : IsLeftCancelMulZero.{u_1} Rᵐᵒᵖ ∧ IsCancelAdd.{u_1} Rᵐᵒᵖ ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
Tactic: rw [← MulOpposite.isLeftCancelMulZero_iff, (opRingEquiv R).isLeftCancelMulZero_iff,
    isLeftCancelMulZero_iff, MulOpposite.isLeftCancelMulZero_iff, MulOpposite.isCancelAdd_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Polynomial.Opposites (goal)
Goal:
R : Type u_1
inst : Semiring R
rw : IsLeftCancelMulZero.{u_1} R[X]ᵐᵒᵖ ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
rw₁ : IsLeftCancelMulZero.{u_1} Rᵐᵒᵖ[X] ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
rw₂ : IsLeftCancelMulZero.{u_1} Rᵐᵒᵖ ∧ IsCancelAdd.{u_1} Rᵐᵒᵖ ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
⊢ IsRightCancelMulZero.{u_1} R[X] ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
have rw₃ : IsRightCancelMulZero R ∧ IsCancelAdd.{u_1} Rᵐᵒᵖ ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
Tactic: rw [← MulOpposite.isLeftCancelMulZero_iff, (opRingEquiv R).isLeftCancelMulZero_iff,
    isLeftCancelMulZero_iff, MulOpposite.isLeftCancelMulZero_iff, MulOpposite.isCancelAdd_iff]