-- Lean 4 proof step from Mathlib.Data.Ordmap.Invariants (goal)
Goal:
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
nil :
  Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id Ordnode.nil)
        (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id (node ls Ordnode.nil lx Ordnode.nil))
          (Ordnode.singleton x) fun (ls_1 : ℕ) (ll : Ordnode α) (lx_1 : α) (lr : Ordnode α) ↦
          casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id ll)
            (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) lr
              (node 2 (node ls Ordnode.nil lx Ordnode.nil) x Ordnode.nil)
              fun (size : ℕ) (l : Ordnode α) (lrx : α) (r : Ordnode α) ↦
              node 3 (Ordnode.singleton lx_1) lrx (Ordnode.singleton x))
            fun (lls : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α) ↦
            casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id lr) (node 3 ll lx_1 (Ordnode.singleton x))
              fun (lrs : ℕ) (lrl : Ordnode α) (lrx : α) (lrr : Ordnode α) ↦
              if lrs < ratio * lls then node (ls_1 + 1) ll lx_1 (node (lrs + 1) lr x Ordnode.nil)
              else node (ls_1 + 1) (node (lls + lrl.size + 1) ll lx_1 lrl) lrx (node (lrr.size + 1) lrr x Ordnode.nil))
        fun (rs : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α) ↦
        casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id (node ls Ordnode.nil lx Ordnode.nil))
          (node (rs + 1) Ordnode.nil x Ordnode.nil) fun (ls_1 : ℕ) (ll : Ordnode α) (lx_1 : α) (lr : Ordnode α) ↦
          if ls_1 > delta * rs then
            casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id ll) Ordnode.nil
              fun (lls : ℕ) (l : Ordnode α) (x_2 : α) (r : Ordnode α) ↦
              casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id lr) Ordnode.nil
                fun (lrs : ℕ) (lrl : Ordnode α) (lrx : α) (lrr : Ordnode α) ↦
                if lrs < ratio * lls then node (ls_1 + rs + 1) ll lx_1 (node (rs + lrs + 1) lr x Ordnode.nil)
                else
                  node (ls_1 + rs + 1) (node (lls + lrl.size + 1) ll lx_1 lrl) lrx
                    (node (lrr.size + rs + 1) lrr x Ordnode.nil)
          else node (ls_1 + rs + 1) (node ls Ordnode.nil lx Ordnode.nil) x Ordnode.nil))
    (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id (dual Ordnode.nil))
      (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id (node ls Ordnode.nil lx Ordnode.nil).dual)
        (Ordnode.singleton x) fun (rs : ℕ) (rl : Ordnode α) (rx : α) (rr : Ordnode α) ↦
        casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id rr)
          (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) rl
            (node 2 Ordnode.nil x (node ls Ordnode.nil lx Ordnode.nil).dual)
            fun (size : ℕ) (l : Ordnode α) (rlx : α) (r : Ordnode α) ↦
            node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx))
          fun (rrs : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α) ↦
          casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id rl) (node 3 (Ordnode.singleton x) rx rr)
            fun (rls : ℕ) (rll : Ordnode α) (rlx : α) (rlr : Ordnode α) ↦
            if rls < ratio * rrs then node (rs + 1) (node (rls + 1) Ordnode.nil x rl) rx rr
            else node (rs + 1) (node (rll.size + 1) Ordnode.nil x rll) rlx (node (rlr.size + rrs + 1) rlr rx rr))
      fun (ls_1 : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α) ↦
      casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id (node ls Ordnode.nil lx Ordnode.nil).dual)
        (node (ls_1 + 1) (dual Ordnode.nil) x Ordnode.nil) fun (rs : ℕ) (rl : Ordnode α) (rx : α) (rr : Ordnode α) ↦
        if rs > delta * ls_1 then
          casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id rr) Ordnode.nil
            fun (rrs : ℕ) (l : Ordnode α) (x_2 : α) (r : Ordnode α) ↦
            casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id rl) Ordnode.nil
              fun (rls : ℕ) (rll : Ordnode α) (rlx : α) (rlr : Ordnode α) ↦
              if rls < ratio * rrs then node (ls_1 + rs + 1) (node (ls_1 + rls + 1) (dual Ordnode.nil) x rl) rx rr
              else
                node (ls_1 + rs + 1) (node (ls_1 + rll.size + 1) (dual Ordnode.nil) x rll) rlx
                  (node (rlr.size + rrs + 1) rlr rx rr)
        else node (ls_1 + rs + 1) (dual Ordnode.nil) x (node ls Ordnode.nil lx Ordnode.nil).dual)
