-- 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)
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
                ⋯).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 =
    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
rw₁ :
  (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
                      ⋯).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
rw₂ :
  (0, p).2 =
    p -
      q *
        (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
⊢ (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₃ : (0, p).2 = p - q * (0, p).1
Tactic: rw [dif_pos hq, if_neg h, dif_pos hq, if_neg h, mul_zero, sub_zero]