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 : 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 neg : (p ^ i * p).natDegree < i * p.natDegree + p.natDegree
Tactic: apply coeff_eq_zero_of_natDegree_lt
-- 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).natDegree < i * p.natDegree
have refine : ∀ (h : (p ^ i).natDegree = i * p.natDegree), p ^ i = 0
Tactic: refine lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
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
h : (p ^ i).natDegree = i * p.natDegree
⊢ p ^ i = 0
have hi₁ : (p ^ i).coeff (p ^ i).natDegree = 0
Tactic: rw [← h, hp1] at hi
Cleared hypotheses: hi, hp1, hp2, h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
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).natDegree < i * p.natDegree + p.natDegree
have h1 : (p ^ i).natDegree < i * p.natDegree
Tactic: have h1 : (p ^ i).natDegree < i * p.natDegree := by
          refine lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_
          rw [← h, hp1] at hi
          exact leadingCoeff_eq_zero.mp hi
-- 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
h1 : (p ^ i).natDegree < i * p.natDegree
⊢ (p ^ i * p).natDegree < i * p.natDegree + p.natDegree
have i₁ : (p ^ i).natDegree + p.natDegree < i * p.natDegree + p.natDegree
Tactic: calc
          (p ^ i * p).natDegree ≤ (p ^ i).natDegree + p.natDegree := natDegree_mul_le
          _ < i * p.natDegree + p.natDegree := by gcongr
-- 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 neg : (p ^ i * p).coeff ((p ^ i).natDegree + p.natDegree) = (p ^ i).leadingCoeff * p.leadingCoeff
Tactic: rw [← natDegree_pow' hp1, ← leadingCoeff_pow' hp1]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
⊢ (p ^ n).coeff (n * p.natDegree) = p.leadingCoeff ^ n
have zero : (HPow.hPow (β := ℕ) p 0).coeff (0 * p.natDegree) = HPow.hPow (β := ℕ) p.leadingCoeff 0
Tactic: induction n with
  | zero => simp
  | succ i hi =>
    rw [pow_succ, pow_succ, Nat.succ_mul]
    by_cases hp1 : p.leadingCoeff ^ i = 0
    · rw [hp1, zero_mul]
      by_cases hp2 : p ^ i = 0
      · rw [hp2, zero_mul, coeff_zero]
      · apply coeff_eq_zero_of_natDegree_lt
        have h1 : (p ^ i).natDegree < i * p.natDegree := by
          refine lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_
          rw [← h, hp1] at hi
          exact leadingCoeff_eq_zero.mp hi
        calc
          (p ^ i * p).natDegree ≤ (p ^ i).natDegree + p.natDegree := natDegree_mul_le
          _ < i * p.natDegree + p.natDegree := by gcongr
    · rw [← natDegree_pow' hp1, ← leadingCoeff_pow' hp1]
      exact coeff_mul_degree_add_degree _ _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
zero : (HPow.hPow (β := ℕ) p 0).coeff (0 * p.natDegree) = HPow.hPow (β := ℕ) p.leadingCoeff 0
⊢ (p ^ n).coeff (n * p.natDegree) = p.leadingCoeff ^ n
have succ : ∀ (i : ℕ) (hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i),
  (p ^ (i + 1)).coeff ((i + 1) * p.natDegree) = p.leadingCoeff ^ (i + 1)
Tactic: induction n with
  | zero => simp
  | succ i hi =>
    rw [pow_succ, pow_succ, Nat.succ_mul]
    by_cases hp1 : p.leadingCoeff ^ i = 0
    · rw [hp1, zero_mul]
      by_cases hp2 : p ^ i = 0
      · rw [hp2, zero_mul, coeff_zero]
      · apply coeff_eq_zero_of_natDegree_lt
        have h1 : (p ^ i).natDegree < i * p.natDegree := by
          refine lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_
          rw [← h, hp1] at hi
          exact leadingCoeff_eq_zero.mp hi
        calc
          (p ^ i * p).natDegree ≤ (p ^ i).natDegree + p.natDegree := natDegree_mul_le
          _ < i * p.natDegree + p.natDegree := by gcongr
    · rw [← natDegree_pow' hp1, ← leadingCoeff_pow' hp1]
      exact coeff_mul_degree_add_degree _ _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
