awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
q p : R[X]
hq : q ≠ 0
inl : degree.{u} (R := R) 0 ≤ (0 * q).degree
⊢ p.degree ≤ (p * q).degree
have inr : ∀ (hp : p ≠ 0), p.degree ≤ (p * q).degree
Tactic: classical
  obtain rfl | hp := eq_or_ne p 0
  · simp
  · rw [degree_mul, degree_eq_natDegree hp, degree_eq_natDegree hq]
    exact WithBot.coe_le_coe.2 (Nat.le_add_right _ _)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
hn : 0 < n
r : R
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).leadingCoeff = 1
have rw : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) (-(C : (a : R) → R[X]) r : R[X])).leadingCoeff = 1
Tactic: rw [sub_eq_add_neg, ← map_neg C r, leadingCoeff_X_pow_add_C hn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
hn : 0 < n
r : R
rw : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) (-(C : (a : R) → R[X]) r : R[X])).leadingCoeff = 1
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).leadingCoeff = 1
have rw₁ : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (-r) : R[X])).leadingCoeff = 1
Tactic: rw [sub_eq_add_neg, ← map_neg C r, leadingCoeff_X_pow_add_C hn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
n : ℕ
hn : 0 < n
r : R
rw : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) (-(C : (a : R) → R[X]) r : R[X])).leadingCoeff = 1
rw₁ : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (-r) : R[X])).leadingCoeff = 1
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).leadingCoeff = 1
have rw₂ : Eq.{u + 1} (α := R) 1 1
Tactic: rw [sub_eq_add_neg, ← map_neg C r, leadingCoeff_X_pow_add_C hn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
a : R
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree = 1
have rw : (HAdd.hAdd (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) a : R[X])).degree = 1
Tactic: rw [sub_eq_add_neg, ← map_neg C a, degree_X_add_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
a : R
rw : (HAdd.hAdd (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) a : R[X])).degree = 1
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree = 1
have rw₁ : (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-a) : R[X])).degree = 1
Tactic: rw [sub_eq_add_neg, ← map_neg C a, degree_X_add_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
a : R
rw : (HAdd.hAdd (α := R[X]) (β := R[X]) X (-(C : (a : R) → R[X]) a : R[X])).degree = 1
rw₁ : (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (-a) : R[X])).degree = 1
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree = 1
have rw₂ : Eq (α := WithBot ℕ) 1 1
Tactic: rw [sub_eq_add_neg, ← map_neg C a, degree_X_add_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
x : R
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree = 1
have rw : natDegree.{u} (R := R) X = 1
Tactic: rw [natDegree_sub_C, natDegree_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
x : R
rw : natDegree.{u} (R := R) X = 1
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).natDegree = 1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [natDegree_sub_C, natDegree_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
S : Type v
inst : Ring S
c : S
⊢ (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) c : S[X])).nextCoeff = -c
have rw : (HAdd.hAdd (α := S[X]) (β := S[X]) X (-(C : (a : S) → S[X]) c : S[X])).nextCoeff = -c
Tactic: rw [sub_eq_add_neg, ← map_neg C c, nextCoeff_X_add_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
S : Type v
inst : Ring S
c : S
rw : (HAdd.hAdd (α := S[X]) (β := S[X]) X (-(C : (a : S) → S[X]) c : S[X])).nextCoeff = -c
⊢ (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) c : S[X])).nextCoeff = -c
have rw₁ : (HAdd.hAdd (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) (-c) : S[X])).nextCoeff = -c
Tactic: rw [sub_eq_add_neg, ← map_neg C c, nextCoeff_X_add_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
S : Type v
inst : Ring S
c : S
rw : (HAdd.hAdd (α := S[X]) (β := S[X]) X (-(C : (a : S) → S[X]) c : S[X])).nextCoeff = -c
rw₁ : (HAdd.hAdd (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) (-c) : S[X])).nextCoeff = -c
⊢ (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) c : S[X])).nextCoeff = -c
have rw₂ : -c = -c
Tactic: rw [sub_eq_add_neg, ← map_neg C c, nextCoeff_X_add_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).degree = (↑n : WithBot ℕ)
have rw : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) (-(C : (a : R) → R[X]) a : R[X])).degree = (↑n : WithBot ℕ)
Tactic: rw [sub_eq_add_neg, ← map_neg C a, degree_X_pow_add_C hn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
n : ℕ
hn : 0 < n
a : R
rw : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) (-(C : (a : R) → R[X]) a : R[X])).degree = (↑n : WithBot ℕ)
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).degree = (↑n : WithBot ℕ)
have rw₁ : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (-a) : R[X])).degree = (↑n : WithBot ℕ)
Tactic: rw [sub_eq_add_neg, ← map_neg C a, degree_X_pow_add_C hn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
n : ℕ
hn : 0 < n
a : R
rw : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) (-(C : (a : R) → R[X]) a : R[X])).degree = (↑n : WithBot ℕ)
rw₁ : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (-a) : R[X])).degree = (↑n : WithBot ℕ)
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).degree = (↑n : WithBot ℕ)
have rw₂ : Eq (α := WithBot ℕ) (↑n : WithBot ℕ) (↑n : WithBot ℕ)
Tactic: rw [sub_eq_add_neg, ← map_neg C a, degree_X_pow_add_C hn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
n : ℕ
hn : 0 < n
a : R
⊢ HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X]) ≠ 0
have rw : HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (-a) : R[X]) ≠ 0
Tactic: rw [sub_eq_add_neg, ← map_neg C a]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
n : ℕ
r : R
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).natDegree = n
have rw : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) (-(C : (a : R) → R[X]) r : R[X])).natDegree = n
Tactic: rw [sub_eq_add_neg, ← map_neg C r, natDegree_X_pow_add_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
n : ℕ
r : R
rw : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) (-(C : (a : R) → R[X]) r : R[X])).natDegree = n
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).natDegree = n
have rw₁ : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (-r) : R[X])).natDegree = n
Tactic: rw [sub_eq_add_neg, ← map_neg C r, natDegree_X_pow_add_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
inst_1 : Nontrivial R
n : ℕ
r : R
rw : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) (-(C : (a : R) → R[X]) r : R[X])).natDegree = n
rw₁ : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) (-r) : R[X])).natDegree = n
⊢ (HSub.hSub (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).natDegree = n
have rw₂ : n = n
Tactic: rw [sub_eq_add_neg, ← map_neg C r, natDegree_X_pow_add_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
S : Type v
inst : Ring S
r : S
⊢ (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) r : S[X])).leadingCoeff = 1
have rw : (HAdd.hAdd (α := S[X]) (β := S[X]) X (-(C : (a : S) → S[X]) r : S[X])).leadingCoeff = 1
Tactic: rw [sub_eq_add_neg, ← map_neg C r, leadingCoeff_X_add_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
S : Type v
inst : Ring S
r : S
rw : (HAdd.hAdd (α := S[X]) (β := S[X]) X (-(C : (a : S) → S[X]) r : S[X])).leadingCoeff = 1
⊢ (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) r : S[X])).leadingCoeff = 1
have rw₁ : (HAdd.hAdd (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) (-r) : S[X])).leadingCoeff = 1
Tactic: rw [sub_eq_add_neg, ← map_neg C r, leadingCoeff_X_add_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
S : Type v
inst : Ring S
r : S
rw : (HAdd.hAdd (α := S[X]) (β := S[X]) X (-(C : (a : S) → S[X]) r : S[X])).leadingCoeff = 1
rw₁ : (HAdd.hAdd (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) (-r) : S[X])).leadingCoeff = 1
⊢ (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) r : S[X])).leadingCoeff = 1
have rw₂ : Eq.{v + 1} (α := S) 1 1
Tactic: rw [sub_eq_add_neg, ← map_neg C r, leadingCoeff_X_add_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.degree ≤ 1
n_1 n m : ℕ
⊢ p.coeff m.succ.succ =
    (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
          ((C : (a : R) → R[X]) (p.coeff 0) : R[X])).coeff
      m.succ.succ
have this : p.degree < (↑m.succ.succ : WithBot ℕ)
Tactic: have : degree p < m.succ.succ := lt_of_le_of_lt h Nat.one_lt_ofNat
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.degree = 1
⊢ HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) =
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
have h₁ : p.degree = (↑1 : WithBot ℕ)
Tactic: rw [← Nat.cast_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.degree = (↑1 : WithBot ℕ)
⊢ HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) =
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
have rw : HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
    ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) =
  HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) X)
    ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
