awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Identities
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k_1 : Type y
A : Type z
a b : R
m n : ℕ
inst : CommRing R
x y : R
k : ℕ
z : R
hz : x ^ (k + 1) - y ^ (k + 1) = z * (x - y)
a₁ :
  x ^ (k + 2) - y ^ (k + 2) + x * (z * (x - y)) - ((z * x + y ^ (k + 1)) * (x - y) + x * (x ^ (k + 1) - y ^ (k + 1))) =
    0
⊢ x ^ (k + 2) - y ^ (k + 2) = (z * x + y ^ (k + 1)) * (x - y)

Tactic:
linear_combination (norm := ring) x * hz
-- Module: Mathlib.Algebra.Polynomial.Identities
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst : CommRing R
f : R[X]
x y : R
refine : eval x f - eval y f = (f.sum fun (i : ℕ) (r : R) ↦ r * (↑(powSubPowFactor x y i) : R)) * (x - y)
⊢ { z : R // eval x f - eval y f = z * (x - y) }

Tactic:
refine ⟨f.sum fun i r => r * (powSubPowFactor x y i).val, ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Identities
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst : CommRing R
f : R[X]
x y : R
delta :
  eval₂ (RingHom.id R) x f - eval₂ (RingHom.id R) y f =
    (f.sum fun (i : ℕ) (r : R) ↦ r * (↑(powSubPowFactor x y i) : R)) * (x - y)
⊢ eval x f - eval y f = (f.sum fun (i : ℕ) (r : R) ↦ r * (↑(powSubPowFactor x y i) : R)) * (x - y)

Tactic:
delta eval

Premises used: Polynomial.eval
-- Module: Mathlib.Algebra.Polynomial.Identities
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst : CommRing R
f : R[X]
x y : R
rw :
  HSub.hSub (α := R) (f.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) a : R) (x ^ e))
      (f.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) a : R) (y ^ e)) =
    (f.sum fun (i : ℕ) (r : R) ↦ r * (↑(powSubPowFactor x y i) : R)) * (x - y)
⊢ eval₂ (RingHom.id R) x f - eval₂ (RingHom.id R) y f =
    (f.sum fun (i : ℕ) (r : R) ↦ r * (↑(powSubPowFactor x y i) : R)) * (x - y)

Tactic:
rw [eval₂_eq_sum, eval₂_eq_sum]

Premises used: Polynomial.eval₂_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Identities
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst : CommRing R
f : R[X]
x y : R
simp :
  Eq.{u + 1} (α := R)
    (∑ x_1 ∈ f.support,
      (HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) (f.coeff x_1) : R) (x ^ x_1) -
        HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) (f.coeff x_1) : R) (y ^ x_1)))
    (∑ i ∈ f.support, f.coeff i * (↑(powSubPowFactor x y i) : R) * (x - y))
⊢ HSub.hSub (α := R) (f.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) a : R) (x ^ e))
      (f.sum fun (e : ℕ) (a : R) ↦ HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) a : R) (y ^ e)) =
    (f.sum fun (i : ℕ) (r : R) ↦ r * (↑(powSubPowFactor x y i) : R)) * (x - y)

Tactic:
simp only [sum, ← Finset.sum_sub_distrib, Finset.sum_mul]

Premises used: Polynomial.sum, Finset.sum_sub_distrib, Finset.sum_mul
-- Module: Mathlib.Algebra.Polynomial.Identities
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst : CommRing R
f : R[X]
x y : R
dsimp :
  Eq.{u + 1} (α := R) (∑ x_1 ∈ f.support, (f.coeff x_1 * x ^ x_1 - f.coeff x_1 * y ^ x_1))
    (∑ i ∈ f.support, f.coeff i * (↑(powSubPowFactor x y i) : R) * (x - y))
⊢ Eq.{u + 1} (α := R)
    (∑ x_1 ∈ f.support,
      (HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) (f.coeff x_1) : R) (x ^ x_1) -
        HMul.hMul (α := R) ((RingHom.id R : (a : R) → R) (f.coeff x_1) : R) (y ^ x_1)))
    (∑ i ∈ f.support, f.coeff i * (↑(powSubPowFactor x y i) : R) * (x - y))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Polynomial.Identities
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst : CommRing R
f : R[X]
x y : R
e_f : ∀ (i : ℕ), f.coeff i * x ^ i - f.coeff i * y ^ i = f.coeff i * (↑(powSubPowFactor x y i) : R) * (x - y)
⊢ Eq.{u + 1} (α := R) (∑ x_1 ∈ f.support, (f.coeff x_1 * x ^ x_1 - f.coeff x_1 * y ^ x_1))
    (∑ i ∈ f.support, f.coeff i * (↑(powSubPowFactor x y i) : R) * (x - y))

