awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : HPow.hPow (β := ℕ) p.leadingCoeff 0 ≠ 0
⊢ (HPow.hPow (β := ℕ) p 0).degree = HSMul.hSMul (α := ℕ) 0 p.degree
have h₁ : Ne.{u + 1} (α := R) 1 0
Tactic: rw [pow_zero, ← C_1] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : Ne.{u + 1} (α := R) 1 0
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) 1) = HSMul.hSMul (α := ℕ) 0 p.degree
have rw : 0 = HSMul.hSMul (α := ℕ) 0 p.degree
Tactic: rw [degree_C h, zero_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : Ne.{u + 1} (α := R) 1 0
rw : 0 = HSMul.hSMul (α := ℕ) 0 p.degree
⊢ degree.{u} (R := R) ((C : (a : R) → R[X]) 1) = HSMul.hSMul (α := ℕ) 0 p.degree
have rw₁ : Eq (α := WithBot ℕ) 0 0
Tactic: rw [degree_C h, zero_nsmul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n = 0
⊢ p.leadingCoeff ^ (n + 1) = 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
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n = 0
rw : p.leadingCoeff ^ n * p.leadingCoeff = 0
⊢ p.leadingCoeff ^ (n + 1) = 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
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n = 0
rw : p.leadingCoeff ^ n * p.leadingCoeff = 0
rw₁ : 0 * p.leadingCoeff = 0
⊢ p.leadingCoeff ^ (n + 1) = 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
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
⊢ (p ^ (n + 1)).degree = (n + 1) • p.degree
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
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
⊢ (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
have rwa : ∀ (h : p.leadingCoeff ^ n * p.leadingCoeff ≠ 0) (h₁ : p.leadingCoeff ^ n ≠ 0), (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
Tactic: rwa [pow_succ, ← leadingCoeff_pow' h₁] 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 : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
rwa :
  ∀ (h : p.leadingCoeff ^ n * p.leadingCoeff ≠ 0) (h₁ : p.leadingCoeff ^ n ≠ 0),
    (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
⊢ (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
have rwa₁ : ∀ (h : (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0) (h₁ : p.leadingCoeff ^ n ≠ 0),
  (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
Tactic: rwa [pow_succ, ← leadingCoeff_pow' h₁] at h
Cleared hypotheses: h, h₁
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
⊢ (p ^ (n + 1)).degree = (n + 1) • p.degree
have h₂ : (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
Tactic: have h₂ : leadingCoeff (p ^ n) * leadingCoeff p ≠ 0 := by
      rwa [pow_succ, ← leadingCoeff_pow' h₁] at h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
⊢ (p ^ (n + 1)).degree = (n + 1) • p.degree
have rw : (p ^ n * p).degree = (n + 1) • p.degree
Tactic: rw [pow_succ, degree_mul' h₂, succ_nsmul, degree_pow' h₁]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
rw : (p ^ n * p).degree = (n + 1) • p.degree
⊢ (p ^ (n + 1)).degree = (n + 1) • p.degree
have rw₁ : (p ^ n).degree + p.degree = (n + 1) • p.degree
Tactic: rw [pow_succ, degree_mul' h₂, succ_nsmul, degree_pow' h₁]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
rw : (p ^ n * p).degree = (n + 1) • p.degree
rw₁ : (p ^ n).degree + p.degree = (n + 1) • p.degree
⊢ (p ^ (n + 1)).degree = (n + 1) • p.degree
have rw₂ : (p ^ n).degree + p.degree = n • p.degree + p.degree
Tactic: rw [pow_succ, degree_mul' h₂, succ_nsmul, degree_pow' h₁]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
h₁ : p.leadingCoeff ^ n ≠ 0
h₂ : (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0
rw : (p ^ n * p).degree = (n + 1) • p.degree
rw₁ : (p ^ n).degree + p.degree = (n + 1) • p.degree
rw₂ : (p ^ n).degree + p.degree = n • p.degree + p.degree
⊢ (p ^ (n + 1)).degree = (n + 1) • p.degree
have rw₃ : n • p.degree + p.degree = n • p.degree + p.degree
Tactic: rw [pow_succ, degree_mul' h₂, succ_nsmul, degree_pow' h₁]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : p = 0
hn0 : ¬n = 0
⊢ (p ^ n).natDegree = n * p.natDegree
have rw : natDegree.{u} (R := R) 0 = n * natDegree.{u} (R := R) 0
Tactic: rw [hp0, zero_pow hn0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn0 : p ^ n = 0
h1 : p.leadingCoeff ^ n ≠ 0
⊢ False
have h₁ : Ne.{u + 1} (α := R) 0 0
Tactic: rw [← leadingCoeff_pow' h1, hpn0, leadingCoeff_zero] at h
Cleared hypotheses: h, this, hp0, hpn0, h1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ n ≠ 0
this : DecidableEq R := Classical.decEq R
hp0 : ¬p = 0
hpn : p ^ n ≠ 0
⊢ Eq (α := WithBot ℕ) (↑(p ^ n).natDegree : WithBot ℕ) (↑(n * p.natDegree) : WithBot ℕ)
have rw : HSMul.hSMul (β := WithBot ℕ) n (↑p.natDegree : WithBot ℕ) = (↑(n * p.natDegree) : WithBot ℕ)
Tactic: rw [← degree_eq_natDegree hpn, degree_pow' h, degree_eq_natDegree hp0]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
⊢ (p * q).leadingCoeff = q.leadingCoeff
have inl : (p * 0).leadingCoeff = leadingCoeff 0
Tactic: rcases eq_or_ne q 0 with (rfl | H)
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
inl : (p * 0).leadingCoeff = leadingCoeff 0
⊢ (p * q).leadingCoeff = q.leadingCoeff
have inr : ∀ (H : q ≠ 0), (p * q).leadingCoeff = q.leadingCoeff
Tactic: rcases eq_or_ne q 0 with (rfl | H)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ (p * q).leadingCoeff = q.leadingCoeff
have inr : p.leadingCoeff * q.leadingCoeff ≠ 0
Tactic: rw [leadingCoeff_mul', hp.leadingCoeff, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
hp : p.Monic
H : q ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
have inr : 1 * q.leadingCoeff ≠ 0
Tactic: rwa [hp.leadingCoeff, one_mul, 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]
hp : p.Monic
H : q ≠ 0
inr : 1 * q.leadingCoeff ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
have inr₁ : q.leadingCoeff ≠ 0
Tactic: rwa [hp.leadingCoeff, one_mul, 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]
hp : p.Monic
H : q ≠ 0
inr : 1 * q.leadingCoeff ≠ 0
inr₁ : q.leadingCoeff ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
have inr₂ : ¬q.leadingCoeff = 0
Tactic: rwa [hp.leadingCoeff, one_mul, 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]
hp : p.Monic
H : q ≠ 0
inr : 1 * q.leadingCoeff ≠ 0
inr₁ : q.leadingCoeff ≠ 0
inr₂ : ¬q.leadingCoeff = 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
have inr₃ : ¬q = 0
Tactic: rwa [hp.leadingCoeff, one_mul, 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
H : p.leadingCoeff = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff
have rw : (p * q).leadingCoeff = 0
Tactic: rw [H, leadingCoeff_eq_zero.1 H, zero_mul, leadingCoeff_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
H : p.leadingCoeff = 0
rw : (p * q).leadingCoeff = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff
have rw₁ : (0 * q).leadingCoeff = 0
Tactic: rw [H, leadingCoeff_eq_zero.1 H, zero_mul, leadingCoeff_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
H : p.leadingCoeff = 0
rw : (p * q).leadingCoeff = 0
rw₁ : (0 * q).leadingCoeff = 0
⊢ (p * q).leadingCoeff = p.leadingCoeff
have rw₂ : Eq.{u + 1} (α := R) (leadingCoeff 0) 0
Tactic: rw [H, leadingCoeff_eq_zero.1 H, zero_mul, leadingCoeff_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
H : p.leadingCoeff = 0
rw : (p * q).leadingCoeff = 0
rw₁ : (0 * q).leadingCoeff = 0
rw₂ : Eq.{u + 1} (α := R) (leadingCoeff 0) 0
⊢ (p * q).leadingCoeff = p.leadingCoeff
have rw₃ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [H, leadingCoeff_eq_zero.1 H, zero_mul, leadingCoeff_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
H : p.leadingCoeff ≠ 0
⊢ (p * q).leadingCoeff = p.leadingCoeff
have rw : p.leadingCoeff * q.leadingCoeff ≠ 0
Tactic: rw [leadingCoeff_mul', hq.leadingCoeff, mul_one]
-- 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
H : p.leadingCoeff ≠ 0
⊢ p.leadingCoeff * q.leadingCoeff ≠ 0
have rwa : p.leadingCoeff * 1 ≠ 0
Tactic: rwa [hq.leadingCoeff, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).degree = p.degree
have inl : (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (0 : R[X])).degree = degree.{u} (R := R) 0
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
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
inl : (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) (0 : R[X])).degree = degree.{u} (R := R) 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).degree = p.degree
have inr : ∀ (hp : p ≠ 0), (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).degree = p.degree
Tactic: obtain rfl | hp := eq_or_ne p 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).degree = p.degree
have a₁ : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
h : Nontrivial R
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).degree = p.degree
have rw : 0 + p.degree = p.degree
Tactic: rw [degree_mul', degree_C ha.ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
h : Nontrivial R
rw : 0 + p.degree = p.degree
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).degree = p.degree
have rw₁ : leadingCoeff ((C : (a : R) → R[X]) a) * p.leadingCoeff ≠ 0
Tactic: rw [degree_mul', degree_C ha.ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).degree = p.degree
have inl : (HMul.hMul (α := R[X]) (β := R[X]) (0 : R[X]) ((C : (a : R) → R[X]) a : R[X])).degree = degree.{u} (R := R) 0
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
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
inl : (HMul.hMul (α := R[X]) (β := R[X]) (0 : R[X]) ((C : (a : R) → R[X]) a : R[X])).degree = degree.{u} (R := R) 0
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).degree = p.degree
have inr : ∀ (hp : p ≠ 0), (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).degree = p.degree
Tactic: obtain rfl | hp := eq_or_ne p 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).degree = p.degree
have a₁ : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
h : Nontrivial R
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).degree = p.degree
have rw : p.degree + 0 = p.degree
Tactic: rw [degree_mul', degree_C ha.ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
hp : p ≠ 0
h : Nontrivial R
rw : p.degree + 0 = p.degree
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).degree = p.degree
have rw₁ : p.leadingCoeff * leadingCoeff ((C : (a : R) → R[X]) a) ≠ 0
Tactic: rw [degree_mul', degree_C ha.ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).leadingCoeff = a * p.leadingCoeff
have rwa : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).coeff
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).natDegree =
  a * p.leadingCoeff
Tactic: rwa [leadingCoeff, coeff_C_mul, natDegree_C_mul_of_isUnit, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
rwa :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).coeff
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).natDegree =
    a * p.leadingCoeff
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).leadingCoeff = a * p.leadingCoeff
have rwa₁ : a * p.coeff (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).natDegree = a * p.leadingCoeff
Tactic: rwa [leadingCoeff, coeff_C_mul, natDegree_C_mul_of_isUnit, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
rwa :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).coeff
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).natDegree =
    a * p.leadingCoeff
rwa₁ : a * p.coeff (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).natDegree = a * p.leadingCoeff
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).leadingCoeff = a * p.leadingCoeff
have rwa₂ : a * p.coeff p.natDegree = a * p.leadingCoeff
Tactic: rwa [leadingCoeff, coeff_C_mul, natDegree_C_mul_of_isUnit, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
rwa :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).coeff
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).natDegree =
    a * p.leadingCoeff
rwa₁ : a * p.coeff (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).natDegree = a * p.leadingCoeff
rwa₂ : a * p.coeff p.natDegree = a * p.leadingCoeff
ha₁ : IsUnit a
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).leadingCoeff = a * p.leadingCoeff
have rwa₃ : a * p.coeff p.natDegree = a * p.coeff p.natDegree
Tactic: rwa [leadingCoeff, coeff_C_mul, natDegree_C_mul_of_isUnit, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = p.leadingCoeff * a
have rwa : (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).coeff
    (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree =
  p.leadingCoeff * a
Tactic: rwa [leadingCoeff, coeff_mul_C, natDegree_mul_C_of_isUnit, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
rwa :
  (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).coeff
      (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree =
    p.leadingCoeff * a
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = p.leadingCoeff * a
have rwa₁ : p.coeff (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree * a = p.leadingCoeff * a
Tactic: rwa [leadingCoeff, coeff_mul_C, natDegree_mul_C_of_isUnit, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
rwa :
  (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).coeff
      (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree =
    p.leadingCoeff * a
rwa₁ : p.coeff (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree * a = p.leadingCoeff * a
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = p.leadingCoeff * a
have rwa₂ : p.coeff p.natDegree * a = p.leadingCoeff * a
Tactic: rwa [leadingCoeff, coeff_mul_C, natDegree_mul_C_of_isUnit, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
a : R
inst : Semiring R
ha : IsUnit a
p : R[X]
rwa :
  (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).coeff
      (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree =
    p.leadingCoeff * a
rwa₁ : p.coeff (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree * a = p.leadingCoeff * a
rwa₂ : p.coeff p.natDegree * a = p.leadingCoeff * a
ha₁ : IsUnit a
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).leadingCoeff = p.leadingCoeff * a
have rwa₃ : p.coeff p.natDegree * a = p.coeff p.natDegree * a
Tactic: rwa [leadingCoeff, coeff_mul_C, natDegree_mul_C_of_isUnit, leadingCoeff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
⊢ (p ^ (i + 1)).coeff ((i + 1) * p.natDegree) = p.leadingCoeff ^ (i + 1)
have succ : (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff
Tactic: rw [pow_succ, pow_succ, Nat.succ_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff
have pos : ∀ (hp1 : p.leadingCoeff ^ i = 0),
  (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff
Tactic: by_cases hp1 : p.leadingCoeff ^ i = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
pos :
  ∀ (hp1 : p.leadingCoeff ^ i = 0),
    (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff
have neg : ∀ (hp1 : ¬p.leadingCoeff ^ i = 0),
  (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff
Tactic: by_cases hp1 : p.leadingCoeff ^ i = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff
have pos : (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0
Tactic: rw [hp1, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0
have pos : ∀ (hp2 : p ^ i = 0), (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0
Tactic: by_cases hp2 : p ^ i = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
pos : ∀ (hp2 : p ^ i = 0), (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0
have neg : ∀ (hp2 : ¬p ^ i = 0), (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0
Tactic: by_cases hp2 : p ^ i = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : p ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0
have pos : (0 * p).coeff (i * p.natDegree + p.natDegree) = 0
Tactic: rw [hp2, zero_mul, coeff_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : p ^ i = 0
pos : (0 * p).coeff (i * p.natDegree + p.natDegree) = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0
have pos₁ : Eq.{u + 1} (α := R) (coeff 0 (i * p.natDegree + p.natDegree)) 0
Tactic: rw [hp2, zero_mul, coeff_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : p ^ i = 0
pos : (0 * p).coeff (i * p.natDegree + p.natDegree) = 0
pos₁ : Eq.{u + 1} (α := R) (coeff 0 (i * p.natDegree + p.natDegree)) 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0
have pos₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [hp2, zero_mul, coeff_zero]