-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rx : α
rr : Ordnode α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
hr : (node rs (node rls rll rlx rlr) rx rr).Balanced
sr : (node rs (node rls rll rlx rlr) rx rr).Sized
rd : delta ≤ (node rls rll rlx rlr).size + rr.size
pos :
  ∀ (hr : (node rs (node rls rll rlx rlr) rx nil).Balanced) (sr : (node rs (node rls rll rlx rlr) rx nil).Sized)
    (rd : delta ≤ (node rls rll rlx rlr).size + size.{u_1} (α := α) nil),
    (node ls ll lx lr).rotateL x (node rs (node rls rll rlx rlr) rx nil) =
      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
                node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x (node rls rll rlx rlr)) rx nil
              else
                node (ls + rs + 1) (node (ls + l.size + 1) (node ls ll lx lr) x l) x_1
                  (node (r.size + size_1 + 1) r rx nil))
            nil)
        (node rls rll rlx rlr)
⊢ (node ls ll lx lr).rotateL x (node rs (node rls rll rlx rlr) rx rr) =
    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
              node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x (node rls rll rlx rlr)) rx rr
            else
              node (ls + rs + 1) (node (ls + l.size + 1) (node ls ll lx lr) x l) x_1
                (node (r.size + size_1 + 1) r rx rr))
          rr)
      (node rls rll rlx rlr)
have pos₁ : ∀ (rrs : ℕ) (rrl : Ordnode α) (rrx : α) (rrr : Ordnode α)
  (hr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Balanced)
  (sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized)
  (rd : delta ≤ (node rls rll rlx rlr).size + (node rrs rrl rrx rrr).size),
  (node ls ll lx lr).rotateL x (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    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
              node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x (node rls rll rlx rlr)) rx
                (node rrs rrl rrx rrr)
            else
              node (ls + rs + 1) (node (ls + l.size + 1) (node ls ll lx lr) x l) x_1
                (node (r.size + size_1 + 1) r rx (node rrs rrl rrx rrr)))
          (node rrs rrl rrx rrr))
      (node rls rll rlx rlr)
Tactic: obtain - | ⟨rrs, rrl, rrx, rrr⟩ := rr
Cleared hypotheses: rr, hr, sr, rd