Tactic:
congr with i
-- Module: Mathlib.Algebra.Polynomial.Identities
Goal:
R : Type u
S : Type v
T : Type w
ι : Type x
k : Type y
A : Type z
a b : R
m n : ℕ
inst : CommRing R
f : R[X]
x y : R
i : ℕ
e_f : f.coeff i * x ^ i - f.coeff i * y ^ i = f.coeff i * ((↑(powSubPowFactor x y i) : R) * (x - y))
e_f₁ : f.coeff i * x ^ i - f.coeff i * y ^ i = f.coeff i * (x ^ i - y ^ i)
e_f₂ e_f₃ : f.coeff i * x ^ i - f.coeff i * y ^ i = f.coeff i * x ^ i - f.coeff i * y ^ i
⊢ f.coeff i * x ^ i - f.coeff i * y ^ i = f.coeff i * (↑(powSubPowFactor x y i) : R) * (x - y)

Tactic:
rw [mul_assoc, ← (powSubPowFactor x y _).prop, mul_sub]

Premises used: mul_sub, mul_assoc, Subtype.prop, Polynomial.powSubPowFactor
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
rw : p.divX.coeff n = p.coeff (1 + n)
⊢ p.divX.coeff n = p.coeff (n + 1)

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
ofFinsupp :
  ∀ (toFinsupp : AddMonoidAlgebra R ℕ),
    { toFinsupp := toFinsupp : R[X] }.divX.coeff n = { toFinsupp := toFinsupp : R[X] }.coeff (1 + n)
⊢ p.divX.coeff n = p.coeff (1 + n)

Tactic:
cases p
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
n : ℕ
inst : Semiring R
toFinsupp : AddMonoidAlgebra R ℕ
⊢ { toFinsupp := toFinsupp : R[X] }.divX.coeff n = { toFinsupp := toFinsupp : R[X] }.coeff (1 + n)

Tactic:
rfl
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff 0 = p.coeff 0

Tactic:
simp [coeff_C, coeff_mul_X]

Premises used: Polynomial.coeff_mul_X, Polynomial.coeff_C
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff (n + 1) = p.coeff (n + 1)

Tactic:
simp [coeff_C, coeff_mul_X]

Premises used: Polynomial.coeff_mul_X, Polynomial.coeff_C
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ (HAdd.hAdd (β := R[X]) (X * p.divX) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff 0 = p.coeff 0

Tactic:
simp [coeff_C]

Premises used: Polynomial.coeff_C
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ (HAdd.hAdd (β := R[X]) (X * p.divX) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff (n + 1) = p.coeff (n + 1)

Tactic:
simp [coeff_C]

Premises used: Polynomial.coeff_C
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
⊢ Eq.{u + 1} (α := R) (coeff (divX ((C : (a : R) → R[X]) a)) n) (coeff 0 n)

Tactic:
simp [coeff_divX]

Premises used: Polynomial.coeff_divX
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.divX = 0
⊢ p = (C : (a : R) → R[X]) (p.coeff 0)

Tactic:
simpa [eq_comm, h] using divX_mul_X_add p

Premises used: Polynomial.divX_mul_X_add, eq_comm
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p = (C : (a : R) → R[X]) (p.coeff 0)
rw : Eq.{u + 1} (α := R[X]) (divX ((C : (a : R) → R[X]) (p.coeff 0))) 0
rw₁ rw₂ : Eq.{u + 1} (α := R[X]) 0 0
⊢ p.divX = 0

Tactic:
rw [h, divX_C]

Premises used: Polynomial.divX_C
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ ∀ (n : ℕ), (p + q).divX.coeff n = (p.divX + q.divX).coeff n

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
⊢ Eq.{u + 1} (α := R[X]) (divX 0) 0

Tactic:
leadingCoeff_eq_zero.mp rfl

Premises used: Iff.mp, Polynomial.leadingCoeff_eq_zero, rfl
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
a : ∀ (n : ℕ), Eq.{u + 1} (α := R) (coeff (divX 1) n) (coeff 0 n)
⊢ Eq.{u + 1} (α := R[X]) (divX 1) 0

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
n : ℕ
⊢ Eq.{u + 1} (α := R) (coeff (divX 1) n) (coeff 0 n)

Tactic:
simpa only [coeff_divX, coeff_zero] using coeff_one

Premises used: Polynomial.coeff_one, Polynomial.coeff_zero, Polynomial.coeff_divX
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
a₁ :
  ∀ (n : ℕ),
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).divX.coeff n =
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p.divX).coeff n
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).divX =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p.divX

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
n : ℕ
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).divX.coeff n =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p.divX).coeff n

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
n : ℕ
inst : Semiring R
zero :
  (HPow.hPow (α := R[X]) (β := ℕ) X 0).divX =
    if Eq (α := ℕ) 0 0 then 0 else HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 0 1)
