awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
rw : (HAdd.hAdd (β := R[X]) p (-(C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
rw₁ : (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) (-a) : R[X])).natDegree = p.natDegree
⊢ (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
have rw₂ : p.natDegree = p.natDegree
Tactic: rw [sub_eq_add_neg, ← C_neg, natDegree_add_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : q.degree < p.degree
⊢ (p - q).leadingCoeff = p.leadingCoeff
have h₁ : (-q).degree < p.degree
Tactic: rw [← q.degree_neg] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : (-q).degree < p.degree
⊢ (p - q).leadingCoeff = p.leadingCoeff
have rw : (p + -q).leadingCoeff = p.leadingCoeff
Tactic: rw [sub_eq_add_neg, leadingCoeff_add_of_degree_lt' h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : (-q).degree < p.degree
rw : (p + -q).leadingCoeff = p.leadingCoeff
⊢ (p - q).leadingCoeff = p.leadingCoeff
have rw₁ : p.leadingCoeff = p.leadingCoeff
Tactic: rw [sub_eq_add_neg, leadingCoeff_add_of_degree_lt' h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : p.degree < q.degree
⊢ (p - q).leadingCoeff = -q.leadingCoeff
have h₁ : p.degree < (-q).degree
Tactic: rw [← q.degree_neg] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : p.degree < (-q).degree
⊢ (p - q).leadingCoeff = -q.leadingCoeff
have rw : (p + -q).leadingCoeff = -q.leadingCoeff
Tactic: rw [sub_eq_add_neg, leadingCoeff_add_of_degree_lt h, leadingCoeff_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : p.degree < (-q).degree
rw : (p + -q).leadingCoeff = -q.leadingCoeff
⊢ (p - q).leadingCoeff = -q.leadingCoeff
have rw₁ : (-q).leadingCoeff = -q.leadingCoeff
Tactic: rw [sub_eq_add_neg, leadingCoeff_add_of_degree_lt h, leadingCoeff_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : p.degree < (-q).degree
rw : (p + -q).leadingCoeff = -q.leadingCoeff
rw₁ : (-q).leadingCoeff = -q.leadingCoeff
⊢ (p - q).leadingCoeff = -q.leadingCoeff
have rw₂ : -q.leadingCoeff = -q.leadingCoeff
Tactic: rw [sub_eq_add_neg, leadingCoeff_add_of_degree_lt h, leadingCoeff_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff ≠ q.leadingCoeff
⊢ (p - q).leadingCoeff = p.leadingCoeff - q.leadingCoeff
have h₁ : p.degree = (-q).degree
Tactic: replace h : degree p = degree (-q) := by rwa [q.degree_neg]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hlc : p.leadingCoeff ≠ q.leadingCoeff
h : p.degree = (-q).degree
⊢ p.leadingCoeff + (-q).leadingCoeff ≠ 0
have rwa : ∀ (hlc : p.leadingCoeff - q.leadingCoeff ≠ 0) (h : p.degree = (-q).degree), p.leadingCoeff + (-q).leadingCoeff ≠ 0
Tactic: rwa [← sub_ne_zero, sub_eq_add_neg, ← q.leadingCoeff_neg] at hlc
Cleared hypotheses: hlc, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hlc : p.leadingCoeff ≠ q.leadingCoeff
h : p.degree = (-q).degree
rwa : ∀ (hlc : p.leadingCoeff - q.leadingCoeff ≠ 0) (h : p.degree = (-q).degree), p.leadingCoeff + (-q).leadingCoeff ≠ 0
⊢ p.leadingCoeff + (-q).leadingCoeff ≠ 0
have rwa₁ : ∀ (hlc : p.leadingCoeff + -q.leadingCoeff ≠ 0) (h : p.degree = (-q).degree), p.leadingCoeff + (-q).leadingCoeff ≠ 0
Tactic: rwa [← sub_ne_zero, sub_eq_add_neg, ← q.leadingCoeff_neg] at hlc
Cleared hypotheses: hlc, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hlc : p.leadingCoeff ≠ q.leadingCoeff
h : p.degree = (-q).degree
rwa : ∀ (hlc : p.leadingCoeff - q.leadingCoeff ≠ 0) (h : p.degree = (-q).degree), p.leadingCoeff + (-q).leadingCoeff ≠ 0
rwa₁ :
  ∀ (hlc : p.leadingCoeff + -q.leadingCoeff ≠ 0) (h : p.degree = (-q).degree), p.leadingCoeff + (-q).leadingCoeff ≠ 0
⊢ p.leadingCoeff + (-q).leadingCoeff ≠ 0
have rwa₂ : ∀ (hlc : p.leadingCoeff + (-q).leadingCoeff ≠ 0) (h : p.degree = (-q).degree), p.leadingCoeff + (-q).leadingCoeff ≠ 0
Tactic: rwa [← sub_ne_zero, sub_eq_add_neg, ← q.leadingCoeff_neg] at hlc
Cleared hypotheses: hlc, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hlc : p.leadingCoeff ≠ q.leadingCoeff
h : p.degree = (-q).degree
⊢ (p - q).leadingCoeff = p.leadingCoeff - q.leadingCoeff
have hlc₁ : p.leadingCoeff + (-q).leadingCoeff ≠ 0
Tactic: replace hlc : leadingCoeff p + leadingCoeff (-q) ≠ 0 := by
    rwa [← sub_ne_zero, sub_eq_add_neg, ← q.leadingCoeff_neg] at hlc
Cleared hypotheses: hlc
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : p.degree = (-q).degree
hlc : p.leadingCoeff + (-q).leadingCoeff ≠ 0
⊢ (p - q).leadingCoeff = p.leadingCoeff - q.leadingCoeff
have rw : (p + -q).leadingCoeff = p.leadingCoeff - q.leadingCoeff
Tactic: rw [sub_eq_add_neg, leadingCoeff_add_of_degree_eq h hlc, leadingCoeff_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : p.degree = (-q).degree
hlc : p.leadingCoeff + (-q).leadingCoeff ≠ 0
rw : (p + -q).leadingCoeff = p.leadingCoeff - q.leadingCoeff
⊢ (p - q).leadingCoeff = p.leadingCoeff - q.leadingCoeff
have rw₁ : p.leadingCoeff + (-q).leadingCoeff = p.leadingCoeff - q.leadingCoeff
Tactic: rw [sub_eq_add_neg, leadingCoeff_add_of_degree_eq h hlc, leadingCoeff_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : p.degree = (-q).degree
hlc : p.leadingCoeff + (-q).leadingCoeff ≠ 0
rw : (p + -q).leadingCoeff = p.leadingCoeff - q.leadingCoeff
rw₁ : p.leadingCoeff + (-q).leadingCoeff = p.leadingCoeff - q.leadingCoeff
⊢ (p - q).leadingCoeff = p.leadingCoeff - q.leadingCoeff
have rw₂ : p.leadingCoeff + -q.leadingCoeff = p.leadingCoeff - q.leadingCoeff
Tactic: rw [sub_eq_add_neg, leadingCoeff_add_of_degree_eq h hlc, leadingCoeff_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : p.degree = (-q).degree
hlc : p.leadingCoeff + (-q).leadingCoeff ≠ 0
rw : (p + -q).leadingCoeff = p.leadingCoeff - q.leadingCoeff
rw₁ : p.leadingCoeff + (-q).leadingCoeff = p.leadingCoeff - q.leadingCoeff
rw₂ : p.leadingCoeff + -q.leadingCoeff = p.leadingCoeff - q.leadingCoeff
⊢ (p - q).leadingCoeff = p.leadingCoeff - q.leadingCoeff
have rw₃ : p.leadingCoeff + -q.leadingCoeff = p.leadingCoeff + -q.leadingCoeff
Tactic: rw [sub_eq_add_neg, leadingCoeff_add_of_degree_eq h hlc, leadingCoeff_neg, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : q.degree < p.degree
⊢ (p - q).degree = p.degree
have h₁ : (-q).degree < p.degree
Tactic: rw [← degree_neg q] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : (-q).degree < p.degree
⊢ (p - q).degree = p.degree
have rw : (p + -q).degree = p.degree
Tactic: rw [sub_eq_add_neg, degree_add_eq_left_of_degree_lt h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : (-q).degree < p.degree
rw : (p + -q).degree = p.degree
⊢ (p - q).degree = p.degree
have rw₁ : p.degree = p.degree
Tactic: rw [sub_eq_add_neg, degree_add_eq_left_of_degree_lt h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : p.degree < q.degree
⊢ (p - q).degree = q.degree
have h₁ : p.degree < (-q).degree
Tactic: rw [← degree_neg q] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : p.degree < (-q).degree
⊢ (p - q).degree = q.degree
have rw : (p + -q).degree = q.degree
Tactic: rw [sub_eq_add_neg, degree_add_eq_right_of_degree_lt h, degree_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : p.degree < (-q).degree
rw : (p + -q).degree = q.degree
⊢ (p - q).degree = q.degree
have rw₁ : (-q).degree = q.degree
Tactic: rw [sub_eq_add_neg, degree_add_eq_right_of_degree_lt h, degree_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
h : p.degree < (-q).degree
rw : (p + -q).degree = q.degree
rw₁ : (-q).degree = q.degree
⊢ (p - q).degree = q.degree
have rw₂ : q.degree = q.degree
Tactic: rw [sub_eq_add_neg, degree_add_eq_right_of_degree_lt h, degree_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
a : R
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree = 1
have this : degree.{u} (R := R) ((C : (a : R) → R[X]) a) < degree.{u} (R := R) X
Tactic: have : degree (C a) < degree (X : R[X]) :=
    calc
      degree (C a) ≤ 0 := degree_C_le
      _ < 1 := WithBot.coe_lt_coe.mpr zero_lt_one
      _ = degree X := degree_X.symm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
a : R
this : degree.{u} (R := R) ((C : (a : R) → R[X]) a) < degree.{u} (R := R) X
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree = 1
have rw : degree.{u} (R := R) X = 1
Tactic: rw [degree_add_eq_left_of_degree_lt this, degree_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
a : R
this : degree.{u} (R := R) ((C : (a : R) → R[X]) a) < degree.{u} (R := R) X
rw : degree.{u} (R := R) X = 1
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).degree = 1
have rw₁ : Eq (α := WithBot ℕ) 1 1
Tactic: rw [degree_add_eq_left_of_degree_lt this, degree_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
S : Type v
inst : Semiring S
c : S
⊢ (HAdd.hAdd (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) c : S[X])).nextCoeff = c
have a : Nontrivial S
Tactic: nontriviality S
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ 0 < (HPow.hPow (α := R[X]) X n).degree
have rwa : LT.lt (α := WithBot ℕ) 0 (↑n : WithBot ℕ)
Tactic: rwa [degree_X_pow, Nat.cast_pos]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).degree = (↑n : WithBot ℕ)
have this : degree.{u} (R := R) ((C : (a : R) → R[X]) a) < (HPow.hPow (α := R[X]) X n).degree
Tactic: have : degree (C a) < degree ((X : R[X]) ^ n) := degree_C_le.trans_lt <| by
    rwa [degree_X_pow, Nat.cast_pos]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
n : ℕ
hn : 0 < n
a : R
this : degree.{u} (R := R) ((C : (a : R) → R[X]) a) < (HPow.hPow (α := R[X]) X n).degree
⊢ (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).degree = (↑n : WithBot ℕ)
have rw : (HPow.hPow (α := R[X]) X n).degree = (↑n : WithBot ℕ)
Tactic: rw [degree_add_eq_left_of_degree_lt this, degree_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
n : ℕ
hn : 0 < n
a : R
this : degree.{u} (R := R) ((C : (a : R) → R[X]) a) < (HPow.hPow (α := R[X]) X n).degree
rw : (HPow.hPow (α := R[X]) X n).degree = (↑n : WithBot ℕ)
⊢ (HAdd.hAdd (β := 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 [degree_add_eq_left_of_degree_lt this, degree_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Nontrivial R
inst_1 : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) a : R[X])).degree ≠ ⊥
have rw : Ne (α := WithBot ℕ) (↑n : WithBot ℕ) ⊥
Tactic: rw [degree_X_pow_add_C hn a]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : 0 < n
r : R
⊢ (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).leadingCoeff = 1
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : 0 < n
r : R
h : Nontrivial R
⊢ (HAdd.hAdd (β := 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])).coeff
    (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).natDegree =
  1
Tactic: rw [leadingCoeff, natDegree_X_pow_add_C, coeff_add, coeff_X_pow_self, coeff_C,
    if_neg (pos_iff_ne_zero.mp hn), add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : 0 < n
r : R
h : Nontrivial R
rw :
  (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff
      (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).natDegree =
    1
⊢ (HAdd.hAdd (β := 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])).coeff n = 1
Tactic: rw [leadingCoeff, natDegree_X_pow_add_C, coeff_add, coeff_X_pow_self, coeff_C,
    if_neg (pos_iff_ne_zero.mp hn), add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : 0 < n
r : R
h : Nontrivial R
rw :
  (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff
      (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).natDegree =
    1
rw₁ : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff n = 1
⊢ (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).leadingCoeff = 1
have rw₂ : (HPow.hPow (α := R[X]) X n).coeff n + coeff ((C : (a : R) → R[X]) r) n = 1
Tactic: rw [leadingCoeff, natDegree_X_pow_add_C, coeff_add, coeff_X_pow_self, coeff_C,
    if_neg (pos_iff_ne_zero.mp hn), add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : 0 < n
r : R
h : Nontrivial R
rw :
  (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff
      (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).natDegree =
    1
rw₁ : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff n = 1
rw₂ : (HPow.hPow (α := R[X]) X n).coeff n + coeff ((C : (a : R) → R[X]) r) n = 1
⊢ (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).leadingCoeff = 1
have rw₃ : HAdd.hAdd (α := R) 1 (coeff ((C : (a : R) → R[X]) r) n) = 1
Tactic: rw [leadingCoeff, natDegree_X_pow_add_C, coeff_add, coeff_X_pow_self, coeff_C,
    if_neg (pos_iff_ne_zero.mp hn), add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : 0 < n
r : R
h : Nontrivial R
rw :
  (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff
      (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).natDegree =
    1
rw₁ : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff n = 1
rw₂ : (HPow.hPow (α := R[X]) X n).coeff n + coeff ((C : (a : R) → R[X]) r) n = 1
rw₃ : HAdd.hAdd (α := R) 1 (coeff ((C : (a : R) → R[X]) r) n) = 1
⊢ (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).leadingCoeff = 1
have rw₄ : (1 + if n = 0 then r else 0) = 1
Tactic: rw [leadingCoeff, natDegree_X_pow_add_C, coeff_add, coeff_X_pow_self, coeff_C,
    if_neg (pos_iff_ne_zero.mp hn), add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : 0 < n
r : R
h : Nontrivial R
rw :
  (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff
      (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).natDegree =
    1
rw₁ : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff n = 1
rw₂ : (HPow.hPow (α := R[X]) X n).coeff n + coeff ((C : (a : R) → R[X]) r) n = 1
rw₃ : HAdd.hAdd (α := R) 1 (coeff ((C : (a : R) → R[X]) r) n) = 1
rw₄ : (1 + if n = 0 then r else 0) = 1
⊢ (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).leadingCoeff = 1
have rw₅ : HAdd.hAdd (α := R) 1 0 = 1
Tactic: rw [leadingCoeff, natDegree_X_pow_add_C, coeff_add, coeff_X_pow_self, coeff_C,
    if_neg (pos_iff_ne_zero.mp hn), add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
hn : 0 < n
r : R
h : Nontrivial R
rw :
  (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff
      (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).natDegree =
    1
rw₁ : (HAdd.hAdd (β := R[X]) (HPow.hPow (α := R[X]) X n) ((C : (a : R) → R[X]) r : R[X])).coeff n = 1
rw₂ : (HPow.hPow (α := R[X]) X n).coeff n + coeff ((C : (a : R) → R[X]) r) n = 1
rw₃ : HAdd.hAdd (α := R) 1 (coeff ((C : (a : R) → R[X]) r) n) = 1
rw₄ : (1 + if n = 0 then r else 0) = 1
rw₅ : HAdd.hAdd (α := R) 1 0 = 1
⊢ (HAdd.hAdd (β := 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 [leadingCoeff, natDegree_X_pow_add_C, coeff_add, coeff_X_pow_self, coeff_C,
    if_neg (pos_iff_ne_zero.mp hn), add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
S : Type v
inst : Semiring S
r : S
⊢ (HAdd.hAdd (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) r : S[X])).leadingCoeff = 1
have rw : (HAdd.hAdd (β := S[X]) (HPow.hPow (α := S[X]) (β := ℕ) X 1) ((C : (a : S) → S[X]) r : S[X])).leadingCoeff = 1
Tactic: rw [← pow_one (X : S[X]), leadingCoeff_X_pow_add_C zero_lt_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
S : Type v
inst : Semiring S
r : S
rw : (HAdd.hAdd (β := S[X]) (HPow.hPow (α := S[X]) (β := ℕ) X 1) ((C : (a : S) → S[X]) r : S[X])).leadingCoeff = 1
⊢ (HAdd.hAdd (α := 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 [← pow_one (X : S[X]), leadingCoeff_X_pow_add_C zero_lt_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
r : R
i : ℕ
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ i).leadingCoeff = 1
have a : Nontrivial R
Tactic: nontriviality
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
r : R
i : ℕ
h : Nontrivial R
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ i).leadingCoeff = 1
have rw : (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).leadingCoeff ^ i = 1
Tactic: rw [leadingCoeff_pow']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
r : R
i : ℕ
h : Nontrivial R
rw : (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).leadingCoeff ^ i = 1
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X]) ^ i).leadingCoeff = 1
have rw₁ : (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) r : R[X])).leadingCoeff ^ i ≠ 0
Tactic: rw [leadingCoeff_pow']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
have pos : ∀ (hp : p = 0), (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
pos : ∀ (hp : p = 0), (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
have neg : ∀ (hp : ¬p = 0), (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
have pos : ∀ (hq : q = 0), (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
pos : ∀ (hq : q = 0), (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
have neg : ∀ (hq : ¬q = 0), (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
Tactic: by_cases hq : q = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p q : R[X]
hp : ¬p = 0
hq : ¬q = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
have neg : p.leadingCoeff * q.leadingCoeff ≠ 0
Tactic: rw [leadingCoeff_mul']
-- 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
⊢ p.degree ≤ (p * q).degree
have inl : degree.{u} (R := R) 0 ≤ (0 * q).degree
Tactic: obtain rfl | hp := eq_or_ne p 0
Cleared hypotheses: p
-- 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: obtain rfl | hp := eq_or_ne p 0
-- 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
hp : p ≠ 0
⊢ p.degree ≤ (p * q).degree
have inr : (↑p.natDegree : WithBot ℕ) ≤ HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
Tactic: rw [degree_mul, degree_eq_natDegree hp, degree_eq_natDegree hq]
-- 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
⊢ p.degree ≤ (p * q).degree
have inl : degree.{u} (R := R) 0 ≤ (0 * 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 _ _)
Cleared hypotheses: p