case pos
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Semiring S
p₁ p₂ : R[X]
hq : Monic q
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

case neg
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Semiring S
p₁ p₂ : R[X]
hq : ¬Monic q
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Semiring S
p₁ p₂ : R[X]
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
by_cases hq : q.Monic
case pos.inl
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Semiring S
p₁ p₂ : R[X]
hq : Monic q
hR : Subsingleton R
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q

case pos.inr
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Semiring S
p₁ p₂ : R[X]
hq : Monic q
hR : Nontrivial R
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
case pos
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Semiring S
p₁ p₂ : R[X]
hq : Monic q
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
cases' subsingleton_or_nontrivial R with hR hR
no goals
case pos.inl
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Semiring S
p₁ p₂ : R[X]
hq : Monic q
hR : Subsingleton R
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
simp only [eq_iff_true_of_subsingleton]
no goals
case pos.inr
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Semiring S
p₁ p₂ : R[X]
hq : Monic q
hR : Nontrivial R
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
exact
(div_modByMonic_unique (p₁ /ₘ q + p₂ /ₘ q) _ hq
    ⟨by
      rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div _ hq, ← add_assoc,
        add_comm (q * _), modByMonic_add_div _ hq],
      (degree_add_le _ _).trans_lt
        (max_lt (degree_modByMonic_lt _ hq) (degree_modByMonic_lt _ hq))⟩).2
no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Semiring S
p₁ p₂ : R[X]
hq : Monic q
hR : Nontrivial R
⊢ p₁ %ₘ q + p₂ %ₘ q + q * (p₁ /ₘ q + p₂ /ₘ q) = p₁ + p₂
rw [mul_add, add_left_comm, add_assoc, modByMonic_add_div _ hq, ← add_assoc,
  add_comm (q * _), modByMonic_add_div _ hq]
no goals
case neg
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
p q : R[X]
inst✝ : Semiring S
p₁ p₂ : R[X]
hq : ¬Monic q
⊢ (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
simp_rw [modByMonic_eq_of_not_monic _ hq]