succ : ∀ (n : ℕ), (HPow.hPow (α := R[X]) X (n + 1)).divX = if n + 1 = 0 then 0 else HPow.hPow (α := R[X]) X (n + 1 - 1)
⊢ (HPow.hPow (α := R[X]) X n).divX = if n = 0 then 0 else HPow.hPow (α := R[X]) X (n - 1)

Tactic:
cases n
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
⊢ (HPow.hPow (α := R[X]) (β := ℕ) X 0).divX =
    if Eq (α := ℕ) 0 0 then 0 else HPow.hPow (α := R[X]) X (HSub.hSub (α := ℕ) 0 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
n : ℕ
succ :
  ∀ (n_1 : ℕ),
    (HPow.hPow (α := R[X]) X (n + 1)).divX.coeff n_1 =
      (if n + 1 = 0 then 0 else HPow.hPow (α := R[X]) X (n + 1 - 1)).coeff n_1
⊢ (HPow.hPow (α := R[X]) X (n + 1)).divX = if n + 1 = 0 then 0 else HPow.hPow (α := R[X]) X (n + 1 - 1)

Tactic:
ext n
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
n_1 n : ℕ
⊢ (HPow.hPow (α := R[X]) X (n_1 + 1)).divX.coeff n =
    (if n_1 + 1 = 0 then 0 else HPow.hPow (α := R[X]) X (n_1 + 1 - 1)).coeff n

Tactic:
simp [coeff_X_pow]

Premises used: Polynomial.coeff_X_pow
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ (divX_hom : (a : R[X]) → R[X]) p = p.divX

Tactic:
rfl

Premises used: Polynomial.divX, rfl
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
φ_k : ∀ (f : R[X]), f.natDegree < 1 → Eq (α := R[X]) ((divX_hom : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
φ_mon :
  ∀ (n : ℕ) (c : R),
    c ≠ 0 → natDegree.{u} (R := R) ((divX_hom : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) c)) = n - 1
⊢ p.divX.natDegree = p.natDegree - 1

Tactic:
apply map_natDegree_eq_sub (φ := divX_hom)

Premises used: Polynomial.map_natDegree_eq_sub
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p f : R[X]
⊢ f.natDegree < 1 → Eq (α := R[X]) ((divX_hom : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])

Tactic:
simpa [divX_hom, divX_eq_zero_iff] using eq_C_of_natDegree_eq_zero

Premises used: Polynomial.divX_eq_zero_iff, Polynomial.eq_C_of_natDegree_eq_zero, Polynomial.divX_hom
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
φ_mon :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X])
        (if n = 0 then 0 else HPow.hPow (α := R[X]) X (n - 1))).natDegree =
    n - 1
⊢ natDegree.{u} (R := R) ((divX_hom : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) c)) = n - 1

Tactic:
rw [← C_mul_X_pow_eq_monomial, divX_hom_toFun, divX_C_mul, divX_X_pow]

Premises used: Polynomial.divX_X_pow, Polynomial.C_mul_X_pow_eq_monomial, Polynomial.divX_hom_toFun, Polynomial.divX_C_mul
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
pos : ∀ (n0 : n = 0), (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) (0 : R[X])).natDegree = n - 1
neg :
  ∀ (n0 : ¬n = 0),
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X (n - 1))).natDegree = n - 1
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X])
        (if n = 0 then 0 else HPow.hPow (α := R[X]) X (n - 1))).natDegree =
    n - 1

Tactic:
split_ifs with n0
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
n0 : n = 0
⊢ (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) c : R[X]) (0 : R[X])).natDegree = n - 1

Tactic:
simp [n0]
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
n0 : ¬n = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X (n - 1))).natDegree = n - 1

Tactic:
natDegree_C_mul_X_pow (n - 1) c c0

Premises used: HSub.hSub, Polynomial.natDegree_C_mul_X_pow, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
n0 : ¬n = 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X (n - 1))).natDegree = n - 1

Tactic:
exact natDegree_C_mul_X_pow (n - 1) c c0

Premises used: HSub.hSub, Polynomial.natDegree_C_mul_X_pow, OfNat.ofNat
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.divX.natDegree ≤ p.natDegree

Tactic:
natDegree_divX_eq_natDegree_tsub_one.trans_le (Nat.pred_le _)

