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
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff + q.leadingCoeff ≠ 0
⊢ (p + q).natDegree = p.natDegree
have h₁ : (p + q).degree = p.degree
Tactic: apply natDegree_eq_of_degree_eq
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff + q.leadingCoeff ≠ 0
⊢ (p + q).degree = p.degree
have h₁ : max p.degree q.degree = p.degree
Tactic: rw [degree_add_eq_of_leadingCoeff_add_ne_zero hlc, h, max_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff + q.leadingCoeff ≠ 0
h₁ : max p.degree q.degree = p.degree
⊢ (p + q).degree = p.degree
have h₂ : max q.degree q.degree = q.degree
Tactic: rw [degree_add_eq_of_leadingCoeff_add_ne_zero hlc, h, max_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff + q.leadingCoeff ≠ 0
h₁ : max p.degree q.degree = p.degree
h₂ : max q.degree q.degree = q.degree
⊢ (p + q).degree = p.degree
have h₃ : q.degree = q.degree
Tactic: rw [degree_add_eq_of_leadingCoeff_add_ne_zero hlc, h, max_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.degree = q.degree
hlc : p.leadingCoeff + q.leadingCoeff ≠ 0
⊢ (p + q).leadingCoeff = p.leadingCoeff + q.leadingCoeff
have this : (p + q).natDegree = p.natDegree
Tactic: have : natDegree (p + q) = natDegree p := by
    apply natDegree_eq_of_degree_eq
    rw [degree_add_eq_of_leadingCoeff_add_ne_zero hlc, h, max_self]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ (p.natDegree + q.natDegree), p.coeff x.1 * q.coeff x.2 =
    p.coeff p.natDegree * q.coeff q.natDegree
have refine_1 : ∀ b ∈ @antidiagonal _ Nat.instAddMonoid _ (p.natDegree + q.natDegree),
  b ≠ (p.natDegree, q.natDegree) → p.coeff b.1 * q.coeff b.2 = 0
Tactic: refine Finset.sum_eq_single (natDegree p, natDegree q) ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
refine_1 :
  ∀ b ∈ @antidiagonal _ Nat.instAddMonoid _ (p.natDegree + q.natDegree),
    b ≠ (p.natDegree, q.natDegree) → p.coeff b.1 * q.coeff b.2 = 0
⊢ ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ (p.natDegree + q.natDegree), p.coeff x.1 * q.coeff x.2 =
    p.coeff p.natDegree * q.coeff q.natDegree
have refine_2 : (p.natDegree, q.natDegree) ∉ @antidiagonal _ Nat.instAddMonoid _ (p.natDegree + q.natDegree) →
  p.coeff (p.natDegree, q.natDegree).1 * q.coeff (p.natDegree, q.natDegree).2 = 0
Tactic: refine Finset.sum_eq_single (natDegree p, natDegree q) ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (p.natDegree + q.natDegree)
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
have h₃ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
Tactic: rw [mem_antidiagonal] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
have pos : ∀ (H : p.natDegree < i), p.coeff (i, j).1 * q.coeff (i, j).2 = 0
Tactic: by_cases H : natDegree p < i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
pos : ∀ (H : p.natDegree < i), p.coeff (i, j).1 * q.coeff (i, j).2 = 0
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
have neg : ∀ (H : ¬p.natDegree < i), p.coeff (i, j).1 * q.coeff (i, j).2 = 0
Tactic: by_cases H : natDegree p < i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree < i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
have pos : 0 * q.coeff (i, j).2 = 0
Tactic: rw [coeff_eq_zero_of_degree_lt
              (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 H)),
            zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree < i
pos : 0 * q.coeff (i, j).2 = 0
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
have pos₁ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [coeff_eq_zero_of_degree_lt
              (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 H)),
            zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : ¬p.natDegree < i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
have H₁ : p.natDegree = i ∨ i < p.natDegree
Tactic: rw [not_lt_iff_eq_or_lt] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree = i ∨ i < p.natDegree
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
have neg : ∀ (H : p.natDegree = i), p.coeff (i, j).1 * q.coeff (i, j).2 = 0
Tactic: rcases H with H | H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : p.natDegree = i ∨ i < p.natDegree
neg : ∀ (H : p.natDegree = i), p.coeff (i, j).1 * q.coeff (i, j).2 = 0
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
have neg₁ : ∀ (H : i < p.natDegree), p.coeff (i, j).1 * q.coeff (i, j).2 = 0
Tactic: rcases H with H | H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
this : q.natDegree < j
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
have rw : p.coeff (i, j).1 * 0 = 0
Tactic: rw [coeff_eq_zero_of_degree_lt
                  (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 this)),
                mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
this : q.natDegree < j
rw : p.coeff (i, j).1 * 0 = 0
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
have rw₁ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [coeff_eq_zero_of_degree_lt
                  (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 this)),
                mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
have neg : q.natDegree < j
Tactic: suffices natDegree q < j by
              rw [coeff_eq_zero_of_degree_lt
                  (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 this)),
                mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natDegree + q.natDegree
h₂ : (i, j) ≠ (p.natDegree, q.natDegree)
H : i < p.natDegree
⊢ q.natDegree < j
have neg : ∀ (H' : j ≤ q.natDegree), False
Tactic: by_contra! H'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p.natDegree, q.natDegree) ∉ @antidiagonal _ Nat.instAddMonoid _ (p.natDegree + q.natDegree)
⊢ p.coeff (p.natDegree, q.natDegree).1 * q.coeff (p.natDegree, q.natDegree).2 = 0
have refine_2 : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p.natDegree, q.natDegree) ∉ @antidiagonal _ Nat.instAddMonoid _ (p.natDegree + q.natDegree)
⊢ False
have refine_2 : (p.natDegree, q.natDegree) ∈ @antidiagonal _ Nat.instAddMonoid _ (p.natDegree + q.natDegree)
Tactic: apply H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
H : (p.natDegree, q.natDegree) ∉ @antidiagonal _ Nat.instAddMonoid _ (p.natDegree + q.natDegree)
⊢ (p.natDegree, q.natDegree) ∈ @antidiagonal _ Nat.instAddMonoid _ (p.natDegree + q.natDegree)
have refine_2 : (p.natDegree, q.natDegree).1 + (p.natDegree, q.natDegree).2 = p.natDegree + q.natDegree
Tactic: rw [mem_antidiagonal]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
⊢ p ≠ 0
have refine : p = 0 → p.leadingCoeff * q.leadingCoeff = 0
Tactic: refine mt ?_ h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p = 0
⊢ p.leadingCoeff * q.leadingCoeff = 0
have rw : leadingCoeff 0 * q.leadingCoeff = 0
Tactic: rw [hp, leadingCoeff_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p = 0
rw : leadingCoeff 0 * q.leadingCoeff = 0
⊢ p.leadingCoeff * q.leadingCoeff = 0
have rw₁ : 0 * q.leadingCoeff = 0
Tactic: rw [hp, leadingCoeff_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p = 0
rw : leadingCoeff 0 * q.leadingCoeff = 0
rw₁ : 0 * q.leadingCoeff = 0
⊢ p.leadingCoeff * q.leadingCoeff = 0
have rw₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [hp, leadingCoeff_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
⊢ q ≠ 0
have refine : q = 0 → p.leadingCoeff * q.leadingCoeff = 0
Tactic: refine mt ?_ h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ p.leadingCoeff * q.leadingCoeff = 0
have rw : p.leadingCoeff * leadingCoeff 0 = 0
Tactic: rw [hq, leadingCoeff_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q = 0
rw : p.leadingCoeff * leadingCoeff 0 = 0
⊢ p.leadingCoeff * q.leadingCoeff = 0
have rw₁ : p.leadingCoeff * 0 = 0
Tactic: rw [hq, leadingCoeff_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q = 0
rw : p.leadingCoeff * leadingCoeff 0 = 0
rw₁ : p.leadingCoeff * 0 = 0
⊢ p.leadingCoeff * q.leadingCoeff = 0
have rw₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [hq, leadingCoeff_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ p.degree + q.degree ≤ (p * q).degree
have rw : HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ) ≤ (p * q).degree
Tactic: rw [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
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ) ≤ (p * q).degree
have refine : (p * q).coeff (p.natDegree + q.natDegree) ≠ 0
Tactic: refine le_degree_of_ne_zero (n := natDegree p + natDegree q) ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
hp : ¬p = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
have rwa : p.leadingCoeff * 1 ≠ 0
Tactic: rwa [hq.leadingCoeff, mul_one, Ne, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
hp : ¬p = 0
rwa : p.leadingCoeff * 1 ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
have rwa₁ : p.leadingCoeff ≠ 0
Tactic: rwa [hq.leadingCoeff, mul_one, Ne, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hq : q.Monic
this : DecidableEq R := Classical.decEq R
hp : ¬p = 0
rwa : p.leadingCoeff * 1 ≠ 0
rwa₁ : p.leadingCoeff ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
have rwa₂ : ¬p.leadingCoeff = 0
Tactic: rwa [hq.leadingCoeff, mul_one, Ne, leadingCoeff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
h₁ : p.leadingCoeff = 0
⊢ p.leadingCoeff * q.leadingCoeff = 0
have rw : 0 * q.leadingCoeff = 0
Tactic: rw [h₁, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
h₁ : p.leadingCoeff = 0
rw : 0 * q.leadingCoeff = 0
⊢ p.leadingCoeff * q.leadingCoeff = 0
have rw₁ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [h₁, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
h₁ : q.leadingCoeff = 0
⊢ p.leadingCoeff * q.leadingCoeff = 0
have rw : p.leadingCoeff * 0 = 0
Tactic: rw [h₁, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
h₁ : q.leadingCoeff = 0
rw : p.leadingCoeff * 0 = 0
⊢ p.leadingCoeff * q.leadingCoeff = 0
have rw₁ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [h₁, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).degree = (↑(p.natDegree + q.natDegree) : WithBot ℕ)
have rw : p.degree + q.degree = (↑(p.natDegree + q.natDegree) : WithBot ℕ)
Tactic: rw [degree_mul' h, Nat.cast_add, 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
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
rw : p.degree + q.degree = (↑(p.natDegree + q.natDegree) : WithBot ℕ)
⊢ (p * q).degree = (↑(p.natDegree + q.natDegree) : WithBot ℕ)
have rw₁ : p.degree + q.degree = HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
Tactic: rw [degree_mul' h, Nat.cast_add, 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
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
rw : p.degree + q.degree = (↑(p.natDegree + q.natDegree) : WithBot ℕ)
rw₁ : p.degree + q.degree = HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
⊢ (p * q).degree = (↑(p.natDegree + q.natDegree) : WithBot ℕ)
have rw₂ : (↑p.natDegree : WithBot ℕ) + q.degree = HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
Tactic: rw [degree_mul' h, Nat.cast_add, 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
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
rw : p.degree + q.degree = (↑(p.natDegree + q.natDegree) : WithBot ℕ)
rw₁ : p.degree + q.degree = HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
rw₂ :
  (↑p.natDegree : WithBot ℕ) + q.degree =
    HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
⊢ (p * q).degree = (↑(p.natDegree + q.natDegree) : WithBot ℕ)
have rw₃ : HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ) =
  HAdd.hAdd (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑q.natDegree : WithBot ℕ)
Tactic: rw [degree_mul' h, Nat.cast_add, 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
p : R[X]
hp : p.Monic
r : R
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).leadingCoeff = r
have pos : ∀ (hr : r = 0), (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).leadingCoeff = r
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.Monic
r : R
pos : ∀ (hr : r = 0), (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).leadingCoeff = r
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).leadingCoeff = r
have neg : ∀ (hr : ¬r = 0), (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) p).leadingCoeff = r
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
n_1 : ℕ
inst : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n = 0
⊢ p.leadingCoeff ^ n.succ = 0
have rw : p.leadingCoeff ^ n * p.leadingCoeff = 0
Tactic: rw [pow_succ, h₁, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
n_1 : ℕ
inst : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n = 0
rw : p.leadingCoeff ^ n * p.leadingCoeff = 0
⊢ p.leadingCoeff ^ n.succ = 0
have rw₁ : 0 * p.leadingCoeff = 0
Tactic: rw [pow_succ, h₁, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
n_1 : ℕ
inst : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n = 0
rw : p.leadingCoeff ^ n * p.leadingCoeff = 0
rw₁ : 0 * p.leadingCoeff = 0
⊢ p.leadingCoeff ^ n.succ = 0
have rw₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [pow_succ, h₁, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
n_1 : ℕ
inst : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
⊢ (p ^ n.succ).leadingCoeff = p.leadingCoeff ^ n.succ
have h₁ : p.leadingCoeff ^ n ≠ 0
Tactic: have h₁ : leadingCoeff p ^ n ≠ 0 := fun h₁ => h <| by rw [pow_succ, h₁, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
n_1 : ℕ
inst : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
⊢ p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
have rwa : ∀ (h : p.leadingCoeff * p.leadingCoeff ^ n ≠ 0) (h₁ : p.leadingCoeff ^ n ≠ 0), p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
Tactic: rwa [pow_succ', ← ih h₁] at h
Cleared hypotheses: h, h₁
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
n_1 : ℕ
inst : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
rwa :
  ∀ (h : p.leadingCoeff * p.leadingCoeff ^ n ≠ 0) (h₁ : p.leadingCoeff ^ n ≠ 0),
    p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
⊢ p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
have rwa₁ : ∀ (h : p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0) (h₁ : p.leadingCoeff ^ n ≠ 0),
  p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
Tactic: rwa [pow_succ', ← ih h₁] at h
Cleared hypotheses: h, h₁
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
n_1 : ℕ
inst : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
⊢ (p ^ n.succ).leadingCoeff = p.leadingCoeff ^ n.succ
have h₂ : p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
Tactic: have h₂ : leadingCoeff p * leadingCoeff (p ^ n) ≠ 0 := by rwa [pow_succ', ← ih h₁] at h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
n_1 : ℕ
inst : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
⊢ (p ^ n.succ).leadingCoeff = p.leadingCoeff ^ n.succ
have rw : (p * p ^ n).leadingCoeff = p.leadingCoeff ^ n.succ
Tactic: rw [pow_succ', pow_succ', leadingCoeff_mul' h₂, ih h₁]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
n_1 : ℕ
inst : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
rw : (p * p ^ n).leadingCoeff = p.leadingCoeff ^ n.succ
⊢ (p ^ n.succ).leadingCoeff = p.leadingCoeff ^ n.succ
have rw₁ : (p * p ^ n).leadingCoeff = p.leadingCoeff * p.leadingCoeff ^ n
Tactic: rw [pow_succ', pow_succ', leadingCoeff_mul' h₂, ih h₁]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
n_1 : ℕ
inst : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
rw : (p * p ^ n).leadingCoeff = p.leadingCoeff ^ n.succ
rw₁ : (p * p ^ n).leadingCoeff = p.leadingCoeff * p.leadingCoeff ^ n
⊢ (p ^ n.succ).leadingCoeff = p.leadingCoeff ^ n.succ
have rw₂ : p.leadingCoeff * (p ^ n).leadingCoeff = p.leadingCoeff * p.leadingCoeff ^ n
Tactic: rw [pow_succ', pow_succ', leadingCoeff_mul' h₂, ih h₁]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
n_1 : ℕ
inst : Semiring R
p : R[X]
n : ℕ
ih : p.leadingCoeff ^ n ≠ 0 → (p ^ n).leadingCoeff = p.leadingCoeff ^ n
h : p.leadingCoeff ^ n.succ ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : p.leadingCoeff * (p ^ n).leadingCoeff ≠ 0
rw : (p * p ^ n).leadingCoeff = p.leadingCoeff ^ n.succ
rw₁ : (p * p ^ n).leadingCoeff = p.leadingCoeff * p.leadingCoeff ^ n
rw₂ : p.leadingCoeff * (p ^ n).leadingCoeff = p.leadingCoeff * p.leadingCoeff ^ n
⊢ (p ^ n.succ).leadingCoeff = p.leadingCoeff ^ n.succ
have rw₃ : p.leadingCoeff * p.leadingCoeff ^ n = p.leadingCoeff * p.leadingCoeff ^ n
Tactic: rw [pow_succ', pow_succ', leadingCoeff_mul' h₂, ih h₁]