⊢ Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id Ordnode.nil)
        (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id (node ls Ordnode.nil lx lr)) (Ordnode.singleton x)
          fun (ls_1 : ℕ) (ll : Ordnode α) (lx_1 : α) (lr_1 : Ordnode α) ↦
          casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id ll)
            (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) lr_1 (node 2 (node ls Ordnode.nil lx lr) x Ordnode.nil)
              fun (size : ℕ) (l : Ordnode α) (lrx : α) (r : Ordnode α) ↦
              node 3 (Ordnode.singleton lx_1) lrx (Ordnode.singleton x))
            fun (lls : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α) ↦
            casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id lr_1) (node 3 ll lx_1 (Ordnode.singleton x))
              fun (lrs : ℕ) (lrl : Ordnode α) (lrx : α) (lrr : Ordnode α) ↦
              if lrs < ratio * lls then node (ls_1 + 1) ll lx_1 (node (lrs + 1) lr_1 x Ordnode.nil)
              else node (ls_1 + 1) (node (lls + lrl.size + 1) ll lx_1 lrl) lrx (node (lrr.size + 1) lrr x Ordnode.nil))
        fun (rs : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α) ↦
        casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id (node ls Ordnode.nil lx lr))
          (node (rs + 1) Ordnode.nil x Ordnode.nil) fun (ls_1 : ℕ) (ll : Ordnode α) (lx_1 : α) (lr_1 : Ordnode α) ↦
          if ls_1 > delta * rs then
            casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id ll) Ordnode.nil
              fun (lls : ℕ) (l : Ordnode α) (x_2 : α) (r : Ordnode α) ↦
              casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id lr_1) Ordnode.nil
                fun (lrs : ℕ) (lrl : Ordnode α) (lrx : α) (lrr : Ordnode α) ↦
                if lrs < ratio * lls then node (ls_1 + rs + 1) ll lx_1 (node (rs + lrs + 1) lr_1 x Ordnode.nil)
                else
                  node (ls_1 + rs + 1) (node (lls + lrl.size + 1) ll lx_1 lrl) lrx
                    (node (lrr.size + rs + 1) lrr x Ordnode.nil)
          else node (ls_1 + rs + 1) (node ls Ordnode.nil lx lr) x Ordnode.nil))
    (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id (dual Ordnode.nil))
      (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id (node ls Ordnode.nil lx lr).dual) (Ordnode.singleton x)
        fun (rs : ℕ) (rl : Ordnode α) (rx : α) (rr : Ordnode α) ↦
        casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id rr)
          (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) rl
            (node 2 Ordnode.nil x (node ls Ordnode.nil lx lr).dual)
            fun (size : ℕ) (l : Ordnode α) (rlx : α) (r : Ordnode α) ↦
            node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx))
          fun (rrs : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α) ↦
          casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id rl) (node 3 (Ordnode.singleton x) rx rr)
            fun (rls : ℕ) (rll : Ordnode α) (rlx : α) (rlr : Ordnode α) ↦
            if rls < ratio * rrs then node (rs + 1) (node (rls + 1) Ordnode.nil x rl) rx rr
            else node (rs + 1) (node (rll.size + 1) Ordnode.nil x rll) rlx (node (rlr.size + rrs + 1) rlr rx rr))
      fun (ls_1 : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α) ↦
      casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id (node ls Ordnode.nil lx lr).dual)
        (node (ls_1 + 1) (dual Ordnode.nil) x Ordnode.nil) fun (rs : ℕ) (rl : Ordnode α) (rx : α) (rr : Ordnode α) ↦
        if rs > delta * ls_1 then
          casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id rr) Ordnode.nil
            fun (rrs : ℕ) (l : Ordnode α) (x_2 : α) (r : Ordnode α) ↦
            casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id rl) Ordnode.nil
              fun (rls : ℕ) (rll : Ordnode α) (rlx : α) (rlr : Ordnode α) ↦
              if rls < ratio * rrs then node (ls_1 + rs + 1) (node (ls_1 + rls + 1) (dual Ordnode.nil) x rl) rx rr
              else
                node (ls_1 + rs + 1) (node (ls_1 + rll.size + 1) (dual Ordnode.nil) x rll) rlx
                  (node (rlr.size + rrs + 1) rlr rx rr)
        else node (ls_1 + rs + 1) (dual Ordnode.nil) x (node ls Ordnode.nil lx lr).dual)
