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 : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
⊢ False
have mp : ∀ (n : ℕ) (hpn : ¬p.coeff n = 0) (hn : (↑n : WithTop ℕ) = p.support.min), False
Tactic: obtain ⟨n, hpn, hn⟩ := by simpa using min_mem_image_coe <| support_nonempty.2 hp
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
n : ℕ
hpn : ¬p.coeff n = 0
hn : (↑n : WithTop ℕ) = p.support.min
⊢ False
have hpn₁ : ¬p.coeff p.natTrailingDegree = 0
Tactic: obtain rfl := (trailingDegree_eq_iff_natTrailingDegree_eq hp).1 hn.symm
Cleared hypotheses: n, hpn, hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.coeff p.natTrailingDegree = 0
hp : ¬p = 0
n : ℕ
hpn : ¬p.coeff n = 0
hn : (↑n : WithTop ℕ) = p.support.min
hpn₁ : ¬p.coeff p.natTrailingDegree = 0
⊢ False
have hn₁ : (↑p.natTrailingDegree : WithTop ℕ) = p.support.min
Tactic: obtain rfl := (trailingDegree_eq_iff_natTrailingDegree_eq hp).1 hn.symm
Cleared hypotheses: n, hpn, hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ ¬(p = 0 ∨ p.coeff 0 ≠ 0) ↔ p ≠ 0 ∧ p.coeff 0 = 0
have rw : ¬p = 0 ∧ ¬p.coeff 0 ≠ 0 ↔ p ≠ 0 ∧ p.coeff 0 = 0
Tactic: rw [not_or, not_ne_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
rw : ¬p = 0 ∧ ¬p.coeff 0 ≠ 0 ↔ p ≠ 0 ∧ p.coeff 0 = 0
⊢ ¬(p = 0 ∨ p.coeff 0 ≠ 0) ↔ p ≠ 0 ∧ p.coeff 0 = 0
have rw₁ : ¬p = 0 ∧ p.coeff 0 = 0 ↔ p ≠ 0 ∧ p.coeff 0 = 0
Tactic: rw [not_or, not_ne_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.coeff 0 ≠ 0
⊢ p.trailingCoeff = p.coeff 0
have rw : p.coeff p.natTrailingDegree = p.coeff 0
Tactic: rw [trailingCoeff, (natTrailingDegree_eq_zero.mpr <| .inr h)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p.coeff 0 ≠ 0
rw : p.coeff p.natTrailingDegree = p.coeff 0
⊢ p.trailingCoeff = p.coeff 0
have rw₁ : p.coeff 0 = p.coeff 0
Tactic: rw [trailingCoeff, (natTrailingDegree_eq_zero.mpr <| .inr h)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.trailingDegree = (↑n : ℕ∞)
⊢ p.natTrailingDegree = n
have rw : p.trailingDegree.toNat = n
Tactic: rw [natTrailingDegree, h, ENat.toNat_coe]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.trailingDegree = (↑n : ℕ∞)
rw : p.trailingDegree.toNat = n
⊢ p.natTrailingDegree = n
have rw₁ : ENat.toNat (↑n : ℕ∞) = n
Tactic: rw [natTrailingDegree, h, ENat.toNat_coe]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : p.trailingDegree = (↑n : ℕ∞)
rw : p.trailingDegree.toNat = n
rw₁ : ENat.toNat (↑n : ℕ∞) = n
⊢ p.natTrailingDegree = n
have rw₂ : n = n
Tactic: rw [natTrailingDegree, h, ENat.toNat_coe]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
H : (↑n : ℕ∞) ≤ p.trailingDegree
⊢ n ≤ p.natTrailingDegree
have rwa : ∀ (H : LE.le (α := ℕ∞) (↑n : ℕ∞) (↑p.natTrailingDegree : ℕ∞)), n ≤ p.natTrailingDegree
Tactic: rwa [trailingDegree_eq_natTrailingDegree hp, Nat.cast_le] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
hp : p ≠ 0
H : (↑n : ℕ∞) ≤ p.trailingDegree
rwa : ∀ (H : LE.le (α := ℕ∞) (↑n : ℕ∞) (↑p.natTrailingDegree : ℕ∞)), n ≤ p.natTrailingDegree
⊢ n ≤ p.natTrailingDegree
have rwa₁ : ∀ (H : n ≤ p.natTrailingDegree), n ≤ p.natTrailingDegree
Tactic: rwa [trailingDegree_eq_natTrailingDegree hp, Nat.cast_le] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
ha : a ≠ 0
⊢ trailingDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) = (↑n : ℕ∞)
have rw : (↑n : WithTop ℕ) = (↑n : ℕ∞)
Tactic: rw [trailingDegree, support_monomial n ha, min_singleton]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
a : R
n : ℕ
inst : Semiring R
ha : a ≠ 0
⊢ natTrailingDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) = n
have rw : ENat.toNat (↑n : ℕ∞) = n
Tactic: rw [natTrailingDegree, trailingDegree_monomial ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
a : R
inst : Semiring R
n : ℕ
ha : a ≠ 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).trailingDegree = (↑n : ℕ∞)
have rw : trailingDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) = (↑n : ℕ∞)
Tactic: rw [C_mul_X_pow_eq_monomial, trailingDegree_monomial ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
a : R
inst : Semiring R
n : ℕ
ha : a ≠ 0
rw : trailingDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a) = (↑n : ℕ∞)
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).trailingDegree = (↑n : ℕ∞)
have rw₁ : Eq (α := ℕ∞) (↑n : ℕ∞) (↑n : ℕ∞)
Tactic: rw [C_mul_X_pow_eq_monomial, trailingDegree_monomial ha]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
a : R
⊢ (↑n : ℕ∞) ≤ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n)).trailingDegree
have rw : (↑n : ℕ∞) ≤ trailingDegree.{u} (R := R) ((monomial n : (a : R) → R[X]) a)
Tactic: rw [C_mul_X_pow_eq_monomial]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
⊢ p.coeff n = 0
have h₁ : (↑n : ℕ∞) < p.trailingDegree
Tactic: apply coeff_eq_zero_of_lt_trailingDegree
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
⊢ (↑n : ℕ∞) < p.trailingDegree
have pos : ∀ (hp : p = 0), (↑n : ℕ∞) < p.trailingDegree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
pos : ∀ (hp : p = 0), (↑n : ℕ∞) < p.trailingDegree
⊢ (↑n : ℕ∞) < p.trailingDegree
have neg : ∀ (hp : ¬p = 0), (↑n : ℕ∞) < p.trailingDegree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : p = 0
⊢ (↑n : ℕ∞) < p.trailingDegree
have pos : LT.lt (α := ℕ∞) (↑n : ℕ∞) ⊤
Tactic: rw [hp, trailingDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
n : ℕ
h : n < p.natTrailingDegree
hp : ¬p = 0
⊢ (↑n : ℕ∞) < p.trailingDegree
have neg : LT.lt (α := ℕ∞) (↑n : ℕ∞) (↑p.natTrailingDegree : ℕ∞)
Tactic: rw [trailingDegree_eq_natTrailingDegree hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
⊢ p.natTrailingDegree = p.support.min' ⋯
have rw : p.trailingDegree.toNat = p.support.min' sorry
Tactic: rw [natTrailingDegree, trailingDegree, ← Finset.coe_min', ENat.some_eq_coe, ENat.toNat_coe]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
rw : p.trailingDegree.toNat = p.support.min' ⋯
⊢ p.natTrailingDegree = p.support.min' ⋯
have rw₁ : ENat.toNat p.support.min = p.support.min' sorry
Tactic: rw [natTrailingDegree, trailingDegree, ← Finset.coe_min', ENat.some_eq_coe, ENat.toNat_coe]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
rw : p.trailingDegree.toNat = p.support.min' ⋯
rw₁ : ENat.toNat p.support.min = p.support.min' ⋯
⊢ p.natTrailingDegree = p.support.min' ⋯
have rw₂ : ENat.toNat (↑(p.support.min' sorry) : WithTop ℕ) = p.support.min' sorry
Tactic: rw [natTrailingDegree, trailingDegree, ← Finset.coe_min', ENat.some_eq_coe, ENat.toNat_coe]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
rw : p.trailingDegree.toNat = p.support.min' ⋯
rw₁ : ENat.toNat p.support.min = p.support.min' ⋯
rw₂ : ENat.toNat (↑(p.support.min' ⋯) : WithTop ℕ) = p.support.min' ⋯
⊢ p.natTrailingDegree = p.support.min' ⋯
have rw₃ : p.support.Nonempty
Tactic: rw [natTrailingDegree, trailingDegree, ← Finset.coe_min', ENat.some_eq_coe, ENat.toNat_coe]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
rw : p.trailingDegree.toNat = p.support.min' ⋯
rw₁ : ENat.toNat p.support.min = p.support.min' ⋯
rw₂ : ENat.toNat (↑(p.support.min' ⋯) : WithTop ℕ) = p.support.min' ⋯
rw₃ : p.support.Nonempty
⊢ p.natTrailingDegree = p.support.min' ⋯
have rw₄ : ENat.toNat (↑(p.support.min' sorry) : WithTop ℕ) = p.support.min' sorry
Tactic: rw [natTrailingDegree, trailingDegree, ← Finset.coe_min', ENat.some_eq_coe, ENat.toNat_coe]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
h : p ≠ 0
rw : p.trailingDegree.toNat = p.support.min' ⋯
rw₁ : ENat.toNat p.support.min = p.support.min' ⋯
rw₂ : ENat.toNat (↑(p.support.min' ⋯) : WithTop ℕ) = p.support.min' ⋯
rw₃ : p.support.Nonempty
rw₄ : ENat.toNat (↑(p.support.min' ⋯) : WithTop ℕ) = p.support.min' ⋯
rw₅ : p.support.Nonempty
⊢ p.natTrailingDegree = p.support.min' ⋯
have rw₆ : p.support.min' sorry = p.support.min' sorry
Tactic: rw [natTrailingDegree, trailingDegree, ← Finset.coe_min', ENat.some_eq_coe, ENat.toNat_coe]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
n : ℕ
inst : Semiring R
p : R[X]
hp : p ≠ 0
hn : ∀ m < n, p.coeff m = 0
⊢ n ≤ p.natTrailingDegree
have rw : n ≤ p.support.min' sorry
Tactic: rw [natTrailingDegree_eq_support_min' hp]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
⊢ p.natTrailingDegree ≤ p.natDegree
have pos : ∀ (hp : p = 0), p.natTrailingDegree ≤ p.natDegree
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
pos : ∀ (hp : p = 0), p.natTrailingDegree ≤ p.natDegree
⊢ p.natTrailingDegree ≤ p.natDegree
have neg : ∀ (hp : ¬p = 0), p.natTrailingDegree ≤ p.natDegree
Tactic: by_cases hp : 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 = 0
⊢ p.natTrailingDegree ≤ p.natDegree
have pos : natTrailingDegree.{u} (R := R) 0 ≤ natDegree.{u} (R := R) 0
Tactic: rw [hp, natDegree_zero, natTrailingDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p = 0
pos : natTrailingDegree.{u} (R := R) 0 ≤ natDegree.{u} (R := R) 0
⊢ p.natTrailingDegree ≤ p.natDegree
have pos₁ : natTrailingDegree.{u} (R := R) 0 ≤ 0
Tactic: rw [hp, natDegree_zero, natTrailingDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p = 0
pos : natTrailingDegree.{u} (R := R) 0 ≤ natDegree.{u} (R := R) 0
pos₁ : natTrailingDegree.{u} (R := R) 0 ≤ 0
⊢ p.natTrailingDegree ≤ p.natDegree
have pos₂ : LE.le (α := ℕ) 0 0
Tactic: rw [hp, natDegree_zero, natTrailingDegree_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ (p * HPow.hPow (α := R[X]) X n).natTrailingDegree = p.natTrailingDegree + n
have a : (p * HPow.hPow (α := R[X]) X n).natTrailingDegree ≤ p.natTrailingDegree + n
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
a : (p * HPow.hPow (α := R[X]) X n).natTrailingDegree ≤ p.natTrailingDegree + n
⊢ (p * HPow.hPow (α := R[X]) X n).natTrailingDegree = p.natTrailingDegree + n
have a₁ : p.natTrailingDegree + n ≤ (p * HPow.hPow (α := R[X]) X n).natTrailingDegree
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ (p * HPow.hPow (α := R[X]) X n).natTrailingDegree ≤ p.natTrailingDegree + n
have a : ∀ (h : (p * HPow.hPow (α := R[X]) X n).coeff (p.natTrailingDegree + n) = 0), p.trailingCoeff = 0
Tactic: refine natTrailingDegree_le_of_ne_zero fun h => mt trailingCoeff_eq_zero.mp hp ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
h : (p * HPow.hPow (α := R[X]) X n).coeff (p.natTrailingDegree + n) = 0
⊢ p.trailingCoeff = 0
have a : p.coeff p.natTrailingDegree = 0
Tactic: rwa [trailingCoeff, ← coeff_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
n : ℕ
⊢ p.natTrailingDegree + n ≤ (p * HPow.hPow (α := R[X]) X n).natTrailingDegree
have a : ∀ y ∈ (p * HPow.hPow (α := R[X]) X n).support, p.natTrailingDegree + n ≤ y
Tactic: rw [natTrailingDegree_eq_support_min' fun h => hp (mul_X_pow_eq_zero h), Finset.le_min'_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : y ∈ (p * HPow.hPow (α := R[X]) X n).support
⊢ n ≤ y
have hy₁ : (if n ≤ y then p.coeff (y - n) else 0) ≠ 0
Tactic: rw [mem_support_iff, coeff_mul_X_pow'] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : y ∈ (p * HPow.hPow (α := R[X]) X n).support
⊢ p.natTrailingDegree + n ≤ y
have key : n ≤ y
Tactic: have key : n ≤ y := by
      rw [mem_support_iff, coeff_mul_X_pow'] at hy
      exact by_contra fun h => hy (if_neg h)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (hypothesis)
Goal:
R : Type u
inst : Semiring R
p : R[X]
hp : p ≠ 0
n y : ℕ
hy : y ∈ (p * HPow.hPow (α := R[X]) X n).support
key : n ≤ y
⊢ p.natTrailingDegree + n ≤ y
have hy₁ : p.coeff (y - n) ≠ 0
Tactic: rw [mem_support_iff, coeff_mul_X_pow', if_pos key] at hy
Cleared hypotheses: hy, key
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree
have refine : ∀ (n : ℕ) (hn : n ∈ (p * q).support), p.trailingDegree + q.trailingDegree ≤ (↑n : WithTop ℕ)
Tactic: refine Finset.le_min fun n hn => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hn : n ∈ (p * q).support
⊢ p.trailingDegree + q.trailingDegree ≤ (↑n : WithTop ℕ)
have hn₁ : Ne.{u + 1} (α := R) (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, p.coeff x.1 * q.coeff x.2) 0
Tactic: rw [mem_support_iff, coeff_mul] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hn : Ne.{u + 1} (α := R) (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, p.coeff x.1 * q.coeff x.2) 0
⊢ p.trailingDegree + q.trailingDegree ≤ (↑n : WithTop ℕ)
have obtain : ∀ (i j : ℕ) (hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n) (hpq : p.coeff (i, j).1 * q.coeff (i, j).2 ≠ 0),
  p.trailingDegree + q.trailingDegree ≤ (↑n : WithTop ℕ)
Tactic: obtain ⟨⟨i, j⟩, hij, hpq⟩ := exists_ne_zero_of_sum_ne_zero hn
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hn : Ne.{u + 1} (α := R) (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, p.coeff x.1 * q.coeff x.2) 0
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
hpq : p.coeff (i, j).1 * q.coeff (i, j).2 ≠ 0
⊢ p.trailingDegree + q.trailingDegree ≤ (↑n : WithTop ℕ)
have this : (↑(i, j).1 : WithTop ℕ) + (↑(i, j).2 : WithTop ℕ) = (↑n : WithTop ℕ)
Tactic: refine
    (add_le_add (min_le (mem_support_iff.mpr (left_ne_zero_of_mul hpq)))
          (min_le (mem_support_iff.mpr (right_ne_zero_of_mul hpq)))).trans_eq ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hn : Ne.{u + 1} (α := R) (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, p.coeff x.1 * q.coeff x.2) 0
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
hpq : p.coeff (i, j).1 * q.coeff (i, j).2 ≠ 0
⊢ (↑(i, j).1 : WithTop ℕ) + (↑(i, j).2 : WithTop ℕ) = (↑n : WithTop ℕ)
have rwa : (↑((i, j).1 + (i, j).2) : WithTop ℕ) = (↑n : WithTop ℕ)
Tactic: rwa [← WithTop.coe_add, WithTop.coe_eq_coe, ← mem_antidiagonal]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
n : ℕ
hn : Ne.{u + 1} (α := R) (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, p.coeff x.1 * q.coeff x.2) 0
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
hpq : p.coeff (i, j).1 * q.coeff (i, j).2 ≠ 0
rwa : (↑((i, j).1 + (i, j).2) : WithTop ℕ) = (↑n : WithTop ℕ)
⊢ (↑(i, j).1 : WithTop ℕ) + (↑(i, j).2 : WithTop ℕ) = (↑n : WithTop ℕ)
have rwa₁ : (i, j).1 + (i, j).2 = n
Tactic: rwa [← WithTop.coe_add, WithTop.coe_eq_coe, ← mem_antidiagonal]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
h : p * q ≠ 0
hp : p = 0
⊢ p * q = 0
have rw : 0 * q = 0
Tactic: rw [hp, 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 * q ≠ 0
hp : p = 0
rw : 0 * q = 0
⊢ p * q = 0
have rw₁ : Eq.{u + 1} (α := R[X]) 0 0
Tactic: rw [hp, 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 * q ≠ 0
⊢ p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).natTrailingDegree
have hp : p ≠ 0
Tactic: have hp : p ≠ 0 := fun hp => h (by rw [hp, 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 * q ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ p * q = 0
have rw : p * 0 = 0
Tactic: rw [hq, 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 * q ≠ 0
hp : p ≠ 0
hq : q = 0
rw : p * 0 = 0
⊢ p * q = 0
have rw₁ : Eq.{u + 1} (α := R[X]) 0 0
Tactic: rw [hq, 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 * q ≠ 0
hp : p ≠ 0
⊢ p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).natTrailingDegree
have hq : q ≠ 0
Tactic: have hq : q ≠ 0 := fun hq => h (by rw [hq, 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 * q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ p.natTrailingDegree + q.natTrailingDegree ≤ (p * q).natTrailingDegree
have rw : p.trailingDegree + q.trailingDegree ≤ (p * q).trailingDegree
Tactic: rw [← WithTop.coe_le_coe, WithTop.coe_add, ← Nat.cast_withTop (natTrailingDegree p),
    ← Nat.cast_withTop (natTrailingDegree q), ← Nat.cast_withTop (natTrailingDegree (p * q)),
    ← trailingDegree_eq_natTrailingDegree hp, ← trailingDegree_eq_natTrailingDegree hq,
    ← trailingDegree_eq_natTrailingDegree h]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ (p * q).coeff (p.natTrailingDegree + q.natTrailingDegree) = p.trailingCoeff * q.trailingCoeff
have rw : ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ (p.natTrailingDegree + q.natTrailingDegree), p.coeff x.1 * q.coeff x.2 =
  p.trailingCoeff * q.trailingCoeff
Tactic: rw [coeff_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (goal)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
⊢ ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ (p.natTrailingDegree + q.natTrailingDegree), p.coeff x.1 * q.coeff x.2 =
    p.trailingCoeff * q.trailingCoeff
have fun : ∀ b ∈ @antidiagonal _ Nat.instAddMonoid _ (p.natTrailingDegree + q.natTrailingDegree),
  b ≠ (p.natTrailingDegree, q.natTrailingDegree) → p.coeff b.1 * q.coeff b.2 = 0
Tactic: refine
    Finset.sum_eq_single (p.natTrailingDegree, q.natTrailingDegree) ?_ fun h =>
      (h (mem_antidiagonal.mpr rfl)).elim
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.TrailingDegree (hypothesis)
Goal:
R : Type u
inst : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ (p.natTrailingDegree + q.natTrailingDegree)
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
have h₃ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
Tactic: rw [mem_antidiagonal] at h₁
Cleared hypotheses: h₁, h₂
-- 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)
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
have pos : ∀ (hi : i < p.natTrailingDegree), p.coeff (i, j).1 * q.coeff (i, j).2 = 0
Tactic: by_cases! hi : i < p.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)
pos : ∀ (hi : i < p.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 : ∀ (hi : p.natTrailingDegree ≤ i), p.coeff (i, j).1 * q.coeff (i, j).2 = 0
Tactic: by_cases! hi : i < p.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 : i < p.natTrailingDegree
⊢ 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_lt_natTrailingDegree hi, zero_mul]
-- 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 : i < p.natTrailingDegree
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_lt_natTrailingDegree hi, zero_mul]
-- 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
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
have pos : ∀ (hj : j < q.natTrailingDegree), p.coeff (i, j).1 * q.coeff (i, j).2 = 0
Tactic: by_cases! hj : j < q.natTrailingDegree