case pos
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
q0 : natDegree q = 0
⊢ natDegree (comp p q) = natDegree p * natDegree q

case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
q0 : ¬natDegree q = 0
⊢ natDegree (comp p q) = natDegree p * natDegree q
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
⊢ natDegree (comp p q) = natDegree p * natDegree q
by_cases q0 : q.natDegree = 0
no goals
case pos
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
q0 : natDegree q = 0
⊢ natDegree (comp p q) = natDegree p * natDegree q
rw [degree_le_zero_iff.mp (natDegree_eq_zero_iff_degree_le_zero.mp q0), comp_C, natDegree_C,
  natDegree_C, mul_zero]
case pos
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
q0 : ¬natDegree q = 0
p0 : p = 0
⊢ natDegree (comp p q) = natDegree p * natDegree q

case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
q0 : ¬natDegree q = 0
p0 : ¬p = 0
⊢ natDegree (comp p q) = natDegree p * natDegree q
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
q0 : ¬natDegree q = 0
⊢ natDegree (comp p q) = natDegree p * natDegree q
by_cases p0 : p = 0
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
q0 : ¬natDegree q = 0
p0 : ¬p = 0
⊢ coeff (comp p q) (natDegree p * natDegree q) ≠ 0
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
q0 : ¬natDegree q = 0
p0 : ¬p = 0
⊢ natDegree (comp p q) = natDegree p * natDegree q
refine' le_antisymm natDegree_comp_le (le_natDegree_of_ne_zero _)
no goals
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
q0 : ¬natDegree q = 0
p0 : ¬p = 0
⊢ coeff (comp p q) (natDegree p * natDegree q) ≠ 0
simp only [coeff_comp_degree_mul_degree q0, p0, mul_eq_zero, leadingCoeff_eq_zero, or_self_iff,
  ne_zero_of_natDegree_gt (Nat.pos_of_ne_zero q0), pow_ne_zero, Ne.def, not_false_iff]
no goals
case pos
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
q0 : ¬natDegree q = 0
p0 : p = 0
⊢ natDegree (comp p q) = natDegree p * natDegree q
simp only [p0, zero_comp, natDegree_zero, zero_mul]