Module: Mathlib.Data.Ordmap.Invariants

Goal state before:
pp: case nil.node.nil
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
⊢ (casesOn (id nil)
        (casesOn (id (node ls nil lx lr)) (Ordnode.singleton x) fun ls_1 ll lx_1 lr_1 ↦
          casesOn (id ll)
            (casesOn lr_1 (node 2 (node ls nil lx lr) x nil) fun size l lrx r ↦
              node 3 (Ordnode.singleton lx_1) lrx (Ordnode.singleton x))
            fun lls l x_1 r ↦
            casesOn (id lr_1) (node 3 ll lx_1 (Ordnode.singleton x)) fun lrs lrl lrx lrr ↦
              if lrs < ratio * lls then node (ls_1 + 1) ll lx_1 (node (lrs + 1) lr_1 x nil)
              else node (ls_1 + 1) (node (lls + lrl.size + 1) ll lx_1 lrl) lrx (node (lrr.size + 1) lrr x nil))
        fun rs l x_1 r ↦
        casesOn (id (node ls nil lx lr)) (node (rs + 1) nil x nil) fun ls_1 ll lx_1 lr_1 ↦
          if ls_1 > delta * rs then
            casesOn (id ll) nil fun lls l x_2 r ↦
              casesOn (id lr_1) nil fun lrs lrl lrx lrr ↦
                if lrs < ratio * lls then node (ls_1 + rs + 1) ll lx_1 (node (rs + lrs + 1) lr_1 x nil)
                else
                  node (ls_1 + rs + 1) (node (lls + lrl.size + 1) ll lx_1 lrl) lrx (node (lrr.size + rs + 1) lrr x nil)
          else node (ls_1 + rs + 1) (node ls nil lx lr) x nil).dual =
    casesOn (id nil.dual)
      (casesOn (id (node ls nil lx lr).dual) (Ordnode.singleton x) fun rs rl rx rr ↦
        casesOn (id rr)
          (casesOn rl (node 2 nil x (node ls nil lx lr).dual) fun size l rlx r ↦
            node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx))
          fun rrs l x_1 r ↦
          casesOn (id rl) (node 3 (Ordnode.singleton x) rx rr) fun rls rll rlx rlr ↦
            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_1 l x_1 r ↦
      casesOn (id (node ls nil lx lr).dual) (node (ls_1 + 1) nil.dual x nil) fun rs rl rx rr ↦
        if rs > delta * ls_1 then
          casesOn (id rr) nil fun rrs l x_2 r ↦
            casesOn (id rl) nil fun rls rll rlx rlr ↦
              if rls < ratio * rrs then node (ls_1 + rs + 1) (node (ls_1 + rls + 1) nil.dual x rl) rx rr
              else
                node (ls_1 + rs + 1) (node (ls_1 + rll.size + 1) nil.dual x rll) rlx
                  (node (rlr.size + rrs + 1) rlr rx rr)
        else node (ls_1 + rs + 1) nil.dual x (node ls nil lx lr).dual

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

Goal state after:
case nil.node.nil.nil
α : Type u_1
x : α
ls : ℕ
lx : α
⊢ (casesOn (id nil)
        (casesOn (id (node ls nil lx nil)) (Ordnode.singleton x) fun ls_1 ll lx_1 lr ↦
          casesOn (id ll)
            (casesOn lr (node 2 (node ls nil lx nil) x nil) fun size l lrx r ↦
              node 3 (Ordnode.singleton lx_1) lrx (Ordnode.singleton x))
            fun lls l x_1 r ↦
            casesOn (id lr) (node 3 ll lx_1 (Ordnode.singleton x)) fun lrs lrl lrx lrr ↦
              if lrs < ratio * lls then node (ls_1 + 1) ll lx_1 (node (lrs + 1) lr x nil)
              else node (ls_1 + 1) (node (lls + lrl.size + 1) ll lx_1 lrl) lrx (node (lrr.size + 1) lrr x nil))
        fun rs l x_1 r ↦
        casesOn (id (node ls nil lx nil)) (node (rs + 1) nil x nil) fun ls_1 ll lx_1 lr ↦
          if ls_1 > delta * rs then
            casesOn (id ll) nil fun lls l x_2 r ↦
              casesOn (id lr) nil fun lrs lrl lrx lrr ↦
                if lrs < ratio * lls then node (ls_1 + rs + 1) ll lx_1 (node (rs + lrs + 1) lr x nil)
                else
                  node (ls_1 + rs + 1) (node (lls + lrl.size + 1) ll lx_1 lrl) lrx (node (lrr.size + rs + 1) lrr x nil)
          else node (ls_1 + rs + 1) (node ls nil lx nil) x nil).dual =
    casesOn (id nil.dual)
      (casesOn (id (node ls nil lx nil).dual) (Ordnode.singleton x) fun rs rl rx rr ↦
        casesOn (id rr)
          (casesOn rl (node 2 nil x (node ls nil lx nil).dual) fun size l rlx r ↦
            node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx))
          fun rrs l x_1 r ↦
          casesOn (id rl) (node 3 (Ordnode.singleton x) rx rr) fun rls rll rlx rlr ↦
            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_1 l x_1 r ↦
      casesOn (id (node ls nil lx nil).dual) (node (ls_1 + 1) nil.dual x nil) fun rs rl rx rr ↦
        if rs > delta * ls_1 then
          casesOn (id rr) nil fun rrs l x_2 r ↦
            casesOn (id rl) nil fun rls rll rlx rlr ↦
              if rls < ratio * rrs then node (ls_1 + rs + 1) (node (ls_1 + rls + 1) nil.dual x rl) rx rr
              else
                node (ls_1 + rs + 1) (node (ls_1 + rll.size + 1) nil.dual x rll) rlx
                  (node (rlr.size + rrs + 1) rlr rx rr)
        else node (ls_1 + rs + 1) nil.dual x (node ls nil lx nil).dual

