awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Ring R
p q : R[X]
⊢ (-p).comp q = -p.comp q

Tactic:
eval₂_neg _

Premises used: Polynomial.eval₂_neg, Polynomial.comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Ring R
p q r : R[X]
⊢ (p - q).comp r = p.comp r - q.comp r

Tactic:
eval₂_sub _

Premises used: Polynomial.eval₂_sub, Polynomial.comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Ring R
p : R[X]
i : ℤ
ofNat : ∀ (a : ℕ), comp (↑(Int.ofNat a) : R[X]) p = (↑(Int.ofNat a) : R[X])
negSucc : ∀ (a : ℕ), comp (↑(Int.negSucc a) : R[X]) p = (↑(Int.negSucc a) : R[X])
⊢ comp (↑i : R[X]) p = (↑i : R[X])

Tactic:
cases i
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Ring R
p : R[X]
a : ℕ
⊢ comp (↑(Int.ofNat a) : R[X]) p = (↑(Int.ofNat a) : R[X])

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Ring R
p : R[X]
a : ℕ
⊢ comp (↑(Int.negSucc a) : R[X]) p = (↑(Int.negSucc a) : R[X])

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Ring R
p : R[X]
S : Type u_1
inst_1 : Ring S
f : R →+* S
n : ℤ
⊢ eval₂ f ((f : (a : R) → S) (↑n : R)) p = (f : (a : R) → S) (eval (↑n : R) p)

Tactic:
eval₂_at_apply (p := p) f n

Premises used: Int.cast, Polynomial.eval₂_at_apply
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Ring R
p : R[X]
S : Type u_1
inst_1 : Ring S
f : R →+* S
n : ℤ
h : Eq.{u_1 + 1} (α := S) ((↑n : S) : S) ((f : (a : R) → S) (↑n : R) : S)
⊢ eval₂ f (↑n : S) p = (f : (a : R) → S) (eval (↑n : R) p)

Tactic:
convert! eval₂_at_apply (p := p) f n

Premises used: Int.cast, Polynomial.eval₂_at_apply
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Ring R
p : R[X]
S : Type u_1
inst_1 : Ring S
f : R →+* S
n : ℤ
⊢ Eq.{u_1 + 1} (α := S) ((↑n : S) : S) ((f : (a : R) → S) (↑n : R) : S)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Eval.Defs
Goal:
R : Type u
inst : Ring R
p q : R[X]
n : ℕ
rw : (p * X - p * (↑n : R[X])).comp q = p.comp q * (q - (↑n : R[X]))
rw₁ : (p * X).comp q - (p * (↑n : R[X])).comp q = p.comp q * (q - (↑n : R[X]))
rw₂ : p.comp q * q - (p * (↑n : R[X])).comp q = p.comp q * (q - (↑n : R[X]))
rw₃ : p.comp q * q - ((↑n : R[X]) * p).comp q = p.comp q * (q - (↑n : R[X]))
rw₄ : p.comp q * q - (↑n : R[X]) * p.comp q = p.comp q * (q - (↑n : R[X]))
rw₅ : p.comp q * q - p.comp q * (↑n : R[X]) = p.comp q * (q - (↑n : R[X]))
rw₆ rw₇ : p.comp q * q - p.comp q * (↑n : R[X]) = p.comp q * q - p.comp q * (↑n : R[X])
⊢ (p * HSub.hSub (α := R[X]) X (↑n : R[X])).comp q = p.comp q * (q - (↑n : R[X]))

Tactic:
rw [mul_sub, sub_comp, mul_X_comp, ← Nat.cast_comm, natCast_mul_comp, Nat.cast_comm, mul_sub]

