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