⊢ (f * g).coeff (df + dg) = f.coeff df * g.coeff dg
have h : (df, dg) ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
Tactic: rw [coeff_mul, Finset.sum_eq_single_of_mem (df, dg)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
h : (df, dg) ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
⊢ (f * g).coeff (df + dg) = f.coeff df * g.coeff dg
have h₀ : ∀ b ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg), b ≠ (df, dg) → f.coeff b.1 * g.coeff b.2 = 0
Tactic: rw [coeff_mul, Finset.sum_eq_single_of_mem (df, dg)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
⊢ (df, dg) ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
have h : (df, dg).1 + (df, dg).2 = df + dg
Tactic: rw [mem_antidiagonal]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
have h₀ : ∀ (h : df < df'), f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
Tactic: obtain h | hdf' := lt_or_ge df df'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
h₀ : ∀ (h : df < df'), f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
have h₁ : ∀ (hdf' : df' ≤ df), f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
Tactic: obtain h | hdf' := lt_or_ge df df'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
h : df < df'
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
have h₀ : 0 * g.coeff (df', dg').2 = 0
Tactic: rw [coeff_eq_zero_of_natDegree_lt (hdf.trans_lt h), zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
h : df < df'
h₀ : 0 * g.coeff (df', dg').2 = 0
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
have h₁ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [coeff_eq_zero_of_natDegree_lt (hdf.trans_lt h), zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
have h₀ : ∀ (h : dg < dg'), f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
Tactic: obtain h | hdg' := lt_or_ge dg dg'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
h₀ : ∀ (h : dg < dg'), f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
have h₁ : ∀ (hdg' : dg' ≤ dg), f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
Tactic: obtain h | hdg' := lt_or_ge dg dg'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
h : dg < dg'
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
have h₀ : f.coeff (df', dg').1 * 0 = 0
Tactic: rw [coeff_eq_zero_of_natDegree_lt (hdg.trans_lt h), mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
h : dg < dg'
h₀ : f.coeff (df', dg').1 * 0 = 0
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
have h₁ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [coeff_eq_zero_of_natDegree_lt (hdg.trans_lt h), mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
hdg' : dg' ≤ dg
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
have hdf₁ : f.natDegree ≤ df'
Tactic: obtain ⟨rfl, rfl⟩ :=
    (add_eq_add_iff_eq_and_eq hdf' hdg').mp (mem_antidiagonal.1 hmem)
Cleared hypotheses: df, dg, hdf, hdg, hmem, hne, hdf', hdg'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
hdg' : dg' ≤ dg
hdf₁ : f.natDegree ≤ df'
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
have hdf'₁ : df' ≤ df'
Tactic: obtain ⟨rfl, rfl⟩ :=
    (add_eq_add_iff_eq_and_eq hdf' hdg').mp (mem_antidiagonal.1 hmem)
Cleared hypotheses: df, dg, hdf, hdg, hmem, hne, hdf', hdg'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
hdg' : dg' ≤ dg
hdf₁ : f.natDegree ≤ df'
hdf'₁ : df' ≤ df'
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
have hdg₁ : g.natDegree ≤ dg'
Tactic: obtain ⟨rfl, rfl⟩ :=
    (add_eq_add_iff_eq_and_eq hdf' hdg').mp (mem_antidiagonal.1 hmem)
Cleared hypotheses: df, dg, hdf, hdg, hmem, hne, hdf', hdg'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
hdg' : dg' ≤ dg
hdf₁ : f.natDegree ≤ df'
hdf'₁ : df' ≤ df'
hdg₁ : g.natDegree ≤ dg'
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
have hdg'₁ : dg' ≤ dg'
Tactic: obtain ⟨rfl, rfl⟩ :=
    (add_eq_add_iff_eq_and_eq hdf' hdg').mp (mem_antidiagonal.1 hmem)
Cleared hypotheses: df, dg, hdf, hdg, hmem, hne, hdf', hdg'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
hdg' : dg' ≤ dg
hdf₁ : f.natDegree ≤ df'
hdf'₁ : df' ≤ df'
hdg₁ : g.natDegree ≤ dg'
hdg'₁ : dg' ≤ dg'
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
have hmem₁ : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df' + dg')
Tactic: obtain ⟨rfl, rfl⟩ :=
    (add_eq_add_iff_eq_and_eq hdf' hdg').mp (mem_antidiagonal.1 hmem)
Cleared hypotheses: df, dg, hdf, hdg, hmem, hne, hdf', hdg'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
df dg : ℕ
f g : R[X]
hdf : f.natDegree ≤ df
hdg : g.natDegree ≤ dg
df' dg' : ℕ
hmem : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df + dg)
hne : (df', dg') ≠ (df, dg)
hdf' : df' ≤ df
hdg' : dg' ≤ dg
hdf₁ : f.natDegree ≤ df'
hdf'₁ : df' ≤ df'
hdg₁ : g.natDegree ≤ dg'
hdg'₁ : dg' ≤ dg'
hmem₁ : (df', dg') ∈ @antidiagonal _ Nat.instAddMonoid _ (df' + dg')
⊢ f.coeff (df', dg').1 * g.coeff (df', dg').2 = 0
have hne₁ : (df', dg') ≠ (df', dg')
Tactic: obtain ⟨rfl, rfl⟩ :=
    (add_eq_add_iff_eq_and_eq hdf' hdg').mp (mem_antidiagonal.1 hmem)
Cleared hypotheses: df, dg, hdf, hdg, hmem, hne, hdf', hdg'
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
S : Type u_2
inst_1 : SMulZeroClass S R
a : S
p : R[X]
⊢ (a • p).degree ≤ p.degree
have refine : ∀ (m : ℕ) (hm : p.degree < (↑m : WithBot ℕ)), (a • p).coeff m = 0
Tactic: refine (degree_le_iff_coeff_zero _ _).2 fun m hm => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
S : Type u_2
inst_1 : SMulZeroClass S R
a : S
p : R[X]
m : ℕ
hm : p.degree < (↑m : WithBot ℕ)
⊢ (a • p).coeff m = 0
have hm₁ : ∀ (m_1 : ℕ), m ≤ m_1 → p.coeff m_1 = 0
Tactic: rw [degree_lt_iff_coeff_zero] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
ha : a ≠ 0
hp : IsRightRegular p.leadingCoeff
⊢ (a • p).degree = p.degree
have refine : (a • p).coeff p.natDegree ≠ 0
Tactic: refine le_antisymm (degree_smul_le a p) <| degree_le_degree ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
ha : a ≠ 0
hp : IsRightRegular p.leadingCoeff
⊢ (a • p).coeff p.natDegree ≠ 0
have rw : ¬a * p.leadingCoeff = 0
Tactic: rw [coeff_smul, coeff_natDegree, smul_eq_mul, ne_eq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
⊢ p.degree < (p * X).degree
have this : Nontrivial R
Tactic: haveI := Nontrivial.of_polynomial_ne hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
this : Nontrivial R
⊢ p.degree < (p * X).degree
have this₁ : p.leadingCoeff * leadingCoeff X ≠ 0
Tactic: have : leadingCoeff p * leadingCoeff X ≠ 0 := by simpa
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
this_1 : Nontrivial R
this : p.leadingCoeff * leadingCoeff X ≠ 0
⊢ p.degree < (p * X).degree
have rw : LT.lt (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑(p.natDegree + 1) : WithBot ℕ)
Tactic: rw [degree_mul' this, degree_eq_natDegree hp, degree_X, ← Nat.cast_one, ← Nat.cast_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
this_1 : Nontrivial R
this : p.leadingCoeff * leadingCoeff X ≠ 0
⊢ LT.lt (α := WithBot ℕ) (↑p.natDegree : WithBot ℕ) (↑(p.natDegree + 1) : WithBot ℕ)
have norm_cast : p.natDegree < p.natDegree + 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p = (C : (a : R) → R[X]) (p.coeff 0)
⊢ p.natDegree = 0
have rw : natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0)) = 0
Tactic: rw [h, natDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p = (C : (a : R) → R[X]) (p.coeff 0)
rw : natDegree.{u} (R := R) ((C : (a : R) → R[X]) (p.coeff 0)) = 0
⊢ p.natDegree = 0
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [h, natDegree_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hf : p.Monic
hfd : p.natDegree = 0
⊢ p = 1
have hf₁ : p.coeff 0 = 1
Tactic: rw [Monic.def, leadingCoeff, hfd] at hf
Cleared hypotheses: hf, hfd
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hf : p.coeff 0 = 1
hfd : p.natDegree = 0
⊢ p = 1
have rw : Eq (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (1 : R[X])
Tactic: rw [eq_C_of_natDegree_eq_zero hfd, hf, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hf : p.coeff 0 = 1
hfd : p.natDegree = 0
rw : Eq (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (1 : R[X])
⊢ p = 1
have rw₁ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 1) 1
Tactic: rw [eq_C_of_natDegree_eq_zero hfd, hf, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hf : p.coeff 0 = 1
hfd : p.natDegree = 0
rw : Eq (α := R[X]) ((C : (a : R) → R[X]) (p.coeff 0) : R[X]) (1 : R[X])
rw₁ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 1) 1
⊢ p = 1
have rw₂ : Eq.{u + 1} (α := R[X]) 1 1
Tactic: rw [eq_C_of_natDegree_eq_zero hfd, hf, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p ≠ 0
⊢ (p * X).natDegree = p.natDegree + 1
have rw : p.natDegree + natDegree.{u} (R := R) X = p.natDegree + 1
Tactic: rw [natDegree_mul' (by simpa), natDegree_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p ≠ 0
rw : p.natDegree + natDegree.{u} (R := R) X = p.natDegree + 1
⊢ (p * X).natDegree = p.natDegree + 1
have rw₁ : p.natDegree + 1 = p.natDegree + 1
Tactic: rw [natDegree_mul' (by simpa), natDegree_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p ≠ 0
⊢ (X * p).natDegree = p.natDegree + 1
have rw : (p * X).natDegree = p.natDegree + 1
Tactic: rw [commute_X p, natDegree_mul_X hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
hp : p ≠ 0
rw : (p * X).natDegree = p.natDegree + 1
⊢ (X * p).natDegree = p.natDegree + 1
have rw₁ : p.natDegree + 1 = p.natDegree + 1
Tactic: rw [commute_X p, natDegree_mul_X hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ (p * HPow.hPow (α := R[X]) X n).natDegree = p.natDegree + n
have rw : p.natDegree + (HPow.hPow (α := R[X]) X n).natDegree = p.natDegree + n
Tactic: rw [natDegree_mul' (by simpa), natDegree_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
n : ℕ
hp : p ≠ 0
rw : p.natDegree + (HPow.hPow (α := R[X]) X n).natDegree = p.natDegree + n
⊢ (p * HPow.hPow (α := R[X]) X n).natDegree = p.natDegree + n
have rw₁ : p.natDegree + n = p.natDegree + n
Tactic: rw [natDegree_mul' (by simpa), natDegree_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
n : ℕ
hp : p ≠ 0
⊢ (HPow.hPow (α := R[X]) X n * p).natDegree = p.natDegree + n
have rw : (p * HPow.hPow (α := R[X]) X n).natDegree = p.natDegree + n
Tactic: rw [commute_X_pow, natDegree_mul_X_pow n hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
p : R[X]
n : ℕ
hp : p ≠ 0
rw : (p * HPow.hPow (α := R[X]) X n).natDegree = p.natDegree + n
⊢ (HPow.hPow (α := R[X]) X n * p).natDegree = p.natDegree + n
have rw₁ : p.natDegree + n = p.natDegree + n
Tactic: rw [commute_X_pow, natDegree_mul_X_pow n hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
⊢ (HPow.hPow (α := R[X]) X n).natDegree ≤ n
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
h : Nontrivial R
⊢ (HPow.hPow (α := R[X]) X n).natDegree ≤ n
have rw : n ≤ n
Tactic: rw [Polynomial.natDegree_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
h : IsUnit.{u} (M := R[X]) X
g : R[X]
_hfg : (monomial 1 : (a : R) → R[X]) 1 * g = 1
hgf : g * (monomial 1 : (a : R) → R[X]) 1 = 1
⊢ Eq.{u + 1} (α := R) 0 1
have rw : 0 = (g * (monomial 1 : (a : R) → R[X]) 1).coeff 0
Tactic: rw [← coeff_one_zero, ← hgf]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
a : R
inst : Ring R
p : R[X]
hp : 0 < p.degree
⊢ (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).degree = p.degree
have rw : (HAdd.hAdd (β := R[X]) p (-(C : (a : R) → R[X]) a : R[X])).degree = p.degree
Tactic: rw [sub_eq_add_neg, ← C_neg, degree_add_C hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
a : R
inst : Ring R
p : R[X]
hp : 0 < p.degree
rw : (HAdd.hAdd (β := R[X]) p (-(C : (a : R) → R[X]) a : R[X])).degree = p.degree
⊢ (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).degree = p.degree
have rw₁ : (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) (-a) : R[X])).degree = p.degree
Tactic: rw [sub_eq_add_neg, ← C_neg, degree_add_C hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
a : R
inst : Ring R
p : R[X]
hp : 0 < p.degree
rw : (HAdd.hAdd (β := R[X]) p (-(C : (a : R) → R[X]) a : R[X])).degree = p.degree
rw₁ : (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) (-a) : R[X])).degree = p.degree
⊢ (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).degree = p.degree
have rw₂ : p.degree = p.degree
Tactic: rw [sub_eq_add_neg, ← C_neg, degree_add_C hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Operations (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
a : R
⊢ (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
have rw : (HAdd.hAdd (β := R[X]) p (-(C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
Tactic: rw [sub_eq_add_neg, ← C_neg, natDegree_add_C]
-- 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
⊢ (HSub.hSub (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
have rw₁ : (HAdd.hAdd (β := R[X]) p ((C : (a : R) → R[X]) (-a) : R[X])).natDegree = p.natDegree
Tactic: rw [sub_eq_add_neg, ← C_neg, natDegree_add_C]