-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem mod_eq_self_iff (hq0 : q ≠ 0) : p % q = p ↔ degree p < degree q :=
  ⟨fun h => h ▸ EuclideanDomain.mod_lt _ hq0, fun h => by
    classical
    have : ¬degree (q * C (leadingCoeff q)⁻¹) ≤ degree p :=
      not_le_of_gt <| by rwa [degree_mul_leadingCoeff_inv q hq0]
    rw [mod_def, modByMonic, dif_pos (monic_mul_leadingCoeff_inv hq0)]
    unfold divModByMonicAux
    dsimp
    simp only [this, false_and, if_false]⟩

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
⊢ p % q = p

Tactic:
have : ¬degree (q * C (leadingCoeff q)⁻¹) ≤ degree p :=
  not_le_of_gt <| by rwa [degree_mul_leadingCoeff_inv q hq0]

Result:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
this : ¬(q * C q.leadingCoeff⁻¹).degree ≤ p.degree
⊢ p % q = p

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
this : ¬(q * C q.leadingCoeff⁻¹).degree ≤ p.degree
⊢ p % q = p

Tactic:
rw [mod_def, modByMonic, dif_pos (monic_mul_leadingCoeff_inv hq0)]

Result:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
this : ¬(q * C q.leadingCoeff⁻¹).degree ≤ p.degree
⊢ (p.divModByMonicAux ⋯).2 = p

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
⊢ (q * C q.leadingCoeff⁻¹).degree > p.degree

Tactic:
rwa [degree_mul_leadingCoeff_inv q hq0]

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
this : ¬(q * C q.leadingCoeff⁻¹).degree ≤ p.degree
⊢ (p.divModByMonicAux ⋯).2 = p

Tactic:
unfold divModByMonicAux

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

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

Tactic:
dsimp

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

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

Tactic:
simp only [this, false_and, if_false]

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
⊢ p % q = p

Tactic:
classical
have : ¬degree (q * C (leadingCoeff q)⁻¹) ≤ degree p :=
  not_le_of_gt <| by rwa [degree_mul_leadingCoeff_inv q hq0]
rw [mod_def, modByMonic, dif_pos (monic_mul_leadingCoeff_inv hq0)]
unfold divModByMonicAux
dsimp
simp only [this, false_and, if_false]

Result:
no goals