awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : p.natTrailingDegree ≤ i
pos : ∀ (hj : j < q.natTrailingDegree), p.coeff (i, j).1 * q.coeff (i, j).2 = 0
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
have neg : ∀ (hj : q.natTrailingDegree ≤ j), p.coeff (i, j).1 * q.coeff (i, j).2 = 0
Tactic: by_cases! hj : j < q.natTrailingDegree
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : p.natTrailingDegree ≤ i
hj : j < q.natTrailingDegree
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
have pos : p.coeff (i, j).1 * 0 = 0
Tactic: rw [coeff_eq_zero_of_lt_natTrailingDegree hj, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : p.natTrailingDegree ≤ i
hj : j < q.natTrailingDegree
pos : p.coeff (i, j).1 * 0 = 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_lt_natTrailingDegree hj, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : p.natTrailingDegree ≤ i
hj : q.natTrailingDegree ≤ j
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
have neg : (p.natTrailingDegree, q.natTrailingDegree).1 = (i, j).1 ∧ (p.natTrailingDegree, q.natTrailingDegree).2 = (i, j).2
Tactic: refine (h₂ (Prod.ext_iff.mpr ?_).symm).elim
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p = 0
⊢ p.trailingCoeff * q.trailingCoeff = 0
have rw : trailingCoeff 0 * q.trailingCoeff = 0
Tactic: rw [hp, trailingCoeff_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p = 0
rw : trailingCoeff 0 * q.trailingCoeff = 0
⊢ p.trailingCoeff * q.trailingCoeff = 0
have rw₁ : 0 * q.trailingCoeff = 0
Tactic: rw [hp, trailingCoeff_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p = 0
rw : trailingCoeff 0 * q.trailingCoeff = 0
rw₁ : 0 * q.trailingCoeff = 0
⊢ p.trailingCoeff * q.trailingCoeff = 0
have rw₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [hp, trailingCoeff_zero, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
have hp : p ≠ 0
Tactic: have hp : p ≠ 0 := fun hp => h (by rw [hp, trailingCoeff_zero, zero_mul])
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ p.trailingCoeff * q.trailingCoeff = 0
have rw : p.trailingCoeff * trailingCoeff 0 = 0
Tactic: rw [hq, trailingCoeff_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q = 0
rw : p.trailingCoeff * trailingCoeff 0 = 0
⊢ p.trailingCoeff * q.trailingCoeff = 0
have rw₁ : p.trailingCoeff * 0 = 0
Tactic: rw [hq, trailingCoeff_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q = 0
rw : p.trailingCoeff * trailingCoeff 0 = 0
rw₁ : p.trailingCoeff * 0 = 0
⊢ p.trailingCoeff * q.trailingCoeff = 0
have rw₂ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [hq, trailingCoeff_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
have hq : q ≠ 0
Tactic: have hq : q ≠ 0 := fun hq => h (by rw [hq, trailingCoeff_zero, mul_zero])
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree = p.trailingDegree + q.trailingDegree
have refine : (p * q).trailingDegree ≤ p.trailingDegree + q.trailingDegree
Tactic: refine le_antisymm ?_ le_trailingDegree_mul
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree ≤ p.trailingDegree + q.trailingDegree
have rw : (p * q).trailingDegree ≤ (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)
Tactic: rw [trailingDegree_eq_natTrailingDegree hp, trailingDegree_eq_natTrailingDegree hq, ←
    ENat.coe_add]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree ≤ (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)
have h₁ : (p * q).coeff (p.natTrailingDegree + q.natTrailingDegree) ≠ 0
Tactic: apply trailingDegree_le_of_ne_zero
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
⊢ (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree
have hp : p ≠ 0
Tactic: have hp : p ≠ 0 := fun hp => h (by rw [hp, trailingCoeff_zero, zero_mul])
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
⊢ (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree
have hq : q ≠ 0
Tactic: have hq : q ≠ 0 := fun hq => h (by rw [hq, trailingCoeff_zero, mul_zero])
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree
have h₁ : (p * q).trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)
Tactic: apply natTrailingDegree_eq_of_trailingDegree_eq_some
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)
have h₁ : p.trailingDegree + q.trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)
Tactic: rw [trailingDegree_mul' h, Nat.cast_withTop (natTrailingDegree p + natTrailingDegree q),
    WithTop.coe_add, ← Nat.cast_withTop, ← Nat.cast_withTop,
    ← trailingDegree_eq_natTrailingDegree hp, ← trailingDegree_eq_natTrailingDegree hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
h₁ : p.trailingDegree + q.trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)
⊢ (p * q).trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)
have h₂ : p.trailingDegree + q.trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : WithTop ℕ)
Tactic: rw [trailingDegree_mul' h, Nat.cast_withTop (natTrailingDegree p + natTrailingDegree q),
    WithTop.coe_add, ← Nat.cast_withTop, ← Nat.cast_withTop,
    ← trailingDegree_eq_natTrailingDegree hp, ← trailingDegree_eq_natTrailingDegree hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
h₁ : p.trailingDegree + q.trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)
h₂ : p.trailingDegree + q.trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : WithTop ℕ)
⊢ (p * q).trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)
have h₃ : p.trailingDegree + q.trailingDegree = (↑p.natTrailingDegree : WithTop ℕ) + (↑q.natTrailingDegree : WithTop ℕ)
Tactic: rw [trailingDegree_mul' h, Nat.cast_withTop (natTrailingDegree p + natTrailingDegree q),
    WithTop.coe_add, ← Nat.cast_withTop, ← Nat.cast_withTop,
    ← trailingDegree_eq_natTrailingDegree hp, ← trailingDegree_eq_natTrailingDegree hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
h₁ : p.trailingDegree + q.trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)
h₂ : p.trailingDegree + q.trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : WithTop ℕ)
h₃ : p.trailingDegree + q.trailingDegree = (↑p.natTrailingDegree : WithTop ℕ) + (↑q.natTrailingDegree : WithTop ℕ)
⊢ (p * q).trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)
have h₄ : p.trailingDegree + q.trailingDegree = (↑p.natTrailingDegree : WithTop ℕ) + (↑q.natTrailingDegree : WithTop ℕ)
Tactic: rw [trailingDegree_mul' h, Nat.cast_withTop (natTrailingDegree p + natTrailingDegree q),
    WithTop.coe_add, ← Nat.cast_withTop, ← Nat.cast_withTop,
    ← trailingDegree_eq_natTrailingDegree hp, ← trailingDegree_eq_natTrailingDegree hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
h₁ : p.trailingDegree + q.trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)
h₂ : p.trailingDegree + q.trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : WithTop ℕ)
h₃ : p.trailingDegree + q.trailingDegree = (↑p.natTrailingDegree : WithTop ℕ) + (↑q.natTrailingDegree : WithTop ℕ)
h₄ : p.trailingDegree + q.trailingDegree = (↑p.natTrailingDegree : WithTop ℕ) + (↑q.natTrailingDegree : WithTop ℕ)
⊢ (p * q).trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)
have h₅ : p.trailingDegree + q.trailingDegree =
  HAdd.hAdd (α := WithTop ℕ) (↑p.natTrailingDegree : WithTop ℕ) (↑q.natTrailingDegree : WithTop ℕ)
