-- Mathlib/Algebra/Polynomial/Div.lean
theorem divByMonic_eq_zero_iff [Nontrivial R] (hq : Monic q) : p /ₘ q = 0 ↔ degree p < degree q :=
  ⟨fun h => by
    have := modByMonic_add_div p hq
    rwa [h, mul_zero, add_zero, modByMonic_eq_self_iff hq] at this,
  fun h => by
    classical
    have : ¬degree q ≤ degree p := not_le_of_gt h
    unfold divByMonic divModByMonicAux; dsimp; rw [dif_pos hq, if_neg (mt And.left this)]⟩

Proof state:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
⊢ p /ₘ q = 0

Tactic:
have : ¬degree q ≤ degree p := not_le_of_gt h

Result:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ p /ₘ q = 0

Proof state:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
⊢ p /ₘ q = 0

Tactic:
classical
have : ¬degree q ≤ degree p := not_le_of_gt h
unfold divByMonic divModByMonicAux; dsimp; rw [dif_pos hq, if_neg (mt And.left this)]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if h : q.Monic then
      (if q.degree ≤ p.degree ∧ ¬p = 0 then
          (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
              ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1,
            ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2)
        else (0, p)).1
    else 0) =
    0

Tactic:
rw [dif_pos hq, if_neg (mt And.left this)]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if h : q.Monic then
      (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
          let z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
          let_fun _wf := ⋯;
          let dm := (p - q * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).1
    else 0) =
    0

Tactic:
dsimp

Result:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if h : q.Monic then
      (if q.degree ≤ p.degree ∧ ¬p = 0 then
          (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree) +
              ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).1,
            ((p - q * (C p.leadingCoeff * X ^ (p.natDegree - q.natDegree))).divModByMonicAux ⋯).2)
        else (0, p)).1
    else 0) =
    0

Proof state:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ p /ₘ q = 0

Tactic:
unfold divByMonic divModByMonicAux

Result:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p.degree < q.degree
this : ¬q.degree ≤ p.degree
⊢ (if h : q.Monic then
      (if h_1 : q.degree ≤ p.degree ∧ p ≠ 0 then
          let z := C p.leadingCoeff * X ^ (p.natDegree - q.natDegree);
          let_fun _wf := ⋯;
          let dm := (p - q * z).divModByMonicAux ⋯;
          (z + dm.1, dm.2)
        else (0, p)).1
    else 0) =
    0

Proof state:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p /ₘ q = 0
⊢ p.degree < q.degree

Tactic:
have := modByMonic_add_div p hq

Result:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p /ₘ q = 0
this : p %ₘ q + q * (p /ₘ q) = p
⊢ p.degree < q.degree

Proof state:
R : Type u
inst✝¹ : Ring R
p q : R[X]
inst✝ : Nontrivial R
hq : q.Monic
h : p /ₘ q = 0
this : p %ₘ q + q * (p /ₘ q) = p
⊢ p.degree < q.degree

Tactic:
rwa [h, mul_zero, add_zero, modByMonic_eq_self_iff hq] at this

Result:
no goals