-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : (node ls (node lls lll llx llr) lx lr).Balanced
sl : (node ls (node lls lll llx llr) lx lr).Sized
ld : delta ≤ (node lls lll llx llr).size + lr.size
pos :
  ∀ (hl : (node ls (node lls lll llx llr) lx nil).Balanced) (sl : (node ls (node lls lll llx llr) lx nil).Sized)
    (ld : delta ≤ (node lls lll llx llr).size + size.{u_1} (α := α) nil),
    (node ls (node lls lll llx llr) lx nil).rotateR x (node rs rl 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 : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
              if size_1 < ratio * size then
                node (ls + rs + 1) (node lls lll llx llr) lx (node (size_1 + rs + 1) nil x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) (node lls lll llx llr) lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            nil)
        (node lls lll llx llr)
pos₁ :
  ∀ (lrs : ℕ) (lrl : Ordnode α) (lrx : α) (lrr : Ordnode α)
    (hl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Balanced)
    (sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized)
    (ld : delta ≤ (node lls lll llx llr).size + (node lrs lrl lrx lrr).size),
    (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).rotateR x (node rs rl 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 : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
              if size_1 < ratio * size then
                node (ls + rs + 1) (node lls lll llx llr) lx
                  (node (size_1 + rs + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) (node lls lll llx llr) lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            (node lrs lrl lrx lrr))
        (node lls lll llx llr)
⊢ (node ls (node lls lll llx llr) lx lr).rotateR x (node rs rl 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 : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
            if size_1 < ratio * size then
              node (ls + rs + 1) (node lls lll llx llr) lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + l.size + 1) (node lls lll llx llr) lx l) x_2
                (node (r.size + rs + 1) r x (node rs rl rx rr)))
          lr)
      (node lls lll llx llr)

Tactic:
obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr