R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
n : ℕ
hn : ¬¬n ∈ trailingDegree p
⊢ trailingDegree p = ↑(natTrailingDegree p)
R : Type u
S : Type v
a b : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
⊢ trailingDegree p = ↑(natTrailingDegree p)
let ⟨n, hn⟩ :=
  not_forall.1 (mt Option.eq_none_iff_forall_not_mem.2 (mt trailingDegree_eq_top.1 hp))
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬¬n ∈ trailingDegree p
hn : trailingDegree p = ↑n
⊢ trailingDegree p = ↑(natTrailingDegree p)
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
n : ℕ
hn : ¬¬n ∈ trailingDegree p
⊢ trailingDegree p = ↑(natTrailingDegree p)
have hn : trailingDegree p = n := Classical.not_not.1 hn
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬¬n ∈ trailingDegree p
hn : trailingDegree p = ↑n
⊢ ↑n = ↑(Option.getD (↑n) 0)
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬¬n ∈ trailingDegree p
hn : trailingDegree p = ↑n
⊢ trailingDegree p = ↑(natTrailingDegree p)
rw [natTrailingDegree, hn]
no goals
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬¬n ∈ trailingDegree p
hn : trailingDegree p = ↑n
⊢ ↑n = ↑(Option.getD (↑n) 0)
rfl