Premises used: Eq.trans_le, Nat.pred_le, Polynomial.natDegree_divX_eq_natDegree_tsub_one
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).divX =
    if n = 0 then 0 else HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X (n - 1))

Tactic:
simp only [divX_C_mul, divX_X_pow, mul_ite, mul_zero]

Premises used: Polynomial.divX_X_pow, mul_ite, Polynomial.divX_C_mul, MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
⊢ Nontrivial R

Tactic:
haveI := Nontrivial.of_polynomial_ne hp0
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
rwa rwa₁ rwa₂ rwa₃ : p ≠ 0
⊢ Ne (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (0 : R[X])

Tactic:
rwa [← eq_C_of_degree_le_zero h]

Premises used: Polynomial.eq_C_of_degree_le_zero
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
⊢ Ne (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (0 : R[X])

Tactic:
have h' : C (p.coeff 0) ≠ 0 := by rwa [← eq_C_of_degree_le_zero h]
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
h' : Ne (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (0 : R[X])
rw : ⊥ < degree.{u} (R := R) ((C : (a : R) → R[X]) (coeff ((C : (a : R) → R[X]) (p.coeff 0)) 0))
⊢ p.divX.degree < (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).degree

Tactic:
rw [eq_C_of_degree_le_zero h, divX_C, degree_zero, zero_mul, zero_add]

Premises used: MulZeroClass.zero_mul, Polynomial.degree_zero, zero_add, Polynomial.eq_C_of_degree_le_zero, Polynomial.divX_C
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
h' : Ne (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (0 : R[X])
⊢ ¬Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) (coeff ((C : (a : R) → R[X]) (p.coeff 0)) 0)) 0

Tactic:
simpa using h'
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : p.degree ≤ 0
h' : Ne (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (0 : R[X])
⊢ ⊥ < degree.{u} (R := R) ((C : (a : R) → R[X]) (coeff ((C : (a : R) → R[X]) (p.coeff 0)) 0))

Tactic:
exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 <| by simpa using h'))

Premises used: mt, Ne.symm, Iff.mp, bot_le, Polynomial.degree_eq_bot, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬p.degree ≤ 0
⊢ p.divX ≠ 0

Tactic:
simpa [divX_eq_zero_iff, -not_le, degree_le_zero_iff] using h

Premises used: not_le, Polynomial.divX_eq_zero_iff, Polynomial.degree_le_zero_iff
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬p.degree ≤ 0
⊢ p.divX ≠ 0

Tactic:
have hXp0 : divX p ≠ 0 := by
          simpa [divX_eq_zero_iff, -not_le, degree_le_zero_iff] using h
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
⊢ p.divX.leadingCoeff * leadingCoeff X ≠ 0

Tactic:
simpa
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
⊢ p.divX.leadingCoeff * leadingCoeff X ≠ 0

Tactic:
have : leadingCoeff (divX p) * leadingCoeff X ≠ 0 := by simpa
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this_1 : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * leadingCoeff X ≠ 0
⊢ LT.lt (α := WithBot ℕ) 0 1

Tactic:
decide
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this_1 : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * leadingCoeff X ≠ 0
rw : 0 + degree.{u} (R := R) X ≤ p.divX.degree + degree.{u} (R := R) X
⊢ degree.{u} (R := R) X ≤ (p.divX * X).degree

Tactic:
rw [← zero_add (degree X), degree_mul' this]

Premises used: Polynomial.degree, zero_add, Polynomial.degree_mul', Polynomial.X
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this_1 : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * leadingCoeff X ≠ 0
rw : ¬p = (C : (a : R) → R[X]) (p.coeff 0)
⊢ 0 ≤ p.divX.degree

Tactic:
rw [zero_le_degree_iff, Ne, divX_eq_zero_iff]

Premises used: Polynomial.zero_le_degree_iff, Polynomial.divX_eq_zero_iff, Ne
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this_1 : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * leadingCoeff X ≠ 0
⊢ ¬p = (C : (a : R) → R[X]) (p.coeff 0)

Tactic:
fun h0 => h (h0.symm ▸ degree_C_le)

Premises used: Eq.rec, Eq.symm, Not, Polynomial.degree_C_le
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this_1 : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * leadingCoeff X ≠ 0
⊢ ¬p = (C : (a : R) → R[X]) (p.coeff 0)

Tactic:
exact fun h0 => h (h0.symm ▸ degree_C_le)
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this_1 : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * leadingCoeff X ≠ 0
⊢ 0 + degree.{u} (R := R) X ≤ p.divX.degree + degree.{u} (R := R) X

Tactic:
exact add_le_add
                (by rw [zero_le_degree_iff, Ne, divX_eq_zero_iff]
                    exact fun h0 => h (h0.symm ▸ degree_C_le))
                    le_rfl

Premises used: le_rfl, add_le_add
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this_1 : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this : p.divX.leadingCoeff * leadingCoeff X ≠ 0
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0)) < (p.divX * X).degree