have nil₁ : ∀ (lrs : ℕ) (lrl : Ordnode α) (lrx : α) (lrr : Ordnode α),
  Eq.{u_1 + 1} (α := Ordnode α)
    (dual
      (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id Ordnode.nil)
        (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id (node ls Ordnode.nil lx (node lrs lrl lrx lrr)))
          (Ordnode.singleton x) fun (ls_1 : ℕ) (ll : Ordnode α) (lx_1 : α) (lr : Ordnode α) ↦
          casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id ll)
            (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) lr
              (node 2 (node ls Ordnode.nil lx (node lrs lrl lrx lrr)) x Ordnode.nil)
              fun (size : ℕ) (l : Ordnode α) (lrx : α) (r : Ordnode α) ↦
              node 3 (Ordnode.singleton lx_1) lrx (Ordnode.singleton x))
            fun (lls : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α) ↦
            casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id lr) (node 3 ll lx_1 (Ordnode.singleton x))
              fun (lrs : ℕ) (lrl : Ordnode α) (lrx : α) (lrr : Ordnode α) ↦
              if lrs < ratio * lls then node (ls_1 + 1) ll lx_1 (node (lrs + 1) lr x Ordnode.nil)
              else node (ls_1 + 1) (node (lls + lrl.size + 1) ll lx_1 lrl) lrx (node (lrr.size + 1) lrr x Ordnode.nil))
        fun (rs : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α) ↦
        casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id (node ls Ordnode.nil lx (node lrs lrl lrx lrr)))
          (node (rs + 1) Ordnode.nil x Ordnode.nil) fun (ls_1 : ℕ) (ll : Ordnode α) (lx_1 : α) (lr : Ordnode α) ↦
          if ls_1 > delta * rs then
            casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id ll) Ordnode.nil
              fun (lls : ℕ) (l : Ordnode α) (x_2 : α) (r : Ordnode α) ↦
              casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id lr) Ordnode.nil
                fun (lrs : ℕ) (lrl : Ordnode α) (lrx : α) (lrr : Ordnode α) ↦
                if lrs < ratio * lls then node (ls_1 + rs + 1) ll lx_1 (node (rs + lrs + 1) lr x Ordnode.nil)
                else
                  node (ls_1 + rs + 1) (node (lls + lrl.size + 1) ll lx_1 lrl) lrx
                    (node (lrr.size + rs + 1) lrr x Ordnode.nil)
          else node (ls_1 + rs + 1) (node ls Ordnode.nil lx (node lrs lrl lrx lrr)) x Ordnode.nil))
    (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id (dual Ordnode.nil))
      (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id (node ls Ordnode.nil lx (node lrs lrl lrx lrr)).dual)
        (Ordnode.singleton x) fun (rs : ℕ) (rl : Ordnode α) (rx : α) (rr : Ordnode α) ↦
        casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id rr)
          (casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) rl
            (node 2 Ordnode.nil x (node ls Ordnode.nil lx (node lrs lrl lrx lrr)).dual)
            fun (size : ℕ) (l : Ordnode α) (rlx : α) (r : Ordnode α) ↦
            node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx))
          fun (rrs : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α) ↦
          casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id rl) (node 3 (Ordnode.singleton x) rx rr)
            fun (rls : ℕ) (rll : Ordnode α) (rlx : α) (rlr : Ordnode α) ↦
            if rls < ratio * rrs then node (rs + 1) (node (rls + 1) Ordnode.nil x rl) rx rr
            else node (rs + 1) (node (rll.size + 1) Ordnode.nil x rll) rlx (node (rlr.size + rrs + 1) rlr rx rr))
      fun (ls_1 : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α) ↦
      casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id (node ls Ordnode.nil lx (node lrs lrl lrx lrr)).dual)
        (node (ls_1 + 1) (dual Ordnode.nil) x Ordnode.nil) fun (rs : ℕ) (rl : Ordnode α) (rx : α) (rr : Ordnode α) ↦
        if rs > delta * ls_1 then
          casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id rr) Ordnode.nil
            fun (rrs : ℕ) (l : Ordnode α) (x_2 : α) (r : Ordnode α) ↦
            casesOn (motive := fun (x : Ordnode α) ↦ Ordnode α) (id rl) Ordnode.nil
              fun (rls : ℕ) (rll : Ordnode α) (rlx : α) (rlr : Ordnode α) ↦
              if rls < ratio * rrs then node (ls_1 + rs + 1) (node (ls_1 + rls + 1) (dual Ordnode.nil) x rl) rx rr
              else
                node (ls_1 + rs + 1) (node (ls_1 + rll.size + 1) (dual Ordnode.nil) x rll) rlx
                  (node (rlr.size + rrs + 1) rlr rx rr)
        else node (ls_1 + rs + 1) (dual Ordnode.nil) x (node ls Ordnode.nil lx (node lrs lrl lrx lrr)).dual)
Tactic: obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr
Cleared hypotheses: lr