Tactic: rw [leadingCoeff, natDegree_eq_of_degree_eq_some h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.degree = (↑1 : WithBot ℕ)
rw :
  HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) =
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
⊢ HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) =
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
have rw₁ : HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
    ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) =
  HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
    ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
Tactic: rw [leadingCoeff, natDegree_eq_of_degree_eq_some h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 1
⊢ p = HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
have rw : p = HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) 1 X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
Tactic: rw [← one_mul X, ← C_1, ← hm.coeff_natDegree, hnd, ← eq_X_add_C_of_natDegree_le_one hnd.le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 1
rw : p = HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) 1 X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
⊢ p = HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
have rw₁ : p = HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 1) X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
Tactic: rw [← one_mul X, ← C_1, ← hm.coeff_natDegree, hnd, ← eq_X_add_C_of_natDegree_le_one hnd.le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 1
rw : p = HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) 1 X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
rw₁ :
  p = HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 1) X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
⊢ p = HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
have rw₂ : p =
  HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) X)
    ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
Tactic: rw [← one_mul X, ← C_1, ← hm.coeff_natDegree, hnd, ← eq_X_add_C_of_natDegree_le_one hnd.le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 1
rw : p = HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) 1 X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
rw₁ :
  p = HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 1) X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
rw₂ :
  p =
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
⊢ p = HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
have rw₃ : p =
  HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
    ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
