-- Mathlib/Data/Ordmap/Ordset.lean
theorem dual_balanceL (l : Ordnode α) (x : α) (r : Ordnode α) :
    dual (balanceL l x r) = balanceR (dual r) x (dual l)

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

Tactic:
obtain - | ⟨ls, ll, lx, lr⟩ := l

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

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