-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : Field R
p q : R[X]
hq0 : q ≠ 0
h : p.degree < q.degree
have have₁ have₂ :
  ∀ (this : ¬(HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree), p % q = p
have₃ :
  ∀ (this : ¬(HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree),
    (p.divModByMonicAux (q := HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) ⋯).2 = p
have₄ :
  ∀ (this : ¬(HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree),
    (if h : (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree ∧ p ≠ 0 then
          have z :=
            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
              (HPow.hPow (α := R[X]) X
                (p.natDegree - (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).natDegree));
          have _wf := ⋯;
          have dm :=
            (p - HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) * z).divModByMonicAux (q :=
              HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) ⋯;
          (z + dm.1, dm.2)
        else (0, p)).2 =
      p
have₅ :
  ∀ (this : ¬(HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree),
    (if (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).degree ≤ p.degree ∧ ¬p = 0 then
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                (HPow.hPow (α := R[X]) X
                  (p.natDegree - (HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).natDegree)) +
              ((p -
                      HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
                        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                          (HPow.hPow (α := R[X]) X
                            (p.natDegree -
                              (HMul.hMul (β := R[X]) q
                                  ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).natDegree))).divModByMonicAux
                  (q := HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) ⋯).1,
            ((p -
                    HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X]) *
                      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                        (HPow.hPow (α := R[X]) X
                          (p.natDegree -
                            (HMul.hMul (β := R[X]) q
                                ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])).natDegree))).divModByMonicAux
                (q := HMul.hMul (β := R[X]) q ((C : (a : R) → R[X]) q.leadingCoeff⁻¹ : R[X])) ⋯).2)
        else (0, p)).2 =
      p
⊢ 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]

Premises used: if_false, false_and, dif_pos, Polynomial.divModByMonicAux, Polynomial.monic_mul_leadingCoeff_inv, Polynomial.modByMonic, Polynomial.mod_def