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

Tactic:
obtain - | ⟨rs, rl, rx, rr⟩ := r