Premises used: Nat.cast_comm, mul_sub, Polynomial.mul_X_comp, Polynomial.natCast_mul_comp, Polynomial.sub_comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
x : S
⊢ Eq.{v + 1} (α := (i : ℕ) → S) (fun (i : ℕ) ↦ eval₂ f x ((monomial i : (a : R) → R[X]) (p.coeff i))) fun (i : ℕ) ↦
    HMul.hMul (α := S) ((f : (a : R) → S) (p.coeff i) : S) (x ^ i)

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
rw : ∀ (n : ℕ), HMul.hMul (α := S) ((f : (a : R) → S) 0 : S) (x ^ n) = 0
⊢ eval₂ f x p = ∑ i ∈ range n, HMul.hMul (α := S) ((f : (a : R) → S) (p.coeff i) : S) (x ^ i)

Tactic:
rw [eval₂_eq_sum, p.sum_over_range' _ _ hn]

Premises used: Polynomial.sum_over_range', Polynomial.eval₂_eq_sum
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
i : ℕ
rw : 0 * x ^ i = 0
rw₁ rw₂ : Eq.{v + 1} (α := S) 0 0
⊢ HMul.hMul (α := S) ((f : (a : R) → S) 0 : S) (x ^ i) = 0

Tactic:
rw [f.map_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, RingHom.map_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : R
h : ∀ (n : ℕ), 0 * x ^ n = 0
⊢ eval x p = ∑ i ∈ range (p.natDegree + 1), p.coeff i * x ^ i

Tactic:
rw [eval_eq_sum, sum_over_range]

Premises used: Polynomial.eval_eq_sum, Polynomial.sum_over_range
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : R
⊢ ∀ (n : ℕ), 0 * x ^ n = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
x : R
rw : ∀ (n : ℕ), 0 * x ^ n = 0
⊢ eval x p = ∑ i ∈ range n, p.coeff i * x ^ i

Tactic:
rw [eval_eq_sum, p.sum_over_range' _ _ hn]

Premises used: Polynomial.eval_eq_sum, Polynomial.sum_over_range'
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
x : R
⊢ ∀ (n : ℕ), 0 * x ^ n = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
S : Type v
inst : CommRing S
d : ℕ
y : S
⊢ HAdd.hAdd (α := S) (↑d : S) 1 = (↑d.succ : S)

Tactic:
simp only [Nat.cast_succ]

Premises used: Nat.cast_succ
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
S : Type v
inst : CommRing S
d : ℕ
y : S
⊢ HAdd.hAdd (α := S) (↑d : S) 1 = (↑d.succ : S)

Tactic:
have cast_succ : (d + 1 : S) = ((d.succ : ℕ) : S) := by simp only [Nat.cast_succ]
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
S : Type v
inst : CommRing S
d : ℕ
y : S
cast_succ : HAdd.hAdd (α := S) (↑d : S) 1 = (↑d.succ : S)
rw :
  HMul.hMul (α := S) (↑d.succ : S) (∑ m ∈ range (d + 1), y ^ m * HPow.hPow (α := S) 1 (d - m) * (↑(d.choose m) : S)) -
      (↑d.succ : S) * y ^ d =
    ∑ x_1 ∈ range (d + 1), (↑((d + 1).choose x_1) : S) * ((↑x_1 : S) * y ^ (x_1 - 1))
⊢ eval (1 + y) ((monomial d : (a : S) → S[X]) (HAdd.hAdd (α := S) (↑d : S) 1)) -
      eval y ((monomial d : (a : S) → S[X]) (HAdd.hAdd (α := S) (↑d : S) 1)) =
    ∑ x_1 ∈ range (d + 1), (↑((d + 1).choose x_1) : S) * ((↑x_1 : S) * y ^ (x_1 - 1))

Tactic:
rw [cast_succ, eval_monomial, eval_monomial, add_comm, add_pow]

Premises used: add_comm, add_pow, Polynomial.eval_monomial
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
S : Type v
inst : CommRing S
d : ℕ
y : S
cast_succ : HAdd.hAdd (α := S) (↑d : S) 1 = (↑d.succ : S)
simp :
  HMul.hMul (α := S) (↑d.succ : S) (∑ x ∈ range (d + 1), (↑(d.choose x) : S) * y ^ x) - (↑d.succ : S) * y ^ d =
    ∑ x_1 ∈ range (d + 1), (↑((d + 1).choose x_1) : S) * ((↑x_1 : S) * y ^ (x_1 - 1))
⊢ HMul.hMul (α := S) (↑d.succ : S) (∑ m ∈ range (d + 1), y ^ m * HPow.hPow (α := S) 1 (d - m) * (↑(d.choose m) : S)) -
      (↑d.succ : S) * y ^ d =
    ∑ x_1 ∈ range (d + 1), (↑((d + 1).choose x_1) : S) * ((↑x_1 : S) * y ^ (x_1 - 1))

Tactic:
simp only [one_pow, mul_one, mul_comm (y ^ _) (d.choose _)]

Premises used: one_pow, Nat.choose, Nat.cast, HPow.hPow, mul_comm, mul_one
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
S : Type v
inst : CommRing S
d : ℕ
y : S
cast_succ : HAdd.hAdd (α := S) (↑d : S) 1 = (↑d.succ : S)
rw :
  Eq.{v + 1} (α := S) (∑ i ∈ range d, (↑d.succ : S) * ((↑(d.choose i) : S) * y ^ i))
    (∑ k ∈ range d, (↑((d + 1).choose (k + 1)) : S) * ((↑(k + 1) : S) * y ^ (k + 1 - 1)))
⊢ HMul.hMul (α := S) (↑d.succ : S) (∑ x ∈ range (d + 1), (↑(d.choose x) : S) * y ^ x) - (↑d.succ : S) * y ^ d =
    ∑ x_1 ∈ range (d + 1), (↑((d + 1).choose x_1) : S) * ((↑x_1 : S) * y ^ (x_1 - 1))

Tactic:
rw [sum_range_succ, mul_add, Nat.choose_self, Nat.cast_one, one_mul, add_sub_cancel_right,
    mul_sum, sum_range_succ', Nat.cast_zero, zero_mul, mul_zero, add_zero]

Premises used: Finset.mul_sum, MulZeroClass.zero_mul, MulZeroClass.mul_zero, mul_add, Nat.cast_zero, add_sub_cancel_right, add_zero, Nat.cast_one, Finset.sum_range_succ', Finset.sum_range_succ, Nat.choose_self, one_mul
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
S : Type v
inst : CommRing S
d : ℕ
y : S
cast_succ : HAdd.hAdd (α := S) (↑d : S) 1 = (↑d.succ : S)
⊢ Eq.{v + 1} (α := S) (∑ i ∈ range d, (↑d.succ : S) * ((↑(d.choose i) : S) * y ^ i))
    (∑ k ∈ range d, (↑((d + 1).choose (k + 1)) : S) * ((↑(k + 1) : S) * y ^ (k + 1 - 1)))

Tactic:
sum_congr rfl fun y _hy => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
S : Type v
inst : CommRing S
d : ℕ
y : S
cast_succ : HAdd.hAdd (α := S) (↑d : S) 1 = (↑d.succ : S)
refine :
  ∀ (y_1 : ℕ) (_hy : y_1 ∈ range d),
    (↑d.succ : S) * ((↑(d.choose y_1) : S) * y ^ y_1) =
      (↑((d + 1).choose (y_1 + 1)) : S) * ((↑(y_1 + 1) : S) * y ^ (y_1 + 1 - 1))
⊢ Eq.{v + 1} (α := S) (∑ i ∈ range d, (↑d.succ : S) * ((↑(d.choose i) : S) * y ^ i))
    (∑ k ∈ range d, (↑((d + 1).choose (k + 1)) : S) * ((↑(k + 1) : S) * y ^ (k + 1 - 1)))

Tactic:
refine sum_congr rfl fun y _hy => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
S : Type v
inst : CommRing S
d : ℕ
y_1 : S
cast_succ : HAdd.hAdd (α := S) (↑d : S) 1 = (↑d.succ : S)
y : ℕ
_hy : y ∈ range d
rw :
  HMul.hMul (α := S) (↑d.succ : S) (↑(d.choose y) : S) * y_1 ^ y =
    (↑((d + 1).choose (y + 1)) : S) * ((↑(y + 1) : S) * y_1 ^ (y + 1 - 1))
rw₁ :
  HMul.hMul (α := S) (↑d.succ : S) (↑(d.choose y) : S) * y_1 ^ y =
    HMul.hMul (α := S) (↑((d + 1).choose (y + 1)) : S) (↑(y + 1) : S) * y_1 ^ (y + 1 - 1)
rw₂ :
  (↑(d.succ * d.choose y) : S) * y_1 ^ y =
    HMul.hMul (α := S) (↑((d + 1).choose (y + 1)) : S) (↑(y + 1) : S) * y_1 ^ (y + 1 - 1)
rw₃ :
  (↑((d + 1).choose (y + 1) * (y + 1)) : S) * y_1 ^ y =
    HMul.hMul (α := S) (↑((d + 1).choose (y + 1)) : S) (↑(y + 1) : S) * y_1 ^ (y + 1 - 1)
rw₄ :
  HMul.hMul (α := S) (↑((d + 1).choose (y + 1)) : S) (↑(y + 1) : S) * y_1 ^ y =
    HMul.hMul (α := S) (↑((d + 1).choose (y + 1)) : S) (↑(y + 1) : S) * y_1 ^ (y + 1 - 1)
rw₅ rw₆ :
  HMul.hMul (α := S) (↑((d + 1).choose (y + 1)) : S) (↑(y + 1) : S) * y_1 ^ y =
    HMul.hMul (α := S) (↑((d + 1).choose (y + 1)) : S) (↑(y + 1) : S) * y_1 ^ y
⊢ (↑d.succ : S) * ((↑(d.choose y) : S) * y_1 ^ y) =
    (↑((d + 1).choose (y + 1)) : S) * ((↑(y + 1) : S) * y_1 ^ (y + 1 - 1))

Tactic:
rw [← mul_assoc, ← mul_assoc, ← Nat.cast_mul, Nat.add_one_mul_choose_eq, Nat.cast_mul,
    Nat.add_sub_cancel]

Premises used: mul_assoc, Nat.cast_mul, Nat.add_one_mul_choose_eq, Nat.add_sub_cancel
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
rw :
  (p.sum fun (a : ℕ) (b : R) ↦
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (q ^ a)).coeff (p.natDegree * q.natDegree)) =
    p.leadingCoeff * q.leadingCoeff ^ p.natDegree
⊢ (p.comp q).coeff (p.natDegree * q.natDegree) = p.leadingCoeff * q.leadingCoeff ^ p.natDegree

Tactic:
rw [comp, eval₂_def, coeff_sum]

Premises used: Polynomial.eval₂_def, Polynomial.coeff_sum, Polynomial.comp
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ (p.sum fun (a : ℕ) (b : R) ↦
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (q ^ a)).coeff (p.natDegree * q.natDegree)) =
    p.leadingCoeff * q.leadingCoeff ^ p.natDegree

Tactic:
Eq.trans (Finset.sum_eq_single p.natDegree ?h₀ ?h₁) ?h₂

Premises used: Finset.sum_eq_single, Polynomial.natDegree, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
refine :
  ∀ b ∈ p.support,
    b ≠ p.natDegree →
      Eq.{u + 1} (α := R)
        ((fun (a : ℕ) (b : R) ↦
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (q ^ a)).coeff (p.natDegree * q.natDegree))
          b (p.coeff b))
        0
refine₁ :
  p.natDegree ∉ p.support →
    Eq.{u + 1} (α := R)
      ((fun (a : ℕ) (b : R) ↦
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (q ^ a)).coeff (p.natDegree * q.natDegree))
        p.natDegree (p.coeff p.natDegree))
      0
