case mp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
⊢ trailingDegree p = ↑n → natTrailingDegree p = n

case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
⊢ natTrailingDegree p = n → trailingDegree p = ↑n
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
⊢ trailingDegree p = ↑n ↔ natTrailingDegree p = n
constructor
case mp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
H : trailingDegree p = ↑n
⊢ natTrailingDegree p = n
case mp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
⊢ trailingDegree p = ↑n → natTrailingDegree p = n
intro H
case mp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
H : trailingDegree p = ↑n
⊢ p ≠ 0
case mp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
H : trailingDegree p = ↑n
⊢ natTrailingDegree p = n
rwa [← trailingDegree_eq_iff_natTrailingDegree_eq]
case mp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : 0 < n
H : trailingDegree 0 = ↑n
⊢ False
case mp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
H : trailingDegree p = ↑n
⊢ p ≠ 0
rintro rfl
case mp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : 0 < n
H : ⊤ = ↑n
⊢ False
case mp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : 0 < n
H : trailingDegree 0 = ↑n
⊢ False
rw [trailingDegree_zero] at H
no goals
case mp
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : 0 < n
H : ⊤ = ↑n
⊢ False
exact Option.noConfusion H
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
H : natTrailingDegree p = n
⊢ trailingDegree p = ↑n
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
⊢ natTrailingDegree p = n → trailingDegree p = ↑n
intro H
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
H : natTrailingDegree p = n
⊢ p ≠ 0
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
H : natTrailingDegree p = n
⊢ trailingDegree p = ↑n
rwa [trailingDegree_eq_iff_natTrailingDegree_eq]
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : 0 < n
H : natTrailingDegree 0 = n
⊢ False
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
hn : 0 < n
H : natTrailingDegree p = n
⊢ p ≠ 0
rintro rfl
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : 0 < n
H : 0 = n
⊢ False
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : 0 < n
H : natTrailingDegree 0 = n
⊢ False
rw [natTrailingDegree_zero] at H
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : n < n
H : 0 = n
⊢ False
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : 0 < n
H : 0 = n
⊢ False
rw [H] at hn
no goals
case mpr
R : Type u
S : Type v
a b : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
hn : n < n
H : 0 = n
⊢ False
exact lt_irrefl _ hn