case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
⊢ p = 1

case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : p = 1
⊢ natDegree p = 0
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
⊢ natDegree p = 0 ↔ p = 1
constructor <;> intro h
case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : p = 1
⊢ natDegree p = 0

case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
⊢ p = 1
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
⊢ p = 1

case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : p = 1
⊢ natDegree p = 0
swap
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
this : p = ↑C (coeff p 0)
⊢ p = 1
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
⊢ p = 1
have : p = C (p.coeff 0) := by
  rw [← Polynomial.degree_le_zero_iff]
  rwa [Polynomial.natDegree_eq_zero_iff_degree_le_zero] at h
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
this : p = ↑C (coeff p 0)
⊢ ↑C (coeff p 0) = 1
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
this : p = ↑C (coeff p 0)
⊢ p = 1
rw [this]
no goals
case mp
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
this : p = ↑C (coeff p 0)
⊢ ↑C (coeff p 0) = 1
rw [← h, ← Polynomial.leadingCoeff, Monic.def.1 hp, C_1]
case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : p = 1
⊢ natDegree 1 = 0
case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : p = 1
⊢ natDegree p = 0
rw [h]
no goals
case mpr
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : p = 1
⊢ natDegree 1 = 0
exact natDegree_one
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
⊢ degree p ≤ 0
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
⊢ p = ↑C (coeff p 0)
rw [← Polynomial.degree_le_zero_iff]
no goals
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p q r : R[X]
hp : Monic p
h : natDegree p = 0
⊢ degree p ≤ 0
rwa [Polynomial.natDegree_eq_zero_iff_degree_le_zero] at h