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

case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ p * q ≠ 0
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
⊢ p * q ≠ 0
by_cases h : p = 1
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬q = 0 ∧ ¬degree p = ⊥
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ p * q ≠ 0
rw [Ne.def, ← degree_eq_bot, hp.degree_mul_comm, hp.degree_mul, WithBot.add_eq_bot, not_or,
  degree_eq_bot]
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬degree p = ⊥
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬q = 0 ∧ ¬degree p = ⊥
refine' ⟨hq, _⟩
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : 0 < degree p
⊢ ¬degree p = ⊥
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : ¬p = 1
⊢ ¬degree p = ⊥
rw [← hp.degree_le_zero_iff_eq_one, not_le] at h
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : 0 < degree p
⊢ ⊥ < 0
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : 0 < degree p
⊢ ¬degree p = ⊥
refine' (lt_trans _ h).ne'
no goals
case neg
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : 0 < degree p
⊢ ⊥ < 0
simp
no goals
case pos
R : Type u
S : Type v
a b : R
m n : ℕ
ι : Type y
inst✝ : Semiring R
p : R[X]
hp : Monic p
q : R[X]
hq : q ≠ 0
h : p = 1
⊢ p * q ≠ 0
simpa [h]