Tactic:
have : degree (C (p.coeff 0)) < degree (divX p * X) :=
          calc
            degree (C (p.coeff 0)) ≤ 0 := degree_C_le
            _ < 1 := by decide
            _ = degree (X : R[X]) := degree_X.symm
            _ ≤ degree (divX p * X) := by
              rw [← zero_add (degree X), degree_mul' this]
              exact add_le_add
                (by rw [zero_le_degree_iff, Ne, divX_eq_zero_iff]
                    exact fun h0 => h (h0.symm ▸ degree_C_le))
                    le_rfl
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this_1 : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this_2 : p.divX.leadingCoeff * leadingCoeff X ≠ 0
this : degree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0)) < (p.divX * X).degree
rw : p.divX.degree < (p.divX * X).degree
⊢ p.divX.degree < (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).degree

Tactic:
rw [degree_add_eq_left_of_degree_lt this]

Premises used: Polynomial.degree_add_eq_left_of_degree_lt
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this_1 : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this_2 : p.divX.leadingCoeff * leadingCoeff X ≠ 0
this : degree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0)) < (p.divX * X).degree
⊢ p.divX.degree < (p.divX * X).degree

Tactic:
degree_lt_degree_mul_X hXp0

Premises used: Polynomial.degree_lt_degree_mul_X
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this_1 : Nontrivial R
h : ¬p.degree ≤ 0
hXp0 : p.divX ≠ 0
this_2 : p.divX.leadingCoeff * leadingCoeff X ≠ 0
this : degree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0)) < (p.divX * X).degree
⊢ p.divX.degree < (p.divX * X).degree

Tactic:
exact degree_lt_degree_mul_X hXp0

Premises used: Polynomial.degree_lt_degree_mul_X
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
⊢ (HAdd.hAdd (β := R[X]) (p.divX * X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).degree = p.degree

Tactic:
congr_arg _ (divX_mul_X_add _)

Premises used: Polynomial.divX_mul_X_add, congr_arg
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp0 : p ≠ 0
this : Nontrivial R
⊢ p.divX.degree < p.degree

Tactic:
calc
    degree (divX p) < (divX p * X + C (p.coeff 0)).degree :=
      if h : degree p ≤ 0 then by
        have h' : C (p.coeff 0) ≠ 0 := by rwa [← eq_C_of_degree_le_zero h]
        rw [eq_C_of_degree_le_zero h, divX_C, degree_zero, zero_mul, zero_add]
        exact lt_of_le_of_ne bot_le (Ne.symm (mt degree_eq_bot.1 <| by simpa using h'))
      else by
        have hXp0 : divX p ≠ 0 := by
          simpa [divX_eq_zero_iff, -not_le, degree_le_zero_iff] using h
        have : leadingCoeff (divX p) * leadingCoeff X ≠ 0 := by simpa
        have : degree (C (p.coeff 0)) < degree (divX p * X) :=
          calc
            degree (C (p.coeff 0)) ≤ 0 := degree_C_le
            _ < 1 := by decide
            _ = degree (X : R[X]) := degree_X.symm
            _ ≤ degree (divX p * X) := by
              rw [← zero_add (degree X), degree_mul' this]
              exact add_le_add
                (by rw [zero_le_degree_iff, Ne, divX_eq_zero_iff]
                    exact fun h0 => h (h0.symm ▸ degree_C_le))
                    le_rfl
        rw [degree_add_eq_left_of_degree_lt this]; exact degree_lt_degree_mul_X hXp0
    _ = degree p := congr_arg _ (divX_mul_X_add _)

Premises used: Polynomial.divX_mul_X_add, Polynomial.degree, Polynomial.divX, congr_arg
-- Module: Mathlib.Algebra.Polynomial.Inductions
Goal:
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst : Semiring R
p_1 q : R[X]
M : R[X] → Sort u_1
p : R[X]
M0 : M 0
MC : (p : R[X]) → (a : R) → p.coeff 0 = 0 → a ≠ 0 → M p → M (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
MX : (p : R[X]) → p ≠ 0 → M p → M (p * X)
this : DecidableEq R := Classical.decEq R
hp : ¬p = 0
have : (wf : p.divX.degree < p.degree) → M p
⊢ M p

Tactic:
have wf : degree (divX p) < degree p := degree_divX_lt hp