-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Div (goal)
Goal:
R : Type u
inst : Ring R
p q : R[X]
this : DecidableEq R := Classical.decEq R
hq : q.Monic
h : ¬(q.degree ≤ p.degree ∧ p ≠ 0)
⊢ (if h : q.Monic then
      (if q.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 - q.natDegree)) +
              ((p -
                      q *
                        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).divModByMonicAux
                  ⋯).1,
            ((p -
                    q *
                      HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                        (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).divModByMonicAux
                ⋯).2)
        else (0, p)).2
    else p) =
    p -
      q *
        if h : q.Monic then
          (if q.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 - q.natDegree)) +
                  ((p -
                          q *
                            HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                              (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).divModByMonicAux
                      ⋯).1,
                ((p -
                        q *
                          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).divModByMonicAux
                    ⋯).2)
            else (0, p)).1
        else 0
have rw : (if q.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 - q.natDegree)) +
          ((p -
                  q *
                    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                      (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).divModByMonicAux
              sorry).1,
        ((p -
                q *
                  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                    (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).divModByMonicAux
            sorry).2)
    else (0, p)).2 =
  p -
    q *
      if h : q.Monic then
        (if q.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 - q.natDegree)) +
                ((p -
                        q *
                          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                            (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).divModByMonicAux
                    sorry).1,
              ((p -
                      q *
                        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) p.leadingCoeff : R[X])
                          (HPow.hPow (α := R[X]) X (p.natDegree - q.natDegree))).divModByMonicAux
                  sorry).2)
          else (0, p)).1
      else 0
Tactic: rw [dif_pos hq, if_neg h, dif_pos hq, if_neg h, mul_zero, sub_zero]