awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact hc ▸ (Commute.all _ _).isNilpotent_mul_left h
-- 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
hb : IsUnit.{u_3} (M := S) ((aeval b : (a : R[X]) → S) P : S)
hab : IsNilpotent (a - b)
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)))
⊢ IsUnit.{u_3} (M := S) ((aeval a : (a : R[X]) → S) P : S)

Tactic:
rw [← add_sub_cancel (aeval b P) (aeval a P)]

Premises used: add_sub_cancel, Polynomial.aeval, DFunLike.coe
-- 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
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)))

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

Premises used: IsNilpotent.isUnit_add_left_of_commute, Commute.all
-- 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
hb : IsUnit.{u_3} (M := S) ((aeval b : (a : R[X]) → S) P : S)
hab : IsNilpotent (a - b)
refine : IsNilpotent (HSub.hSub (α := S) (β := S) ((aeval a : (a : R[X]) → S) P : S) ((aeval b : (a : R[X]) → S) P : S))
⊢ 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:
refine IsNilpotent.isUnit_add_left_of_commute ?_ hb (Commute.all _ _)

Premises used: IsNilpotent.isUnit_add_left_of_commute, Commute.all
-- 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
hb : IsUnit.{u_3} (M := S) ((aeval b : (a : R[X]) → S) P : S)
hab : IsNilpotent (a - b)
⊢ IsNilpotent (HSub.hSub (α := S) (β := S) ((aeval a : (a : R[X]) → S) P : S) ((aeval b : (a : R[X]) → S) P : S))

Tactic:
isNilpotent_aeval_sub_of_isNilpotent_sub P hab

Premises used: Polynomial.isNilpotent_aeval_sub_of_isNilpotent_sub
-- 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
hb : IsUnit.{u_3} (M := S) ((aeval b : (a : R[X]) → S) P : S)
hab : IsNilpotent (a - b)
⊢ IsNilpotent (HSub.hSub (α := S) (β := S) ((aeval a : (a : R[X]) → S) P : S) ((aeval b : (a : R[X]) → S) P : S))

Tactic:
exact isNilpotent_aeval_sub_of_isNilpotent_sub P hab

Premises used: Polynomial.isNilpotent_aeval_sub_of_isNilpotent_sub
-- Module: Mathlib.RingTheory.Polynomial.Opposites
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
r : R
⊢ Eq (α := Rᵐᵒᵖ[X]) ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) (op ((monomial n : (a : R) → R[X]) r)) : Rᵐᵒᵖ[X])
    ((monomial n : (a : Rᵐᵒᵖ) → Rᵐᵒᵖ[X]) (op r) : Rᵐᵒᵖ[X])

Tactic:
simp [opRingEquiv]

Premises used: Polynomial.opRingEquiv
-- Module: Mathlib.RingTheory.Polynomial.Opposites
Goal:
R : Type u_1
inst : Semiring R
a : R
⊢ Eq (α := Rᵐᵒᵖ[X]) ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) (op ((C : (a : R) → R[X]) a)) : Rᵐᵒᵖ[X])
    ((C : (a : Rᵐᵒᵖ) → Rᵐᵒᵖ[X]) (op a) : Rᵐᵒᵖ[X])

Tactic:
opRingEquiv_op_monomial 0 a

Premises used: Polynomial.opRingEquiv_op_monomial, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Opposites
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq (α := Rᵐᵒᵖ[X]) ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) (op X) : Rᵐᵒᵖ[X]) (X : Rᵐᵒᵖ[X])

Tactic:
opRingEquiv_op_monomial 1 1

Premises used: Polynomial.opRingEquiv_op_monomial, OfNat.ofNat, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Opposites
Goal:
R : Type u_1
inst : Semiring R
r : R
n : ℕ
⊢ (opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X])
      (op (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))) =
    HMul.hMul (α := Rᵐᵒᵖ[X]) ((C : (a : Rᵐᵒᵖ) → Rᵐᵒᵖ[X]) (op r) : Rᵐᵒᵖ[X]) (HPow.hPow (α := Rᵐᵒᵖ[X]) X n)

Tactic:
simp only [X_pow_mul, op_mul, op_pow, map_mul, map_pow, opRingEquiv_op_X, opRingEquiv_op_C]