refine₂ :
  (fun (a : ℕ) (b : R) ↦
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (q ^ a)).coeff (p.natDegree * q.natDegree))
      p.natDegree (p.coeff p.natDegree) =
    p.leadingCoeff * q.leadingCoeff ^ p.natDegree
⊢ (p.sum fun (a : ℕ) (b : R) ↦
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (q ^ a)).coeff (p.natDegree * q.natDegree)) =
    p.leadingCoeff * q.leadingCoeff ^ p.natDegree

Tactic:
refine Eq.trans (Finset.sum_eq_single p.natDegree ?h₀ ?h₁) ?h₂

Premises used: Finset.sum_eq_single, Polynomial.natDegree, Eq.trans
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ (fun (a : ℕ) (b : R) ↦
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (q ^ a)).coeff (p.natDegree * q.natDegree))
      p.natDegree (p.coeff p.natDegree) =
    p.leadingCoeff * q.leadingCoeff ^ p.natDegree

Tactic:
simp only [coeff_natDegree, coeff_C_mul, coeff_pow_mul_natDegree]

Premises used: Polynomial.coeff_natDegree, Polynomial.coeff_C_mul, Polynomial.coeff_pow_mul_natDegree
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ (fun (a : ℕ) (b : R) ↦
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (q ^ a)).coeff (p.natDegree * q.natDegree))
      p.natDegree (p.coeff p.natDegree) =
    p.leadingCoeff * q.leadingCoeff ^ p.natDegree

