awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
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]))
⊢ (p * HSub.hSub (α := R[X]) X (↑n : R[X])).comp q = p.comp q * (q - (↑n : R[X]))
have rw₄ : p.comp q * q - (↑n : R[X]) * p.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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
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]))
⊢ (p * HSub.hSub (α := R[X]) X (↑n : R[X])).comp q = p.comp q * (q - (↑n : R[X]))
have rw₅ : p.comp q * q - p.comp q * (↑n : R[X]) = 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Defs (goal)
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]))
⊢ (p * HSub.hSub (α := R[X]) X (↑n : R[X])).comp q = p.comp q * (q - (↑n : R[X]))
have rw₆ : p.comp q * q - p.comp q * (↑n : R[X]) = p.comp q * q - p.comp q * (↑n : R[X])
Tactic: rw [mul_sub, sub_comp, mul_X_comp, ← Nat.cast_comm, natCast_mul_comp, Nat.cast_comm, mul_sub]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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
⊢ eval₂ f x p = ∑ i ∈ range n, HMul.hMul (α := S) ((f : (a : R) → S) (p.coeff i) : S) (x ^ i)
have rw : ∀ (n : ℕ), HMul.hMul (α := S) ((f : (a : R) → S) 0 : S) (x ^ n) = 0
Tactic: rw [eval₂_eq_sum, p.sum_over_range' _ _ hn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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 : ℕ
⊢ HMul.hMul (α := S) ((f : (a : R) → S) 0 : S) (x ^ i) = 0
have rw : 0 * x ^ i = 0
Tactic: rw [f.map_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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
⊢ HMul.hMul (α := S) ((f : (a : R) → S) 0 : S) (x ^ i) = 0
have rw₁ : Eq.{v + 1} (α := S) 0 0
Tactic: rw [f.map_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
x : R
⊢ eval x p = ∑ i ∈ range (p.natDegree + 1), p.coeff i * x ^ i
have h : ∀ (n : ℕ), 0 * x ^ n = 0
Tactic: rw [eval_eq_sum, sum_over_range]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hn : p.natDegree < n
x : R
⊢ eval x p = ∑ i ∈ range n, p.coeff i * x ^ i
have rw : ∀ (n : ℕ), 0 * x ^ n = 0
Tactic: rw [eval_eq_sum, p.sum_over_range' _ _ hn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (hypothesis)
Goal:
S : Type v
inst : CommRing S
d : ℕ
y : S
⊢ 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))
have cast_succ : 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
S : Type v
inst : CommRing S
d : ℕ
y : S
cast_succ : HAdd.hAdd (α := S) (↑d : S) 1 = (↑d.succ : S)
⊢ 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))
have 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))
Tactic: rw [cast_succ, eval_monomial, eval_monomial, add_comm, add_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
S : Type v
inst : CommRing S
d : ℕ
y : S
cast_succ : HAdd.hAdd (α := S) (↑d : S) 1 = (↑d.succ : S)
⊢ 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))
have 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))
Tactic: simp only [one_pow, mul_one, mul_comm (y ^ _) (d.choose _)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
S : Type v
inst : CommRing S
d : ℕ
y : S
cast_succ : HAdd.hAdd (α := S) (↑d : S) 1 = (↑d.succ : S)
⊢ 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))
have 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)))
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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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)))
have 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))
Tactic: refine sum_congr rfl fun y _hy => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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
⊢ (↑d.succ : S) * ((↑(d.choose y) : S) * y_1 ^ y) =
    (↑((d + 1).choose (y + 1)) : S) * ((↑(y + 1) : S) * y_1 ^ (y + 1 - 1))
have 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))
Tactic: rw [← mul_assoc, ← mul_assoc, ← Nat.cast_mul, Nat.add_one_mul_choose_eq, Nat.cast_mul,
    Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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))
⊢ (↑d.succ : S) * ((↑(d.choose y) : S) * y_1 ^ y) =
    (↑((d + 1).choose (y + 1)) : S) * ((↑(y + 1) : S) * y_1 ^ (y + 1 - 1))
have 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)
Tactic: rw [← mul_assoc, ← mul_assoc, ← Nat.cast_mul, Nat.add_one_mul_choose_eq, Nat.cast_mul,
    Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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)
⊢ (↑d.succ : S) * ((↑(d.choose y) : S) * y_1 ^ y) =
    (↑((d + 1).choose (y + 1)) : S) * ((↑(y + 1) : S) * y_1 ^ (y + 1 - 1))
have 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)
Tactic: rw [← mul_assoc, ← mul_assoc, ← Nat.cast_mul, Nat.add_one_mul_choose_eq, Nat.cast_mul,
    Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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)
⊢ (↑d.succ : S) * ((↑(d.choose y) : S) * y_1 ^ y) =
    (↑((d + 1).choose (y + 1)) : S) * ((↑(y + 1) : S) * y_1 ^ (y + 1 - 1))
have 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)
Tactic: rw [← mul_assoc, ← mul_assoc, ← Nat.cast_mul, Nat.add_one_mul_choose_eq, Nat.cast_mul,
    Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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)
⊢ (↑d.succ : S) * ((↑(d.choose y) : S) * y_1 ^ y) =
    (↑((d + 1).choose (y + 1)) : S) * ((↑(y + 1) : S) * y_1 ^ (y + 1 - 1))
have 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)
Tactic: rw [← mul_assoc, ← mul_assoc, ← Nat.cast_mul, Nat.add_one_mul_choose_eq, Nat.cast_mul,
    Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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)