Premises used: Polynomial.opRingEquiv_op_C, MulOpposite.op_pow, Polynomial.opRingEquiv_op_X, map_pow, map_mul, MulOpposite.op_mul, Polynomial.X_pow_mul
-- Module: Mathlib.RingTheory.Polynomial.Opposites
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
r : Rᵐᵒᵖ
⊢ Eq (α := Rᵐᵒᵖ[X])
    ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X])
        ((RingEquiv.symm (opRingEquiv R) : (a : Rᵐᵒᵖ[X]) → R[X]ᵐᵒᵖ) ((monomial n : (a : Rᵐᵒᵖ) → Rᵐᵒᵖ[X]) r : Rᵐᵒᵖ[X])) :
      Rᵐᵒᵖ[X])
    ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) (op ((monomial n : (a : R) → R[X]) (unop r))) : Rᵐᵒᵖ[X])

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Opposites
Goal:
R : Type u_1
inst : Semiring R
a : Rᵐᵒᵖ
⊢ Eq (α := R[X]ᵐᵒᵖ)
    ((RingEquiv.symm (opRingEquiv R) : (a : Rᵐᵒᵖ[X]) → R[X]ᵐᵒᵖ) ((C : (a : Rᵐᵒᵖ) → Rᵐᵒᵖ[X]) a : Rᵐᵒᵖ[X]) : R[X]ᵐᵒᵖ)
    (op ((C : (a : R) → R[X]) (unop a)) : R[X]ᵐᵒᵖ)

Tactic:
opRingEquiv_symm_monomial 0 a

Premises used: Polynomial.opRingEquiv_symm_monomial, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Opposites
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq (α := R[X]ᵐᵒᵖ) ((RingEquiv.symm (opRingEquiv R) : (a : Rᵐᵒᵖ[X]) → R[X]ᵐᵒᵖ) X : R[X]ᵐᵒᵖ) (op X : R[X]ᵐᵒᵖ)

Tactic:
opRingEquiv_symm_monomial 1 1

Premises used: Polynomial.opRingEquiv_symm_monomial, MulOpposite.unop, OfNat.ofNat, Polynomial.X
-- Module: Mathlib.RingTheory.Polynomial.Opposites
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))
rw₂ 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]ᵐᵒᵖ)
⊢ (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))

Tactic:
rw [C_mul_X_pow_eq_monomial, opRingEquiv_symm_monomial, C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial, Polynomial.opRingEquiv_symm_monomial
-- Module: Mathlib.RingTheory.Polynomial.Opposites
Goal:
R : Type u_1
inst : Semiring R
p : R[X]ᵐᵒᵖ
n : ℕ
⊢ coeff ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p) n = op ((unop p).coeff n)

Tactic:
simp [opRingEquiv, coeff]

Premises used: Polynomial.coeff, Polynomial.opRingEquiv
-- Module: Mathlib.RingTheory.Polynomial.Opposites
Goal:
R : Type u_1
inst : Semiring R
p : R[X]ᵐᵒᵖ
h : ∀ (a : ℕ), a ∈ support.{u_1} (R := Rᵐᵒᵖ) ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p) ↔ a ∈ (unop p).support
⊢ support.{u_1} (R := Rᵐᵒᵖ) ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p) = (unop p).support

Tactic:
ext
-- Module: Mathlib.RingTheory.Polynomial.Opposites
Goal:
R : Type u_1
inst : Semiring R
p : R[X]ᵐᵒᵖ
a : ℕ
⊢ a ∈ support.{u_1} (R := Rᵐᵒᵖ) ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p) ↔ a ∈ (unop p).support

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Opposites
Goal:
R : Type u_1
inst : Semiring R
p : R[X]ᵐᵒᵖ
p0 : p = 0
⊢ natDegree.{u_1} (R := Rᵐᵒᵖ) ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p) = (unop p).natDegree

Tactic:
simp only [p0, map_zero, natDegree_zero, unop_zero]

Premises used: map_zero, Polynomial.natDegree_zero, MulOpposite.unop_zero
-- Module: Mathlib.RingTheory.Polynomial.Opposites
Goal:
R : Type u_1
inst : Semiring R
p : R[X]ᵐᵒᵖ
p0 : ¬p = 0
⊢ natDegree.{u_1} (R := Rᵐᵒᵖ) ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p) = (unop p).natDegree

Tactic:
simp only [p0, natDegree_eq_support_max', Ne, EmbeddingLike.map_eq_zero_iff, not_false_iff,
      support_opRingEquiv, unop_eq_zero_iff]

Premises used: Polynomial.natDegree_eq_support_max', Ne, Polynomial.support_opRingEquiv, not_false_iff, EmbeddingLike.map_eq_zero_iff, MulOpposite.unop_eq_zero_iff
-- Module: Mathlib.RingTheory.Polynomial.Opposites
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
rw₃ rw₄ : op ((unop p).coeff (unop p).natDegree) = op ((unop p).coeff (unop p).natDegree)
⊢ leadingCoeff ((opRingEquiv R : (a : R[X]ᵐᵒᵖ) → Rᵐᵒᵖ[X]) p) = op (unop p).leadingCoeff

Tactic:
rw [leadingCoeff, coeff_opRingEquiv, natDegree_opRingEquiv, leadingCoeff]