Tactic: rw [← one_mul X, ← C_1, ← hm.coeff_natDegree, hnd, ← eq_X_add_C_of_natDegree_le_one hnd.le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 1
rw : p = HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) 1 X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
rw₁ :
  p = HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) 1) X) ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
rw₂ :
  p =
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff p.natDegree) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
rw₃ :
  p =
    HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) (p.coeff 1) : R[X]) X)
      ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
⊢ p = HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (p.coeff 0) : R[X])
have rw₄ : p = p
Tactic: rw [← one_mul X, ← C_1, ← hm.coeff_natDegree, hnd, ← eq_X_add_C_of_natDegree_le_one hnd.le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ 0 ≤ p.degree ↔ p ≠ 0
have rw : ¬p.degree < 0 ↔ p ≠ 0
Tactic: rw [← not_lt, Nat.WithBot.lt_zero_iff, degree_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : ¬p.degree < 0 ↔ p ≠ 0
⊢ 0 ≤ p.degree ↔ p ≠ 0
have rw₁ : ¬p.degree = ⊥ ↔ p ≠ 0
Tactic: rw [← not_lt, Nat.WithBot.lt_zero_iff, degree_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : ¬p.degree < 0 ↔ p ≠ 0
rw₁ : ¬p.degree = ⊥ ↔ p ≠ 0
⊢ 0 ≤ p.degree ↔ p ≠ 0
have rw₂ : ¬p = 0 ↔ p ≠ 0
Tactic: rw [← not_lt, Nat.WithBot.lt_zero_iff, degree_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
hdeg : (↑n : WithBot ℕ) ≤ p.degree
⊢ (↑n : WithBot ℕ) ≤ (↑p.natDegree : WithBot ℕ)
have rwa : ∀ (hdeg : LE.le (α := WithBot ℕ) (↑n : WithBot ℕ) (↑p.natDegree : WithBot ℕ)),
  (↑n : WithBot ℕ) ≤ (↑p.natDegree : WithBot ℕ)
Tactic: rwa [degree_eq_natDegree <| ne_zero_of_coe_le_degree hdeg] at hdeg
Cleared hypotheses: hdeg
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
a b : R
inst : Semiring R
ha : a ≠ 0
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).degree =
    1
have rw : (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).degree = 1
Tactic: rw [degree_add_eq_left_of_degree_lt <| degree_C_lt_degree_C_mul_X ha, degree_C_mul_X ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
a b : R
inst : Semiring R
ha : a ≠ 0
rw : (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).degree = 1
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).degree =
    1
have rw₁ : Eq (α := WithBot ℕ) 1 1
Tactic: rw [degree_add_eq_left_of_degree_lt <| degree_C_lt_degree_C_mul_X ha, degree_C_mul_X ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
a b : R
inst : Semiring R
ha : a ≠ 0
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree =
    1
have rw : (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).natDegree = 1
Tactic: rw [natDegree_add_C, natDegree_C_mul_X a ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
a b : R
inst : Semiring R
ha : a ≠ 0
rw : (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).natDegree = 1
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).natDegree =
    1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [natDegree_add_C, natDegree_C_mul_X a ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
a b : R
inst : Semiring R
ha : a ≠ 0
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).leadingCoeff =
    a
have rw : (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) b : R[X])
      (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)).leadingCoeff =
  a
Tactic: rw [add_comm, leadingCoeff_add_of_degree_lt (degree_C_lt_degree_C_mul_X ha),
    leadingCoeff_C_mul_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
a b : R
inst : Semiring R
ha : a ≠ 0
rw :
  (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) b : R[X])
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)).leadingCoeff =
    a
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).leadingCoeff =
    a
