-- Lean 4 proof step from Mathlib.Algebra.Polynomial.FieldDivision (goal)
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
⊢ p % q = p
have 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])) sorry).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])) sorry).2)
      else (0, p)).2 =
    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]