R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
this : ↑n = ↑n
⊢ natTrailingDegree p ≠ n → trailingDegree p ≠ ↑n
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
⊢ natTrailingDegree p ≠ n → trailingDegree p ≠ ↑n
have : Nat.cast n = WithTop.some n := rfl
no goals
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
this : ↑n = ↑n
⊢ natTrailingDegree p ≠ n → trailingDegree p ≠ ↑n
exact mt fun h => by rw [natTrailingDegree, h, this, ←WithTop.some_eq_coe, Option.getD_coe]
no goals
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
this : ↑n = ↑n
h : trailingDegree p = ↑n
⊢ natTrailingDegree p = n
rw [natTrailingDegree, h, this, ←WithTop.some_eq_coe, Option.getD_coe]