case nil.node.nil.node
α : Type u_1
x : α
ls : ℕ
lx : α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ (casesOn (id nil)
        (casesOn (id (node ls nil lx (node lrs lrl lrx lrr))) (Ordnode.singleton x) fun ls_1 ll lx_1 lr ↦
          casesOn (id ll)
            (casesOn lr (node 2 (node ls nil lx (node lrs lrl lrx lrr)) x nil) fun size l lrx r ↦
              node 3 (Ordnode.singleton lx_1) lrx (Ordnode.singleton x))
            fun lls l x_1 r ↦
            casesOn (id lr) (node 3 ll lx_1 (Ordnode.singleton x)) fun lrs lrl lrx lrr ↦
              if lrs < ratio * lls then node (ls_1 + 1) ll lx_1 (node (lrs + 1) lr x nil)
              else node (ls_1 + 1) (node (lls + lrl.size + 1) ll lx_1 lrl) lrx (node (lrr.size + 1) lrr x nil))
        fun rs l x_1 r ↦
        casesOn (id (node ls nil lx (node lrs lrl lrx lrr))) (node (rs + 1) nil x nil) fun ls_1 ll lx_1 lr ↦
          if ls_1 > delta * rs then
            casesOn (id ll) nil fun lls l x_2 r ↦
              casesOn (id lr) nil fun lrs lrl lrx lrr ↦
                if lrs < ratio * lls then node (ls_1 + rs + 1) ll lx_1 (node (rs + lrs + 1) lr x nil)
                else
                  node (ls_1 + rs + 1) (node (lls + lrl.size + 1) ll lx_1 lrl) lrx (node (lrr.size + rs + 1) lrr x nil)
          else node (ls_1 + rs + 1) (node ls nil lx (node lrs lrl lrx lrr)) x nil).dual =
    casesOn (id nil.dual)
      (casesOn (id (node ls nil lx (node lrs lrl lrx lrr)).dual) (Ordnode.singleton x) fun rs rl rx rr ↦
        casesOn (id rr)
          (casesOn rl (node 2 nil x (node ls nil lx (node lrs lrl lrx lrr)).dual) fun size l rlx r ↦
            node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx))
          fun rrs l x_1 r ↦
          casesOn (id rl) (node 3 (Ordnode.singleton x) rx rr) fun rls rll rlx rlr ↦
            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_1 l x_1 r ↦
      casesOn (id (node ls nil lx (node lrs lrl lrx lrr)).dual) (node (ls_1 + 1) nil.dual x nil) fun rs rl rx rr ↦
        if rs > delta * ls_1 then
          casesOn (id rr) nil fun rrs l x_2 r ↦
            casesOn (id rl) nil fun rls rll rlx rlr ↦
              if rls < ratio * rrs then node (ls_1 + rs + 1) (node (ls_1 + rls + 1) nil.dual x rl) rx rr
              else
                node (ls_1 + rs + 1) (node (ls_1 + rll.size + 1) nil.dual x rll) rlx
                  (node (rlr.size + rrs + 1) rlr rx rr)
        else node (ls_1 + rs + 1) nil.dual x (node ls nil lx (node lrs lrl lrx lrr)).dual