awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ (-p).support.max = p.support.max
have rw : p.support.max = p.support.max
Tactic: rw [support_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Ring R
n : ℤ
⊢ natDegree.{u} (R := R) (↑n : R[X]) = 0
have rw : natDegree.{u} (R := R) ((C : (a : R) → R[X]) (↑n : R)) = 0
Tactic: rw [← C_eq_intCast, natDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Ring R
n : ℤ
rw : natDegree.{u} (R := R) ((C : (a : R) → R[X]) (↑n : R)) = 0
⊢ natDegree.{u} (R := R) (↑n : R[X]) = 0
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [← C_eq_intCast, natDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ (-p).leadingCoeff = -p.leadingCoeff
have rw : (-p).coeff (-p).natDegree = -p.leadingCoeff
Tactic: rw [leadingCoeff, leadingCoeff, natDegree_neg, coeff_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
rw : (-p).coeff (-p).natDegree = -p.leadingCoeff
⊢ (-p).leadingCoeff = -p.leadingCoeff
have rw₁ : (-p).coeff (-p).natDegree = -p.coeff p.natDegree
Tactic: rw [leadingCoeff, leadingCoeff, natDegree_neg, coeff_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
rw : (-p).coeff (-p).natDegree = -p.leadingCoeff
rw₁ : (-p).coeff (-p).natDegree = -p.coeff p.natDegree
⊢ (-p).leadingCoeff = -p.leadingCoeff
have rw₂ : (-p).coeff p.natDegree = -p.coeff p.natDegree
Tactic: rw [leadingCoeff, leadingCoeff, natDegree_neg, coeff_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
rw : (-p).coeff (-p).natDegree = -p.leadingCoeff
rw₁ : (-p).coeff (-p).natDegree = -p.coeff p.natDegree
rw₂ : (-p).coeff p.natDegree = -p.coeff p.natDegree
⊢ (-p).leadingCoeff = -p.leadingCoeff
have rw₃ : -p.coeff p.natDegree = -p.coeff p.natDegree
Tactic: rw [leadingCoeff, leadingCoeff, natDegree_neg, coeff_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.nextCoeff = 0 ↔ p.natDegree = 0 ∨ 0 < p.natDegree ∧ p.coeff (p.natDegree - 1) = 0
have simp : ¬p.natDegree = 0 → p.coeff (p.natDegree - 1) = 0 ↔ ¬p.natDegree = 0 → ¬p.natDegree = 0 ∧ p.coeff (p.natDegree - 1) = 0
Tactic: simp [nextCoeff, or_iff_not_imp_left, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : 0 < p.natDegree
⊢ p.nextCoeff = p.coeff (p.natDegree - 1)
have hnc : ¬p.natDegree = 0
Tactic: rw [nextCoeff, if_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : 0 < p.natDegree
⊢ ¬p.natDegree = 0
have hnc : ∀ (hp : p.natDegree = 0), p.natDegree ≤ 0
Tactic: contrapose! hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ (p + q).natDegree ≤ max p.natDegree q.natDegree
have inl : ∀ (h : (p + q).degree ≤ p.degree), (p + q).natDegree ≤ max p.natDegree q.natDegree
Tactic: rcases le_max_iff.1 (degree_add_le p q) with h | h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
inl : ∀ (h : (p + q).degree ≤ p.degree), (p + q).natDegree ≤ max p.natDegree q.natDegree
⊢ (p + q).natDegree ≤ max p.natDegree q.natDegree
have inr : ∀ (h : (p + q).degree ≤ q.degree), (p + q).natDegree ≤ max p.natDegree q.natDegree
Tactic: rcases le_max_iff.1 (degree_add_le p q) with h | h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.leadingCoeff ≠ 0 ↔ p ≠ 0
have rw : ¬p.leadingCoeff = 0 ↔ p ≠ 0
Tactic: rw [Ne, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : ¬p.leadingCoeff = 0 ↔ p ≠ 0
⊢ p.leadingCoeff ≠ 0 ↔ p ≠ 0
have rw₁ : ¬p = 0 ↔ p ≠ 0
Tactic: rw [Ne, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.leadingCoeff = 0 ↔ p.degree = ⊥
have rw : p = 0 ↔ p.degree = ⊥
Tactic: rw [leadingCoeff_eq_zero, degree_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : p = 0 ↔ p.degree = ⊥
⊢ p.leadingCoeff = 0 ↔ p.degree = ⊥
have rw₁ : p = 0 ↔ p = 0
Tactic: rw [leadingCoeff_eq_zero, degree_eq_bot]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ (erase n p).degree ≤ p.degree
have simp : (Finsupp.erase n p.toFinsupp).support.max ≤ p.toFinsupp.support.max
Tactic: simp only [erase_def, AddMonoidAlgebra.erase, AddMonoidAlgebra.coeff, AddMonoidAlgebra.ofCoeff,
    degree, support]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ (Finsupp.erase n p.toFinsupp).support.max ≤ p.toFinsupp.support.max
have h : (Finsupp.erase n p.toFinsupp).support ⊆ p.toFinsupp.support
Tactic: apply sup_mono
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
⊢ (erase p.natDegree p).degree < p.degree
have apply : (erase p.natDegree p).degree ≠ p.degree
Tactic: apply lt_of_le_of_ne (degree_erase_le _ _)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
⊢ (erase p.natDegree p).degree ≠ p.degree
have rw : (p.support.erase p.natDegree).max ≠ (↑p.natDegree : WithBot ℕ)
Tactic: rw [degree_eq_natDegree hp, degree, support_erase]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (p.update n a).degree ≤ max p.degree (↑n : WithBot ℕ)
have rw : (if a = 0 then p.support.erase n else insert n p.support).max ≤ max p.degree (↑n : WithBot ℕ)
Tactic: rw [degree, support_update]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (if a = 0 then p.support.erase n else insert n p.support).max ≤ max p.degree (↑n : WithBot ℕ)
have pos : a = 0 → (p.support.erase n).max ≤ max p.degree (↑n : WithBot ℕ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
pos : a = 0 → (p.support.erase n).max ≤ max p.degree (↑n : WithBot ℕ)
⊢ (if a = 0 then p.support.erase n else insert n p.support).max ≤ max p.degree (↑n : WithBot ℕ)
have neg : ¬a = 0 → (insert n p.support).max ≤ max p.degree (↑n : WithBot ℕ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
h : ¬a = 0
⊢ (insert n p.support).max ≤ max p.degree (↑n : WithBot ℕ)
have neg : max p.support.max (↑n : WithBot ℕ) ≤ max p.degree (↑n : WithBot ℕ)
Tactic: rw [max_insert, max_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
⊢ (p.update n a).degree ≤ max p.degree (↑n : WithBot ℕ)
have rw : (p.update n a).support.max ≤ max p.degree (↑n : WithBot ℕ)
Tactic: classical
  rw [degree, support_update]
  split_ifs
  · exact (Finset.max_mono (erase_subset _ _)).trans (le_max_left _ _)
  · rw [max_insert, max_comm]
    exact le_rfl
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
rw : (p.update n a).support.max ≤ max p.degree (↑n : WithBot ℕ)
⊢ (p.update n a).degree ≤ max p.degree (↑n : WithBot ℕ)
have rw₁ : (if a = 0 then p.support.erase n else insert n p.support).max ≤ max p.degree (↑n : WithBot ℕ)
Tactic: classical
  rw [degree, support_update]
  split_ifs
  · exact (Finset.max_mono (erase_subset _ _)).trans (le_max_left _ _)
  · rw [max_insert, max_comm]
    exact le_rfl
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
rw : (p.update n a).support.max ≤ max p.degree (↑n : WithBot ℕ)
rw₁ rw₂ rw₃ : (if a = 0 then p.support.erase n else insert n p.support).max ≤ max p.degree (↑n : WithBot ℕ)
⊢ (p.update n a).degree ≤ max p.degree (↑n : WithBot ℕ)
have pos : a = 0 → (p.support.erase n).max ≤ max p.degree (↑n : WithBot ℕ)
Tactic: classical
  rw [degree, support_update]
  split_ifs
  · exact (Finset.max_mono (erase_subset _ _)).trans (le_max_left _ _)
  · rw [max_insert, max_comm]
    exact le_rfl
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
a : R
rw : (p.update n a).support.max ≤ max p.degree (↑n : WithBot ℕ)
rw₁ rw₂ rw₃ : (if a = 0 then p.support.erase n else insert n p.support).max ≤ max p.degree (↑n : WithBot ℕ)
pos : a = 0 → (p.support.erase n).max ≤ max p.degree (↑n : WithBot ℕ)
⊢ (p.update n a).degree ≤ max p.degree (↑n : WithBot ℕ)
have neg : ¬a = 0 → (insert n p.support).max ≤ max p.degree (↑n : WithBot ℕ)
Tactic: classical
  rw [degree, support_update]
  split_ifs
  · exact (Finset.max_mono (erase_subset _ _)).trans (le_max_left _ _)
  · rw [max_insert, max_comm]
    exact le_rfl
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type u_1
s_1 : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : degree.{u} (R := R) (∑ i ∈ s, f i) ≤ s.sup fun (b : ι) ↦ (f b).degree
⊢ degree.{u} (R := R) (∑ i ∈ cons a s has, f i) ≤ max (f a).degree (degree.{u} (R := R) (∑ i ∈ s, f i))
have rw : (f a + ∑ x ∈ s, f x).degree ≤ max (f a).degree (degree.{u} (R := R) (∑ i ∈ s, f i))
Tactic: rw [Finset.sum_cons]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
ι : Type u_1
s_1 : Finset ι
f : ι → R[X]
a : ι
s : Finset ι
has : a ∉ s
ih : degree.{u} (R := R) (∑ i ∈ s, f i) ≤ s.sup fun (b : ι) ↦ (f b).degree
⊢ max (f a).degree (degree.{u} (R := R) (∑ i ∈ s, f i)) ≤ (cons a s has).sup fun (b : ι) ↦ (f b).degree
have rw : max (f a).degree (degree.{u} (R := R) (∑ i ∈ s, f i)) ≤ max (f a).degree (s.sup fun (b : ι) ↦ (f b).degree)
Tactic: rw [sup_cons]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
a b : WithBot ℕ
hp : p.degree ≤ a
hq : q.degree ≤ b
⊢ (p * q).degree ≤ a + b
have grw : p.degree + q.degree ≤ a + b
Tactic: grw [degree_mul_le, hp, hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
a b : WithBot ℕ
hp : p.degree ≤ a
hq : q.degree ≤ b
grw : p.degree + q.degree ≤ a + b
⊢ (p * q).degree ≤ a + b
have grw₁ : a + q.degree ≤ a + b
Tactic: grw [degree_mul_le, hp, hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
a b : WithBot ℕ
hp : p.degree ≤ a
hq : q.degree ≤ b
grw : p.degree + q.degree ≤ a + b
grw₁ : a + q.degree ≤ a + b
⊢ (p * q).degree ≤ a + b
have grw₂ : a + b ≤ a + b
Tactic: grw [degree_mul_le, hp, hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ (HPow.hPow (β := ℕ) p 0).degree ≤ HSMul.hSMul (α := ℕ) 0 p.degree
have rw : degree.{u} (R := R) 1 ≤ 0
Tactic: rw [pow_zero, zero_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ (p ^ (n + 1)).degree ≤ (n + 1) • p.degree
have grw : (p ^ n * p).degree ≤ (n + 1) • p.degree
Tactic: grw [pow_succ, succ_nsmul, degree_mul_le, degree_pow_le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
grw : (p ^ n * p).degree ≤ (n + 1) • p.degree
⊢ (p ^ (n + 1)).degree ≤ (n + 1) • p.degree
have grw₁ : (p ^ n * p).degree ≤ n • p.degree + p.degree
Tactic: grw [pow_succ, succ_nsmul, degree_mul_le, degree_pow_le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
grw : (p ^ n * p).degree ≤ (n + 1) • p.degree
grw₁ : (p ^ n * p).degree ≤ n • p.degree + p.degree
⊢ (p ^ (n + 1)).degree ≤ (n + 1) • p.degree
have grw₂ : (p ^ n).degree + p.degree ≤ n • p.degree + p.degree
Tactic: grw [pow_succ, succ_nsmul, degree_mul_le, degree_pow_le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
grw : (p ^ n * p).degree ≤ (n + 1) • p.degree
grw₁ : (p ^ n * p).degree ≤ n • p.degree + p.degree
grw₂ : (p ^ n).degree + p.degree ≤ n • p.degree + p.degree
⊢ (p ^ (n + 1)).degree ≤ (n + 1) • p.degree
have grw₃ : n • p.degree + p.degree ≤ n • p.degree + p.degree
Tactic: grw [pow_succ, succ_nsmul, degree_mul_le, degree_pow_le]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : WithBot ℕ
hp : p.degree ≤ a
n : ℕ
hn : (p ^ n).degree ≤ (↑n : WithBot ℕ) * a
⊢ (p ^ (n + 1)).degree ≤ (↑(n + 1) : WithBot ℕ) * a
have succ : (p ^ n * p).degree ≤ (↑n : WithBot ℕ) * a + a
Tactic: rw [Nat.cast_succ, add_mul, one_mul, pow_succ]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : WithBot ℕ
b : ℕ
hp : p.degree ≤ a
⊢ (p ^ b).degree ≤ (↑b : WithBot ℕ) * a
have zero : (HPow.hPow (β := ℕ) p 0).degree ≤ (↑0 : WithBot ℕ) * a
Tactic: induction b with
  | zero => simp [degree_one_le]
  | succ n hn =>
      rw [Nat.cast_succ, add_mul, one_mul, pow_succ]
      exact degree_mul_le_of_le hn hp
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
a : WithBot ℕ
b : ℕ
hp : p.degree ≤ a
zero : (HPow.hPow (β := ℕ) p 0).degree ≤ (↑0 : WithBot ℕ) * a
⊢ (p ^ b).degree ≤ (↑b : WithBot ℕ) * a
have succ : ∀ (n : ℕ) (hn : (p ^ n).degree ≤ (↑n : WithBot ℕ) * a), (p ^ (n + 1)).degree ≤ (↑(n + 1) : WithBot ℕ) * a
Tactic: induction b with
  | zero => simp [degree_one_le]
  | succ n hn =>
      rw [Nat.cast_succ, add_mul, one_mul, pow_succ]
      exact degree_mul_le_of_le hn hp
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
⊢ leadingCoeff ((monomial n : (a : R) → R[X]) a) = a
have pos : ∀ (ha : a = 0), leadingCoeff ((monomial n : (a : R) → R[X]) a) = a
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
pos : ∀ (ha : a = 0), leadingCoeff ((monomial n : (a : R) → R[X]) a) = a
⊢ leadingCoeff ((monomial n : (a : R) → R[X]) a) = a
have neg : ∀ (ha : ¬a = 0), leadingCoeff ((monomial n : (a : R) → R[X]) a) = a
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
ha : ¬a = 0
⊢ leadingCoeff ((monomial n : (a : R) → R[X]) a) = a
have neg : (if n = n then a else 0) = a
Tactic: rw [leadingCoeff, natDegree_monomial, if_neg ha, coeff_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
⊢ leadingCoeff ((monomial n : (a : R) → R[X]) a) = a
have pos : ∀ (ha : a = 0), leadingCoeff ((monomial n : (a : R) → R[X]) a) = a
Tactic: classical
  by_cases ha : a = 0
  · simp only [ha, (monomial n).map_zero, leadingCoeff_zero]
  · rw [leadingCoeff, natDegree_monomial, if_neg ha, coeff_monomial]
    simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
pos : ∀ (ha : a = 0), leadingCoeff ((monomial n : (a : R) → R[X]) a) = a
⊢ leadingCoeff ((monomial n : (a : R) → R[X]) a) = a
have neg : ∀ (ha : ¬a = 0), leadingCoeff ((monomial n : (a : R) → R[X]) a) = a
Tactic: classical
  by_cases ha : a = 0
  · simp only [ha, (monomial n).map_zero, leadingCoeff_zero]
  · rw [leadingCoeff, natDegree_monomial, if_neg ha, coeff_monomial]
    simp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).leadingCoeff = a
have rw : leadingCoeff ((monomial n : (a : R) → R[X]) a) = a
Tactic: rw [C_mul_X_pow_eq_monomial, leadingCoeff_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
a : R
n : ℕ
rw : leadingCoeff ((monomial n : (a : R) → R[X]) a) = a
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).leadingCoeff = a
have rw₁ : a = a
Tactic: rw [C_mul_X_pow_eq_monomial, leadingCoeff_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (hypothesis)
Goal:
R : Type u
inst : Semiring R
h : Ne.{u + 1} (α := R) 0 1
p : R[X]
hp : p.Monic
⊢ p ≠ 0
have inst : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ (p * q).natDegree ≤ p.natDegree + q.natDegree
have a : (p * q).degree ≤ (↑(p.natDegree + q.natDegree) : WithBot ℕ)
Tactic: apply natDegree_le_of_degree_le
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ (p * q).degree ≤ (↑(p.natDegree + q.natDegree) : WithBot ℕ)
have a : p.degree + q.degree ≤ (↑(p.natDegree + q.natDegree) : WithBot ℕ)
Tactic: apply le_trans (degree_mul_le p q)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ p.degree + q.degree ≤ HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
have a : p.degree ≤ (↑p.natDegree : WithBot ℕ)
Tactic: apply add_le_add
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
a : p.degree ≤ (↑p.natDegree : WithBot ℕ)
⊢ p.degree + q.degree ≤ HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
have a₁ : q.degree ≤ (↑q.natDegree : WithBot ℕ)
Tactic: apply add_le_add
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
ih : (p ^ n).natDegree ≤ n * p.natDegree
⊢ (p ^ (n + 1)).natDegree ≤ (n + 1) * p.natDegree
have succ : (p ^ n * p).natDegree ≤ (n + 1) * p.natDegree
Tactic: grw [pow_succ, Nat.succ_mul, natDegree_mul_le, ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
ih : (p ^ n).natDegree ≤ n * p.natDegree
succ : (p ^ n * p).natDegree ≤ (n + 1) * p.natDegree
⊢ (p ^ (n + 1)).natDegree ≤ (n + 1) * p.natDegree
have succ₁ : (p ^ n * p).natDegree ≤ n * p.natDegree + p.natDegree
Tactic: grw [pow_succ, Nat.succ_mul, natDegree_mul_le, ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
ih : (p ^ n).natDegree ≤ n * p.natDegree
succ : (p ^ n * p).natDegree ≤ (n + 1) * p.natDegree
succ₁ : (p ^ n * p).natDegree ≤ n * p.natDegree + p.natDegree
⊢ (p ^ (n + 1)).natDegree ≤ (n + 1) * p.natDegree
have succ₂ : (p ^ n).natDegree + p.natDegree ≤ n * p.natDegree + p.natDegree
Tactic: grw [pow_succ, Nat.succ_mul, natDegree_mul_le, ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
ih : (p ^ n).natDegree ≤ n * p.natDegree
succ : (p ^ n * p).natDegree ≤ (n + 1) * p.natDegree
succ₁ : (p ^ n * p).natDegree ≤ n * p.natDegree + p.natDegree
succ₂ : (p ^ n).natDegree + p.natDegree ≤ n * p.natDegree + p.natDegree
⊢ (p ^ (n + 1)).natDegree ≤ (n + 1) * p.natDegree
have succ₃ : n * p.natDegree + p.natDegree ≤ n * p.natDegree + p.natDegree
Tactic: grw [pow_succ, Nat.succ_mul, natDegree_mul_le, ih]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ (p ^ n).natDegree ≤ n * p.natDegree
have zero : (HPow.hPow (β := ℕ) p 0).natDegree ≤ 0 * p.natDegree
Tactic: induction n with
  | zero => simp
  | succ n ih => grw [pow_succ, Nat.succ_mul, natDegree_mul_le, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
zero : (HPow.hPow (β := ℕ) p 0).natDegree ≤ 0 * p.natDegree
⊢ (p ^ n).natDegree ≤ n * p.natDegree
have succ : ∀ (n : ℕ) (ih : (p ^ n).natDegree ≤ n * p.natDegree), (p ^ (n + 1)).natDegree ≤ (n + 1) * p.natDegree
Tactic: induction n with
  | zero => simp
  | succ n ih => grw [pow_succ, Nat.succ_mul, natDegree_mul_le, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.natDegree = 0 ↔ p.degree ≤ 0
have rw : p.natDegree ≤ 0 ↔ p.degree ≤ 0
Tactic: rw [← nonpos_iff_eq_zero, natDegree_le_iff_degree_le, Nat.cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : p.natDegree ≤ 0 ↔ p.degree ≤ 0
⊢ p.natDegree = 0 ↔ p.degree ≤ 0
have rw₁ : p.degree ≤ (↑0 : WithBot ℕ) ↔ p.degree ≤ 0
Tactic: rw [← nonpos_iff_eq_zero, natDegree_le_iff_degree_le, Nat.cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : p.natDegree ≤ 0 ↔ p.degree ≤ 0
rw₁ : p.degree ≤ (↑0 : WithBot ℕ) ↔ p.degree ≤ 0
⊢ p.natDegree = 0 ↔ p.degree ≤ 0
have rw₂ : p.degree ≤ 0 ↔ p.degree ≤ 0
Tactic: rw [← nonpos_iff_eq_zero, natDegree_le_iff_degree_le, Nat.cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
⊢ (HPow.hPow (α := R[X]) X n).degree = (↑n : WithBot ℕ)
have rw : degree.{u} (R := R) ((monomial n : (a : R) → R[X]) 1) = (↑n : WithBot ℕ)
Tactic: rw [X_pow_eq_monomial, degree_monomial _ (one_ne_zero' R)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
rw : degree.{u} (R := R) ((monomial n : (a : R) → R[X]) 1) = (↑n : WithBot ℕ)
⊢ (HPow.hPow (α := R[X]) X n).degree = (↑n : WithBot ℕ)
have rw₁ : Eq (α := WithBot ℕ) (↑n : WithBot ℕ) (↑n : WithBot ℕ)
Tactic: rw [X_pow_eq_monomial, degree_monomial _ (one_ne_zero' R)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : HAdd.hAdd (α := R[X]) ((monomial p.natDegree : (a : R) → R[X]) p.leadingCoeff : R[X]) (erase p.natDegree p) = p
hq : HAdd.hAdd (α := R[X]) ((monomial q.natDegree : (a : R) → R[X]) q.leadingCoeff : R[X]) (erase q.natDegree q) = q
⊢ WithBot.unbotD 0 p.degree = WithBot.unbotD 0 q.degree
have rw : WithBot.unbotD 0 q.degree = WithBot.unbotD 0 q.degree
Tactic: rw [hd]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : HAdd.hAdd (α := R[X]) ((monomial p.natDegree : (a : R) → R[X]) p.leadingCoeff : R[X]) (erase p.natDegree p) = p
hq : HAdd.hAdd (α := R[X]) ((monomial q.natDegree : (a : R) → R[X]) q.leadingCoeff : R[X]) (erase q.natDegree q) = q
hd' : p.natDegree = q.natDegree
hq0 : q ≠ 0
| (p - q).degree = (erase q.natDegree p + -erase q.natDegree q).degree
have lhs : (p - q).degree
Tactic: lhs
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Defs (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
hd : p.degree = q.degree
hp0 : p ≠ 0
hlc : p.leadingCoeff = q.leadingCoeff
hp : HAdd.hAdd (α := R[X]) ((monomial p.natDegree : (a : R) → R[X]) p.leadingCoeff : R[X]) (erase p.natDegree p) = p
hq : HAdd.hAdd (α := R[X]) ((monomial q.natDegree : (a : R) → R[X]) q.leadingCoeff : R[X]) (erase q.natDegree q) = q
hd' : p.natDegree = q.natDegree
hq0 : q ≠ 0
| (p - q).degree
have rw : (erase q.natDegree p + -erase q.natDegree q).degree
Tactic: rw [← hp, ← hq, hlc, hd', add_sub_add_left_eq_sub, sub_eq_add_neg]