Tactic:
case h₂ =>
    simp only [coeff_natDegree, coeff_C_mul, coeff_pow_mul_natDegree]

Premises used: Polynomial.coeff_natDegree, Polynomial.coeff_C_mul, Polynomial.coeff_pow_mul_natDegree
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ Eq.{u + 1} (α := R)
    ((fun (a : ℕ) (b : R) ↦
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (q ^ a)).coeff (p.natDegree * q.natDegree))
      b (p.coeff b))
    0

Tactic:
coeff_eq_zero_of_natDegree_lt (natDegree_mul_le.trans_lt ?_)

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt, Polynomial.natDegree_mul_le, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
refine : natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff b)) + (q ^ b).natDegree < p.natDegree * q.natDegree
⊢ Eq.{u + 1} (α := R)
    ((fun (a : ℕ) (b : R) ↦
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (q ^ a)).coeff (p.natDegree * q.natDegree))
      b (p.coeff b))
    0

Tactic:
refine coeff_eq_zero_of_natDegree_lt (natDegree_mul_le.trans_lt ?_)

Premises used: Polynomial.coeff_eq_zero_of_natDegree_lt, Polynomial.natDegree_mul_le, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
rw : (q ^ b).natDegree < p.natDegree * q.natDegree
⊢ natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff b)) + (q ^ b).natDegree < p.natDegree * q.natDegree

Tactic:
rw [natDegree_C, zero_add]

Premises used: Polynomial.natDegree_C, zero_add
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ (q ^ b).natDegree < p.natDegree * q.natDegree

Tactic:
natDegree_pow_le.trans_lt ?_

Premises used: Polynomial.natDegree_pow_le, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
refine : b * q.natDegree < p.natDegree * q.natDegree
⊢ (q ^ b).natDegree < p.natDegree * q.natDegree

Tactic:
refine natDegree_pow_le.trans_lt ?_

Premises used: Polynomial.natDegree_pow_le, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
hbc : b < p.natDegree
⊢ b * q.natDegree < p.natDegree * q.natDegree

Tactic:
gcongr
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ b < p.natDegree

Tactic:
lt_of_le_of_ne (le_natDegree_of_mem_supp _ hbs) hbp

Premises used: Polynomial.le_natDegree_of_mem_supp, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ b < p.natDegree

Tactic:
exact lt_of_le_of_ne (le_natDegree_of_mem_supp _ hbs) hbp

Premises used: Polynomial.le_natDegree_of_mem_supp, lt_of_le_of_ne
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ ∀ b ∈ p.support,
    b ≠ p.natDegree →
      Eq.{u + 1} (α := R)
        ((fun (a : ℕ) (b : R) ↦
            (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (q ^ a)).coeff (p.natDegree * q.natDegree))
          b (p.coeff b))
        0