Premises used: Polynomial.leadingCoeff, Polynomial.coeff_opRingEquiv, Polynomial.natDegree_opRingEquiv
-- Module: Mathlib.RingTheory.Polynomial.Opposites
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)
⊢ Nontrivial R

Tactic:
nontriviality R
-- Module: Mathlib.RingTheory.Polynomial.Opposites
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
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])
⊢ 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:
simp only [trinomial, mul_add, add_mul, ← C_mul', C_1, one_mul, ← mul_assoc, X_mul_C, C_add]

Premises used: add_mul, Polynomial.C_1, Polynomial.C_mul', Polynomial.X_mul_C, mul_assoc, mul_add, Polynomial.C_add, one_mul
-- Module: Mathlib.RingTheory.Polynomial.Opposites
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
noncomm_ring noncomm_ring₁ noncomm_ring₂ 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])
⊢ 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:
noncomm_ring
-- Module: Mathlib.RingTheory.Polynomial.Opposites
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])

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
-- Module: Mathlib.RingTheory.Polynomial.Opposites
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
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])
⊢ 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))

Tactic:
simp_rw [ht, eq]
-- Module: Mathlib.RingTheory.Polynomial.Opposites
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])
⊢ b = c

Tactic:
simpa [trinomial] using congr_arg (coeff · 1) <|
        h.1 (a₁ := trinomial b) (a₂ := trinomial c) (X_add_C_ne_zero 1) <| by simp_rw [ht, eq]

Premises used: Polynomial.X_add_C_ne_zero, IsLeftCancelMulZero.mul_left_cancel_of_ne_zero, Polynomial.coeff, congr_arg, OfNat.ofNat
-- Module: Mathlib.RingTheory.Polynomial.Opposites
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
rw₃ : IsRightCancelMulZero R ∧ IsCancelAdd.{u_1} Rᵐᵒᵖ ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
rw₄ rw₅ : IsRightCancelMulZero R ∧ IsCancelAdd R ↔ IsRightCancelMulZero R ∧ IsCancelAdd R
⊢ IsRightCancelMulZero.{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]

Premises used: Polynomial.isLeftCancelMulZero_iff, RingEquiv.toMulEquiv, MulEquiv.isLeftCancelMulZero_iff, Polynomial.opRingEquiv, MulOpposite.isCancelAdd_iff, MulOpposite.isLeftCancelMulZero_iff
-- Module: Mathlib.RingTheory.Polynomial.Opposites
Goal:
R : Type u_1
inst : Semiring R
simp_rw :
  (IsLeftCancelMulZero R ∧ IsCancelAdd R) ∧ IsRightCancelMulZero R ∧ IsCancelAdd R ↔
    (IsLeftCancelMulZero R ∧ IsRightCancelMulZero R) ∧ IsCancelAdd R
⊢ IsCancelMulZero.{u_1} R[X] ↔ IsCancelMulZero R ∧ IsCancelAdd R

Tactic:
simp_rw [isCancelMulZero_iff, isLeftCancelMulZero_iff, isRightCancelMulZero_iff]

Premises used: Polynomial.isLeftCancelMulZero_iff, isCancelMulZero_iff, Polynomial.isRightCancelMulZero_iff
-- Module: Mathlib.RingTheory.Polynomial.Opposites
Goal:
R : Type u_1
inst : Semiring R
rw :
  (IsLeftCancelMulZero R ∧ IsRightCancelMulZero R) ∧ IsCancelAdd R ∧ IsCancelAdd R ↔
    (IsLeftCancelMulZero R ∧ IsRightCancelMulZero R) ∧ IsCancelAdd R
rw₁ rw₂ :
  (IsLeftCancelMulZero R ∧ IsRightCancelMulZero R) ∧ IsCancelAdd R ↔
    (IsLeftCancelMulZero R ∧ IsRightCancelMulZero R) ∧ IsCancelAdd R
⊢ (IsLeftCancelMulZero R ∧ IsCancelAdd R) ∧ IsRightCancelMulZero R ∧ IsCancelAdd R ↔
    (IsLeftCancelMulZero R ∧ IsRightCancelMulZero R) ∧ IsCancelAdd R

Tactic:
rw [and_and_and_comm, and_self]

Premises used: and_self, and_and_and_comm
-- Module: Mathlib.RingTheory.Polynomial.Opposites
Goal:
R : Type u_1
inst : Semiring R
simp_rw : IsCancelMulZero.{u_1} R[X] ∧ Nontrivial.{u_1} R[X] ↔ (IsCancelMulZero R ∧ Nontrivial R) ∧ IsCancelAdd R
simp_rw₁ : IsCancelMulZero.{u_1} R[X] ∧ Nontrivial R ↔ (IsCancelMulZero R ∧ Nontrivial R) ∧ IsCancelAdd R
simp_rw₂ : (IsCancelMulZero R ∧ IsCancelAdd R) ∧ Nontrivial R ↔ (IsCancelMulZero R ∧ Nontrivial R) ∧ IsCancelAdd R
⊢ IsDomain.{u_1} R[X] ↔ IsDomain R ∧ IsCancelAdd R