have rw₁ : (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).leadingCoeff = a
Tactic: rw [add_comm, leadingCoeff_add_of_degree_lt (degree_C_lt_degree_C_mul_X ha),
    leadingCoeff_C_mul_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
a b : R
inst : Semiring R
ha : a ≠ 0
rw :
  (HAdd.hAdd (α := R[X]) ((C : (a : R) → R[X]) b : R[X])
        (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)).leadingCoeff =
    a
rw₁ : (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X).leadingCoeff = a
⊢ (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) X)
        ((C : (a : R) → R[X]) b : R[X])).leadingCoeff =
    a
have rw₂ : a = a
Tactic: rw [add_comm, leadingCoeff_add_of_degree_lt (degree_C_lt_degree_C_mul_X ha),
    leadingCoeff_C_mul_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
a b c : R
inst : Semiring R
ha : a ≠ 0
⊢ (HAdd.hAdd (β := R[X])
        (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]) b : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).degree =
    2
have rw : Eq (α := WithBot ℕ) (↑2 : WithBot ℕ) 2
Tactic: rw [add_assoc, degree_add_eq_left_of_degree_lt <| degree_linear_lt_degree_C_mul_X_sq ha,
    degree_C_mul_X_pow 2 ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
a b c : R
inst : Semiring R
ha : a ≠ 0
⊢ (HAdd.hAdd (β := R[X])
        (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]) b : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).leadingCoeff =
    a
have rw : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
      HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).leadingCoeff =
  a
Tactic: rw [add_assoc, add_comm, leadingCoeff_add_of_degree_lt <| degree_linear_lt_degree_C_mul_X_sq ha,
    leadingCoeff_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.SmallDegree (goal)
Goal:
R : Type u
a b c : R
inst : Semiring R
ha : a ≠ 0
rw :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2) +
        HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
          ((C : (a : R) → R[X]) c : R[X])).leadingCoeff =
    a
⊢ (HAdd.hAdd (β := R[X])
        (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]) b : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X])).leadingCoeff =
    a
have rw₁ : (HAdd.hAdd (β := R[X]) (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
        ((C : (a : R) → R[X]) c : R[X]) +
      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) (β := ℕ) X 2)).leadingCoeff =
  a
Tactic: rw [add_assoc, add_comm, leadingCoeff_add_of_degree_lt <| degree_linear_lt_degree_C_mul_X_sq ha,
    leadingCoeff_C_mul_X_pow]