Tactic:
case h₀ =>
    intro b hbs hbp
    refine coeff_eq_zero_of_natDegree_lt (natDegree_mul_le.trans_lt ?_)
    rw [natDegree_C, zero_add]
    refine natDegree_pow_le.trans_lt ?_
    gcongr
    exact lt_of_le_of_ne (le_natDegree_of_mem_supp _ hbs) hbp

Premises used: Polynomial.natDegree_C, zero_add, Polynomial.natDegree_pow_le, Polynomial.coeff_eq_zero_of_natDegree_lt, Polynomial.natDegree_mul_le, LE.le.trans_lt
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ p.natDegree ∉ p.support →
    Eq.{u + 1} (α := R)
      ((fun (a : ℕ) (b : R) ↦
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (q ^ a)).coeff (p.natDegree * q.natDegree))
        p.natDegree (p.coeff p.natDegree))
      0

Tactic:
simp +contextual
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ p.natDegree ∉ p.support →
    Eq.{u + 1} (α := R)
      ((fun (a : ℕ) (b : R) ↦
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) (q ^ a)).coeff (p.natDegree * q.natDegree))
        p.natDegree (p.coeff p.natDegree))
      0

Tactic:
case h₁ =>
    simp +contextual
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p : R[X]
r : R
n : ℕ
simp_rw : ∑ x ∈ range (p.natDegree + 1), p.coeff x * (r ^ x * if n = x then 1 else 0) = p.coeff n * r ^ n
⊢ (p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X)).coeff n = p.coeff n * r ^ n

Tactic:
simp_rw [comp, eval₂_eq_sum_range, (commute_X _).symm.mul_pow,
    ← C_pow, finsetSum_coeff, coeff_C_mul, coeff_X_pow]

Premises used: Polynomial.coeff_X_pow, Polynomial.coeff_C_mul, Polynomial.finsetSum_coeff, Polynomial.commute_X, Commute.symm, Commute.mul_pow, Polynomial.eval₂_eq_sum_range, Polynomial.comp, Polynomial.C_pow
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p : R[X]
r : R
n : ℕ
rw : ∀ b ∈ range (p.natDegree + 1), b ≠ n → p.coeff b * (r ^ b * if n = b then 1 else 0) = 0
rw₁ : ∀ (h : n ∉ range (p.natDegree + 1)), p.coeff n * (r ^ n * if n = n then 1 else 0) = 0
⊢ ∑ x ∈ range (p.natDegree + 1), p.coeff x * (r ^ x * if n = x then 1 else 0) = p.coeff n * r ^ n

Tactic:
rw [Finset.sum_eq_single n _ fun h ↦ ?_, if_pos rfl, mul_one]

Premises used: if_pos, Finset.sum_eq_single, mul_one, rfl
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p : R[X]
r : R
n b : ℕ
_ : b ∈ range (p.natDegree + 1) → b ≠ n → p.coeff b * (r ^ b * if n = b then 1 else 0) = 0
⊢ b ∈ range (p.natDegree + 1) → b ≠ n → p.coeff b * (r ^ b * if n = b then 1 else 0) = 0

Tactic:
_
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p : R[X]
r : R
n b : ℕ
h_1 : b ∈ range (p.natDegree + 1)
h : b ≠ n
simp_rw : p.coeff b * (r ^ b * 0) = 0
⊢ p.coeff b * (r ^ b * if n = b then 1 else 0) = 0

Tactic:
simp_rw [if_neg h.symm, mul_zero]

Premises used: Ne.symm, MulZeroClass.mul_zero, if_neg
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
rw : p.natDegree < n
⊢ p.coeff n * (r ^ n * if n = n then 1 else 0) = 0