Tactic:
simp_rw [isDomain_iff_cancelMulZero_and_nontrivial, nontrivial_iff,
    Polynomial.isCancelMulZero_iff, and_right_comm]

Premises used: isDomain_iff_cancelMulZero_and_nontrivial, Polynomial.isCancelMulZero_iff, Polynomial.nontrivial_iff, and_right_comm
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
⊢ Eq (α := S[X]) (ascPochhammer S 0) 1

Tactic:
rfl

Premises used: ascPochhammer, rfl
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
⊢ Eq (α := S[X]) (ascPochhammer S 1) X

Tactic:
simp [ascPochhammer]

Premises used: ascPochhammer
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
n : ℕ
rw rw₁ :
  X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1) = X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)
⊢ ascPochhammer S (n + 1) = X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)

Tactic:
rw [ascPochhammer]

Premises used: ascPochhammer
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
inst_1 : Nontrivial S
inst_2 : NoZeroDivisors S
⊢ Monic (ascPochhammer S 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
inst_1 : Nontrivial S
inst_2 : NoZeroDivisors S
n : ℕ
hn : Monic (ascPochhammer S n)
⊢ (HAdd.hAdd (α := S[X]) X 1).leadingCoeff = 1

Tactic:
have : leadingCoeff (X + 1 : S[X]) = 1 := leadingCoeff_X_add_C 1
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
inst_1 : Nontrivial S
inst_2 : NoZeroDivisors S
n : ℕ
hn : Monic (ascPochhammer S n)
this : (HAdd.hAdd (α := S[X]) X 1).leadingCoeff = 1
succ : (X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).Monic
succ₁ : (X * comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).leadingCoeff = 1
succ₂ : leadingCoeff X * (comp (ascPochhammer S n) (HAdd.hAdd (α := S[X]) X 1)).leadingCoeff = 1
succ₃ :
  leadingCoeff X *
      (leadingCoeff (ascPochhammer S n) * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n)) =
    1
succ₄ : leadingCoeff X * (1 * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n)) = 1
succ₅ : 1 * (1 * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n)) = 1
succ₆ : 1 * (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n) = 1
succ₇ : (HAdd.hAdd (α := S[X]) X 1).leadingCoeff ^ natDegree (ascPochhammer S n) = 1
succ₈ : HPow.hPow (α := S) 1 (natDegree (ascPochhammer S n)) = 1
succ₉ succ₁₀ : Eq.{u + 1} (α := S) 1 1
⊢ Monic (ascPochhammer S (n + 1))

Tactic:
rw [ascPochhammer_succ_left, Monic.def, leadingCoeff_mul,
      leadingCoeff_comp (ne_zero_of_eq_one <| natDegree_X_add_C 1 : natDegree (X + 1) ≠ 0), hn,
      monic_X, one_mul, one_mul, this, one_pow]

Premises used: one_pow, ne_zero_of_eq_one, Polynomial.leadingCoeff_mul, Polynomial.natDegree_X_add_C, Polynomial.leadingCoeff_comp, Polynomial.Monic.def, OfNat.ofNat, ascPochhammer_succ_left, one_mul, Polynomial.monic_X
-- Module: Mathlib.RingTheory.Polynomial.Pochhammer
Goal:
S : Type u
inst : Semiring S
n : ℕ
inst_1 : Nontrivial S
inst_2 : NoZeroDivisors S
zero : Monic (ascPochhammer S 0)
succ : ∀ (n : ℕ) (hn : Monic (ascPochhammer S n)), Monic (ascPochhammer S (n + 1))
⊢ Monic (ascPochhammer S n)

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    have : leadingCoeff (X + 1 : S[X]) = 1 := leadingCoeff_X_add_C 1
    rw [ascPochhammer_succ_left, Monic.def, leadingCoeff_mul,
      leadingCoeff_comp (ne_zero_of_eq_one <| natDegree_X_add_C 1 : natDegree (X + 1) ≠ 0), hn,
      monic_X, one_mul, one_mul, this, one_pow]

Premises used: one_pow, ne_zero_of_eq_one, Polynomial.leadingCoeff_mul, Polynomial.natDegree_X_add_C, Polynomial.leadingCoeff_comp, Polynomial.Monic.def, OfNat.ofNat, ascPochhammer_succ_left, one_mul, Polynomial.monic_X