-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (Ordnode.node ls ll lx lr).Balanced
sl : (Ordnode.node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (Ordnode.node rs rl rx rr).Balanced
sr : (Ordnode.node rs rl rx rr).Sized
node :
  (if delta * ls < rs then (Ordnode.node ls ll lx lr).rotateL x (Ordnode.node rs rl rx rr)
    else
      if delta * rs < ls then (Ordnode.node ls ll lx lr).rotateR x (Ordnode.node rs rl rx rr)
      else (Ordnode.node ls ll lx lr).node' x (Ordnode.node rs rl rx rr)) =
    if delta * ls < rs then
      rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
        (fun (size : ℕ) (l : Ordnode α) (x_1 : α) (r l_ih r_ih : Ordnode α) ↦
          rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
            (fun (size_1 : ℕ) (l_1 : Ordnode α) (x_2 : α) (r_1 l_ih r_ih : Ordnode α) ↦
              if size < ratio * size_1 then
                Ordnode.node (ls + rs + 1) (Ordnode.node (ls + size + 1) (Ordnode.node ls ll lx lr) x rl) rx rr
              else
                Ordnode.node (ls + rs + 1) (Ordnode.node (ls + l.size + 1) (Ordnode.node ls ll lx lr) x l) x_1
                  (Ordnode.node (r.size + size_1 + 1) r rx rr))
            rr)
        rl
    else
      if delta * rs < ls then
        rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
          (fun (size : ℕ) (l : Ordnode α) (x_1 : α) (r l_ih r_ih : Ordnode α) ↦
            rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
              (fun (size_1 : ℕ) (l : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
                if size_1 < ratio * size then
                  Ordnode.node (ls + rs + 1) ll lx (Ordnode.node (size_1 + rs + 1) lr x (Ordnode.node rs rl rx rr))
                else
                  Ordnode.node (ls + rs + 1) (Ordnode.node (size + l.size + 1) ll lx l) x_2
                    (Ordnode.node (r.size + rs + 1) r x (Ordnode.node rs rl rx rr)))
              lr)
          ll
      else Ordnode.node (ls + rs + 1) (Ordnode.node ls ll lx lr) x (Ordnode.node rs rl rx rr)
⊢ (if ls + rs ≤ 1 then (Ordnode.node ls ll lx lr).node' x (Ordnode.node rs rl rx rr)
    else
      if delta * ls < rs then (Ordnode.node ls ll lx lr).rotateL x (Ordnode.node rs rl rx rr)
      else
        if delta * rs < ls then (Ordnode.node ls ll lx lr).rotateR x (Ordnode.node rs rl rx rr)
        else (Ordnode.node ls ll lx lr).node' x (Ordnode.node rs rl rx rr)) =
    if delta * ls < rs then
      rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
        (fun (size : ℕ) (l : Ordnode α) (x_1 : α) (r l_ih r_ih : Ordnode α) ↦
          rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
            (fun (size_1 : ℕ) (l_1 : Ordnode α) (x_2 : α) (r_1 l_ih r_ih : Ordnode α) ↦
              if size < ratio * size_1 then
                Ordnode.node (ls + rs + 1) (Ordnode.node (ls + size + 1) (Ordnode.node ls ll lx lr) x rl) rx rr
              else
                Ordnode.node (ls + rs + 1) (Ordnode.node (ls + l.size + 1) (Ordnode.node ls ll lx lr) x l) x_1
                  (Ordnode.node (r.size + size_1 + 1) r rx rr))
            rr)
        rl
    else
      if delta * rs < ls then
        rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
          (fun (size : ℕ) (l : Ordnode α) (x_1 : α) (r l_ih r_ih : Ordnode α) ↦
            rec (motive := fun (x : Ordnode α) ↦ Ordnode α) nil
              (fun (size_1 : ℕ) (l : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
                if size_1 < ratio * size then
                  Ordnode.node (ls + rs + 1) ll lx (Ordnode.node (size_1 + rs + 1) lr x (Ordnode.node rs rl rx rr))
                else
                  Ordnode.node (ls + rs + 1) (Ordnode.node (size + l.size + 1) ll lx l) x_2
                    (Ordnode.node (r.size + rs + 1) r x (Ordnode.node rs rl rx rr)))
              lr)
          ll
      else Ordnode.node (ls + rs + 1) (Ordnode.node ls ll lx lr) x (Ordnode.node rs rl rx rr)
have node₁ : ¬ls + rs ≤ 1
Tactic: rw [if_neg]