Tactic:
rw [coeff_eq_zero_of_natDegree_lt, zero_mul]

Premises used: MulZeroClass.zero_mul, Polynomial.coeff_eq_zero_of_natDegree_lt
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
rwa : ∀ (h : ¬n ≤ p.natDegree), p.natDegree < n
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : p.natDegree < n), p.natDegree < n
⊢ p.natDegree < n

Tactic:
rwa [Finset.mem_range_succ_iff, not_le] at h

Premises used: not_le, Finset.mem_range_succ_iff
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p : R[X]
r : R
hr : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) r
simp_rw :
  (∀ (n : ℕ), (p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X)).coeff n = coeff 0 n) ↔
    ∀ (n : ℕ), p.coeff n = coeff 0 n
⊢ p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X) = 0 ↔ p = 0

Tactic:
simp_rw [ext_iff]

Premises used: Polynomial.ext_iff
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p : R[X]
r : R
hr : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) r
⊢ (∀ (n : ℕ), (p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X)).coeff n = coeff 0 n) ↔
    ∀ (n : ℕ), p.coeff n = coeff 0 n

Tactic:
forall_congr' fun n ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p : R[X]
r : R
hr : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) r
refine :
  ∀ (n : ℕ),
    (p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X)).coeff n = coeff 0 n ↔
      p.coeff n = coeff 0 n
⊢ (∀ (n : ℕ), (p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X)).coeff n = coeff 0 n) ↔
    ∀ (n : ℕ), p.coeff n = coeff 0 n

Tactic:
refine forall_congr' fun n ↦ ?_

Premises used: forall_congr'
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
inst : Semiring R
p : R[X]
r : R
hr : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) r
n : ℕ
rw : p.coeff n * r ^ n = coeff 0 n ↔ p.coeff n = coeff 0 n
rw₁ : p.coeff n * r ^ n = 0 ↔ p.coeff n = 0
rw₂ rw₃ : p.coeff n = 0 ↔ p.coeff n = 0
⊢ (p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X)).coeff n = coeff 0 n ↔
    p.coeff n = coeff 0 n

Tactic:
rw [comp_C_mul_X_coeff, coeff_zero, mul_right_mem_nonZeroDivisors_eq_zero_iff (pow_mem hr _)]

Premises used: mul_right_mem_nonZeroDivisors_eq_zero_iff, Polynomial.comp_C_mul_X_coeff, pow_mem, Polynomial.coeff_zero
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst : Semiring R
p_1 q r : R[X]
inst_1 : Semiring S
f : R →+* S
p : R[X]
e : R ≃+* S
a₁ :
  ∀ (x : S[X]) (n : ℕ),
    Eq.{v + 1} (α := S)
      (coeff
        ((RingHom.comp (β := R[X]) (mapRingHom (↑e : R →+* S)) (mapRingHom (↑e.symm : S →+* R)) : (a : S[X]) → S[X]) x)
        n)
      (coeff ((RingHom.id S[X] : (a : S[X]) → S[X]) x) n)
⊢ Eq (α := S[X] →+* S[X]) (RingHom.comp (β := R[X]) (mapRingHom (↑e : R →+* S)) (mapRingHom (↑e.symm : S →+* R)))
    (RingHom.id S[X])

Tactic:
ext
-- Module: Mathlib.Algebra.Polynomial.Eval.Degree
Goal:
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst : Semiring R
p_1 q r : R[X]
inst_1 : Semiring S
f : R →+* S
p : R[X]
e : R ≃+* S
x : S[X]
n_1 : ℕ
⊢ Eq.{v + 1} (α := S)
    (coeff
      ((RingHom.comp (β := R[X]) (mapRingHom (↑e : R →+* S)) (mapRingHom (↑e.symm : S →+* R)) : (a : S[X]) → S[X]) x)
      n_1)
    (coeff ((RingHom.id S[X] : (a : S[X]) → S[X]) x) n_1)

Tactic:
simp