⊢ (↑d.succ : S) * ((↑(d.choose y) : S) * y_1 ^ y) =
    (↑((d + 1).choose (y + 1)) : S) * ((↑(y + 1) : S) * y_1 ^ (y + 1 - 1))
have 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
Tactic: rw [← mul_assoc, ← mul_assoc, ← Nat.cast_mul, Nat.add_one_mul_choose_eq, Nat.cast_mul,
    Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
⊢ (p.comp q).coeff (p.natDegree * q.natDegree) = p.leadingCoeff * q.leadingCoeff ^ p.natDegree
have 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
Tactic: rw [comp, eval₂_def, coeff_sum]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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
have 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
Tactic: refine Eq.trans (Finset.sum_eq_single p.natDegree ?h₀ ?h₁) ?h₂
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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
⊢ (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
have 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
Tactic: refine Eq.trans (Finset.sum_eq_single p.natDegree ?h₀ ?h₁) ?h₂
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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
⊢ (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
have 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
Tactic: refine Eq.trans (Finset.sum_eq_single p.natDegree ?h₀ ?h₁) ?h₂
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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
have refine : natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff b)) + (q ^ b).natDegree < p.natDegree * q.natDegree
Tactic: refine coeff_eq_zero_of_natDegree_lt (natDegree_mul_le.trans_lt ?_)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hqd0 : q.natDegree ≠ 0
b : ℕ
hbs : b ∈ p.support
hbp : b ≠ p.natDegree
⊢ natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff b)) + (q ^ b).natDegree < p.natDegree * q.natDegree
have rw : (q ^ b).natDegree < p.natDegree * q.natDegree
Tactic: rw [natDegree_C, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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
have refine : b * q.natDegree < p.natDegree * q.natDegree
Tactic: refine natDegree_pow_le.trans_lt ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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 * q.natDegree < p.natDegree * q.natDegree
have hbc : b < p.natDegree
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
r : 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
have simp_rw : ∑ x ∈ range (p.natDegree + 1), p.coeff x * (r ^ x * if n = x then 1 else 0) = 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
r : R
n : ℕ
⊢ ∑ x ∈ range (p.natDegree + 1), p.coeff x * (r ^ x * if n = x then 1 else 0) = p.coeff n * r ^ n
have rw : ∀ b ∈ range (p.natDegree + 1), b ≠ n → p.coeff b * (r ^ b * if n = b then 1 else 0) = 0
Tactic: rw [Finset.sum_eq_single n _ fun h ↦ ?_, if_pos rfl, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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
⊢ ∑ x ∈ range (p.natDegree + 1), p.coeff x * (r ^ x * if n = x then 1 else 0) = p.coeff n * r ^ n
have rw₁ : ∀ (h : n ∉ range (p.natDegree + 1)), p.coeff n * (r ^ n * if n = n then 1 else 0) = 0
Tactic: rw [Finset.sum_eq_single n _ fun h ↦ ?_, if_pos rfl, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
r : R
n b : ℕ
h_1 : b ∈ range (p.natDegree + 1)
h : b ≠ n
⊢ p.coeff b * (r ^ b * if n = b then 1 else 0) = 0
have simp_rw : p.coeff b * (r ^ b * 0) = 0
Tactic: simp_rw [if_neg h.symm, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ p.coeff n * (r ^ n * if n = n then 1 else 0) = 0
have rw : p.natDegree < n
Tactic: rw [coeff_eq_zero_of_natDegree_lt, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
r : R
n : ℕ
h : n ∉ range (p.natDegree + 1)
⊢ p.natDegree < n
have rwa : ∀ (h : ¬n ≤ p.natDegree), p.natDegree < n
Tactic: rwa [Finset.mem_range_succ_iff, not_le] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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
⊢ p.natDegree < n
have rwa₁ : ∀ (h : p.natDegree < n), p.natDegree < n
Tactic: rwa [Finset.mem_range_succ_iff, not_le] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
r : R
hr : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) r
⊢ p.comp (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X]) X) = 0 ↔ p = 0
have 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
Tactic: simp_rw [ext_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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
have 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
Tactic: refine forall_congr' fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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 ↔
    p.coeff n = coeff 0 n
have rw : p.coeff n * r ^ 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 _)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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
⊢ (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
have rw₁ : p.coeff n * r ^ n = 0 ↔ p.coeff n = 0
Tactic: rw [comp_C_mul_X_coeff, coeff_zero, mul_right_mem_nonZeroDivisors_eq_zero_iff (pow_mem hr _)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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
⊢ (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
have rw₂ : p.coeff n = 0 ↔ p.coeff n = 0
Tactic: rw [comp_C_mul_X_coeff, coeff_zero, mul_right_mem_nonZeroDivisors_eq_zero_iff (pow_mem hr _)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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
⊢ Eq (α := S[X] →+* S[X]) (RingHom.comp (β := R[X]) (mapRingHom (↑e : R →+* S)) (mapRingHom (↑e.symm : S →+* R)))
    (RingHom.id S[X])
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Degree (goal)
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
⊢ Eq (α := R[X] →+* R[X]) (RingHom.comp (β := S[X]) (mapRingHom (↑e.symm : S →+* R)) (mapRingHom (↑e : R →+* S)))
    (RingHom.id R[X])
have a₁ : ∀ (x : R[X]) (n : ℕ),
  Eq.{u + 1} (α := R)
    (coeff
      ((RingHom.comp (β := S[X]) (mapRingHom (↑e.symm : S →+* R)) (mapRingHom (↑e : R →+* S)) : (a : R[X]) → R[X]) x) n)
    (coeff ((RingHom.id R[X] : (a : R[X]) → R[X]) x) n)
Tactic: ext