R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
⊢ natTrailingDegree (p * q) = natTrailingDegree p + natTrailingDegree q
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
⊢ natTrailingDegree (p * q) = natTrailingDegree p + natTrailingDegree q
have hp : p ≠ 0 := fun hp => h (by rw [hp, trailingCoeff_zero, zero_mul])
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ natTrailingDegree (p * q) = natTrailingDegree p + natTrailingDegree q
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
⊢ natTrailingDegree (p * q) = natTrailingDegree p + natTrailingDegree q
have hq : q ≠ 0 := fun hq => h (by rw [hq, trailingCoeff_zero, mul_zero])
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
aux1 : ∀ (n : ℕ), ↑n = ↑n
⊢ natTrailingDegree (p * q) = natTrailingDegree p + natTrailingDegree q
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
⊢ natTrailingDegree (p * q) = natTrailingDegree p + natTrailingDegree q
have aux1 : ∀ n, Nat.cast n = WithTop.some (n) := fun n ↦ rfl
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
aux1 : ∀ (n : ℕ), ↑n = ↑n
aux2 : ∀ (p : R[X]), ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ natTrailingDegree (p * q) = natTrailingDegree p + natTrailingDegree q
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
aux1 : ∀ (n : ℕ), ↑n = ↑n
⊢ natTrailingDegree (p * q) = natTrailingDegree p + natTrailingDegree q
have aux2 : ∀ (p : R[X]), WithTop.some (natTrailingDegree p) = Nat.cast (natTrailingDegree p) :=
  fun p ↦ rfl
case h
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
aux1 : ∀ (n : ℕ), ↑n = ↑n
aux2 : ∀ (p : R[X]), ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ trailingDegree (p * q) = ↑(natTrailingDegree p + natTrailingDegree q)
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
aux1 : ∀ (n : ℕ), ↑n = ↑n
aux2 : ∀ (p : R[X]), ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ natTrailingDegree (p * q) = natTrailingDegree p + natTrailingDegree q
apply natTrailingDegree_eq_of_trailingDegree_eq_some
no goals
case h
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q ≠ 0
aux1 : ∀ (n : ℕ), ↑n = ↑n
aux2 : ∀ (p : R[X]), ↑(natTrailingDegree p) = ↑(natTrailingDegree p)
⊢ trailingDegree (p * q) = ↑(natTrailingDegree p + natTrailingDegree q)
rw [trailingDegree_mul' h, aux1 (natTrailingDegree p + natTrailingDegree q),
  WithTop.coe_add, aux2 p, aux2 q, ← trailingDegree_eq_natTrailingDegree hp, ←
  trailingDegree_eq_natTrailingDegree hq]
no goals
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p = 0
⊢ trailingCoeff p * trailingCoeff q = 0
rw [hp, trailingCoeff_zero, zero_mul]
no goals
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : trailingCoeff p * trailingCoeff q ≠ 0
hp : p ≠ 0
hq : q = 0
⊢ trailingCoeff p * trailingCoeff q = 0
rw [hq, trailingCoeff_zero, mul_zero]