R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
n : ℕ
hn : ¬¬n ∈ degree p
⊢ degree p = ↑(natDegree p)
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
⊢ degree p = ↑(natDegree p)
let ⟨n, hn⟩ := not_forall.1 (mt Option.eq_none_iff_forall_not_mem.2 (mt degree_eq_bot.1 hp))
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬¬n ∈ degree p
hn : degree p = Option.some n
⊢ degree p = ↑(natDegree p)
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
n : ℕ
hn : ¬¬n ∈ degree p
⊢ degree p = ↑(natDegree p)
have hn : degree p = some n := Classical.not_not.1 hn
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬¬n ∈ degree p
hn : degree p = Option.some n
⊢ Option.some n = ↑(WithBot.unbot' 0 (Option.some n))
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬¬n ∈ degree p
hn : degree p = Option.some n
⊢ degree p = ↑(natDegree p)
rw [natDegree, hn]
no goals
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
hp : p ≠ 0
n : ℕ
hn✝ : ¬¬n ∈ degree p
hn : degree p = Option.some n
⊢ Option.some n = ↑(WithBot.unbot' 0 (Option.some n))
rfl