-- Module: Mathlib.Data.Ordmap.Invariants
Goal:
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
h : ls > delta * rs
pos :
  Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (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) nil lx (node (rs + size_1 + 1) lr x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) nil lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            lr)
        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 : Ordnode α) (x_2 : α) (r l_ih r_ih : Ordnode α) ↦
            if size_1 < ratio * size then
              node (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x lr.dual) lx (dual nil)
            else
              node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
                (node (r.size + size + 1) r lx (dual nil)))
          lr.dual)
      (dual nil))
pos₁ :
  ∀ (lls : ℕ) (lll : Ordnode α) (llx : α) (llr : Ordnode α),
    Eq.{u_1 + 1} (α := Ordnode α)
      (dual
        (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 (rs + size_1 + 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)))
      (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 (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x lr.dual) lx
                  (node lls lll llx llr).dual
              else
                node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
                  (node (r.size + size + 1) r lx (node lls lll llx llr).dual))
            lr.dual)
        (node lls lll llx llr).dual)
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (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) ll lx (node (rs + size_1 + 1) lr x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            lr)
        ll))
    (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 (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x lr.dual) lx ll.dual
            else
              node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
                (node (r.size + size + 1) r lx ll.dual))
          lr.dual)
      ll.dual)

Tactic:
obtain - | ⟨lls, lll, llx, llr⟩ := ll