Tactic: rw [trailingDegree_mul' h, Nat.cast_withTop (natTrailingDegree p + natTrailingDegree q),
    WithTop.coe_add, ← Nat.cast_withTop, ← Nat.cast_withTop,
    ← trailingDegree_eq_natTrailingDegree hp, ← trailingDegree_eq_natTrailingDegree hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
h₁ : p.trailingDegree + q.trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)
h₂ : p.trailingDegree + q.trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : WithTop ℕ)
h₃ : p.trailingDegree + q.trailingDegree = (↑p.natTrailingDegree : WithTop ℕ) + (↑q.natTrailingDegree : WithTop ℕ)
h₄ : p.trailingDegree + q.trailingDegree = (↑p.natTrailingDegree : WithTop ℕ) + (↑q.natTrailingDegree : WithTop ℕ)
h₅ :
  p.trailingDegree + q.trailingDegree =
    HAdd.hAdd (α := WithTop ℕ) (↑p.natTrailingDegree : WithTop ℕ) (↑q.natTrailingDegree : WithTop ℕ)
⊢ (p * q).trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)
have h₆ : p.trailingDegree + q.trailingDegree = p.trailingDegree + (↑q.natTrailingDegree : WithTop ℕ)
Tactic: rw [trailingDegree_mul' h, Nat.cast_withTop (natTrailingDegree p + natTrailingDegree q),
    WithTop.coe_add, ← Nat.cast_withTop, ← Nat.cast_withTop,
    ← trailingDegree_eq_natTrailingDegree hp, ← trailingDegree_eq_natTrailingDegree hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p.trailingCoeff * q.trailingCoeff ≠ 0
hp : p ≠ 0
hq : q ≠ 0
h₁ : p.trailingDegree + q.trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)
h₂ : p.trailingDegree + q.trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : WithTop ℕ)
h₃ : p.trailingDegree + q.trailingDegree = (↑p.natTrailingDegree : WithTop ℕ) + (↑q.natTrailingDegree : WithTop ℕ)
h₄ : p.trailingDegree + q.trailingDegree = (↑p.natTrailingDegree : WithTop ℕ) + (↑q.natTrailingDegree : WithTop ℕ)
h₅ :
  p.trailingDegree + q.trailingDegree =
    HAdd.hAdd (α := WithTop ℕ) (↑p.natTrailingDegree : WithTop ℕ) (↑q.natTrailingDegree : WithTop ℕ)
h₆ : p.trailingDegree + q.trailingDegree = p.trailingDegree + (↑q.natTrailingDegree : WithTop ℕ)
⊢ (p * q).trailingDegree = (↑(p.natTrailingDegree + q.natTrailingDegree) : ℕ∞)
have h₇ : p.trailingDegree + q.trailingDegree = p.trailingDegree + q.trailingDegree
Tactic: rw [trailingDegree_mul' h, Nat.cast_withTop (natTrailingDegree p + natTrailingDegree q),
    WithTop.coe_add, ← Nat.cast_withTop, ← Nat.cast_withTop,
    ← trailingDegree_eq_natTrailingDegree hp, ← trailingDegree_eq_natTrailingDegree hq]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
⊢ (HPow.hPow (α := R[X]) X n).trailingDegree = (↑n : ℕ∞)
have rw : trailingDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) 1) = (↑n : ℕ∞)
Tactic: rw [X_pow_eq_monomial, trailingDegree_monomial one_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
rw : trailingDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) 1) = (↑n : ℕ∞)
⊢ (HPow.hPow (α := R[X]) X n).trailingDegree = (↑n : ℕ∞)
have rw₁ : Eq (α := ℕ∞) (↑n : ℕ∞) (↑n : ℕ∞)
Tactic: rw [X_pow_eq_monomial, trailingDegree_monomial one_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
⊢ (HPow.hPow (α := R[X]) X n).natTrailingDegree = n
have rw : natTrailingDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) 1) = n
Tactic: rw [X_pow_eq_monomial, natTrailingDegree_monomial one_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
n : ℕ
rw : natTrailingDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) 1) = n
⊢ (HPow.hPow (α := R[X]) X n).natTrailingDegree = n
have rw₁ : n = n
Tactic: rw [X_pow_eq_monomial, natTrailingDegree_monomial one_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Ring R
p : R[X]
⊢ (-p).support.min = p.support.min
have rw : p.support.min = p.support.min
Tactic: rw [support_neg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.coeff 0 = 0
⊢ p.nextCoeffUp = p.coeff (p.natTrailingDegree + 1)
have inl : ∀ (hp : Eq.{u + 1} (α := R) (coeff 0 0) 0),
  Eq.{u + 1} (α := R) (nextCoeffUp 0) (coeff 0 (natTrailingDegree.{u} (R := R) 0 + 1))
Tactic: obtain rfl | hp₀ := eq_or_ne p 0
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.coeff 0 = 0
inl :
  ∀ (hp : Eq.{u + 1} (α := R) (coeff 0 0) 0),
    Eq.{u + 1} (α := R) (nextCoeffUp 0) (coeff 0 (natTrailingDegree.{u} (R := R) 0 + 1))
⊢ p.nextCoeffUp = p.coeff (p.natTrailingDegree + 1)
have inr : ∀ (hp₀ : p ≠ 0), p.nextCoeffUp = p.coeff (p.natTrailingDegree + 1)
Tactic: obtain rfl | hp₀ := eq_or_ne p 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.coeff 0 = 0
hp₀ : p ≠ 0
⊢ p.nextCoeffUp = p.coeff (p.natTrailingDegree + 1)
have inr : (if p.natTrailingDegree = 0 then 0 else p.coeff (p.natTrailingDegree + 1)) = p.coeff (p.natTrailingDegree + 1)
Tactic: rw [nextCoeffUp, if_neg (natTrailingDegree_ne_zero.2 ⟨hp₀, hp⟩)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p.coeff 0 = 0
hp₀ : p ≠ 0
inr : (if p.natTrailingDegree = 0 then 0 else p.coeff (p.natTrailingDegree + 1)) = p.coeff (p.natTrailingDegree + 1)
⊢ p.nextCoeffUp = p.coeff (p.natTrailingDegree + 1)
have inr₁ : p.coeff (p.natTrailingDegree + 1) = p.coeff (p.natTrailingDegree + 1)
Tactic: rw [nextCoeffUp, if_neg (natTrailingDegree_ne_zero.2 ⟨hp₀, hp⟩)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
⊢ p = HPow.hPow (α := R[X]) X p.natDegree ↔ p.natDegree ≤ p.natTrailingDegree
have refine_1 : ∀ (h : p = HPow.hPow (α := R[X]) X p.natDegree), p.natDegree ≤ p.natTrailingDegree
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
refine_1 : ∀ (h : p = HPow.hPow (α := R[X]) X p.natDegree), p.natDegree ≤ p.natTrailingDegree
⊢ p = HPow.hPow (α := R[X]) X p.natDegree ↔ p.natDegree ≤ p.natTrailingDegree
have refine_2 : ∀ (h : p.natDegree ≤ p.natTrailingDegree), p = HPow.hPow (α := R[X]) X p.natDegree
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
h : p = HPow.hPow (α := R[X]) X p.natDegree
⊢ p.natDegree ≤ p.natTrailingDegree
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
h : p = HPow.hPow (α := R[X]) X p.natDegree
h_1 : Nontrivial R
⊢ p.natDegree ≤ p.natTrailingDegree
have rw : (HPow.hPow (α := R[X]) X p.natDegree).natDegree ≤ (HPow.hPow (α := R[X]) X p.natDegree).natTrailingDegree
Tactic: rw [h, natTrailingDegree_X_pow, ← h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
h : p = HPow.hPow (α := R[X]) X p.natDegree
h_1 : Nontrivial R
rw : (HPow.hPow (α := R[X]) X p.natDegree).natDegree ≤ (HPow.hPow (α := R[X]) X p.natDegree).natTrailingDegree
⊢ p.natDegree ≤ p.natTrailingDegree
have rw₁ : (HPow.hPow (α := R[X]) X p.natDegree).natDegree ≤ p.natDegree
Tactic: rw [h, natTrailingDegree_X_pow, ← h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
h : p = HPow.hPow (α := R[X]) X p.natDegree
h_1 : Nontrivial R
rw : (HPow.hPow (α := R[X]) X p.natDegree).natDegree ≤ (HPow.hPow (α := R[X]) X p.natDegree).natTrailingDegree
rw₁ : (HPow.hPow (α := R[X]) X p.natDegree).natDegree ≤ p.natDegree
⊢ p.natDegree ≤ p.natTrailingDegree
have rw₂ : p.natDegree ≤ p.natDegree
Tactic: rw [h, natTrailingDegree_X_pow, ← h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
⊢ p = HPow.hPow (α := R[X]) X p.natDegree
have refine_2 : ∀ (n : ℕ), p.coeff n = (HPow.hPow (α := R[X]) X p.natDegree).coeff n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
⊢ p.coeff n = (HPow.hPow (α := R[X]) X p.natDegree).coeff n
have refine_2 : p.coeff n = if n = p.natDegree then 1 else 0
Tactic: rw [coeff_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
⊢ p.coeff n = if n = p.natDegree then 1 else 0
have refine_2 : ∀ (hn : n < p.natDegree), p.coeff n = if n = p.natDegree then 1 else 0
Tactic: obtain hn | rfl | hn := lt_trichotomy n p.natDegree
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
refine_2 : ∀ (hn : n < p.natDegree), p.coeff n = if n = p.natDegree then 1 else 0
⊢ p.coeff n = if n = p.natDegree then 1 else 0
have refine_2₁ : p.coeff p.natDegree = if p.natDegree = p.natDegree then 1 else 0
Tactic: obtain hn | rfl | hn := lt_trichotomy n p.natDegree
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
refine_2 : ∀ (hn : n < p.natDegree), p.coeff n = if n = p.natDegree then 1 else 0
refine_2₁ : p.coeff p.natDegree = if p.natDegree = p.natDegree then 1 else 0
⊢ p.coeff n = if n = p.natDegree then 1 else 0
have refine_2₂ : ∀ (hn : p.natDegree < n), p.coeff n = if n = p.natDegree then 1 else 0
Tactic: obtain hn | rfl | hn := lt_trichotomy n p.natDegree
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
hn : n < p.natDegree
⊢ p.coeff n = if n = p.natDegree then 1 else 0
have refine_2 : p.coeff n = 0
Tactic: rw [if_neg hn.ne, coeff_eq_zero_of_lt_natTrailingDegree (hn.trans_le h)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
hn : n < p.natDegree
refine_2 : p.coeff n = 0
⊢ p.coeff n = if n = p.natDegree then 1 else 0
have refine_2₁ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [if_neg hn.ne, coeff_eq_zero_of_lt_natTrailingDegree (hn.trans_le h)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
hn : p.natDegree < n
⊢ p.coeff n = if n = p.natDegree then 1 else 0
have refine_2 : p.coeff n = 0
Tactic: rw [if_neg hn.ne', coeff_eq_zero_of_natDegree_lt hn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
n : ℕ
hn : p.natDegree < n
refine_2 : p.coeff n = 0
⊢ p.coeff n = if n = p.natDegree then 1 else 0
have refine_2₁ : Eq.{u + 1} (α := R) 0 0
Tactic: rw [if_neg hn.ne', coeff_eq_zero_of_natDegree_lt hn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Units (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
h : IsUnit p
⊢ p.natDegree = 0
have a : Nontrivial R
Tactic: nontriviality R
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Units (goal)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
h : IsUnit p
h_1 : Nontrivial R
⊢ p.natDegree = 0
have obtain : ∀ (q : R[X]) (hq : p * q = 1), p.natDegree = 0
Tactic: obtain ⟨q, hq⟩ := h.exists_right_inv
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Units (hypothesis)
Goal:
R : Type u
inst : Semiring R
inst_1 : NoZeroDivisors R
p : R[X]
h : IsUnit p
h_1 : Nontrivial R
q : R[X]
hq : p * q = 1
⊢ p.natDegree = 0
have this : (p * q).natDegree = p.natDegree + q.natDegree
Tactic: have := natDegree_mul (left_ne_zero_of_mul_eq_one hq) (right_ne_zero_of_mul_eq_one hq)