-- 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 pos.node.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
lx : α
h✝ : ls > delta * rs
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ (rec nil
        (fun size l x_1 r l_ih r_ih =>
          rec nil
            (fun size_1 l x_2 r l_ih r_ih =>
              if size_1 < ratio * size then
                node (ls + rs + 1) (node lls lll llx llr) lx
                  (node (rs + size_1 + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))
              else
                node (ls + rs + 1) (node (size + l.size + 1) (node lls lll llx llr) lx l) x_2
                  (node (r.size + rs + 1) r x (node rs rl rx rr)))
            (node lrs lrl lrx lrr))
        (node lls lll llx llr)).dual =
    rec nil
      (fun size l x_1 r l_ih r_ih =>
        rec nil
          (fun size_1 l x_2 r l_ih r_ih =>
            if size_1 < ratio * size then
              node (rs + ls + 1) (node (rs + size_1 + 1) (node rs rr.dual rx rl.dual) x (node lrs lrl lrx lrr).dual) lx
                (node lls lll llx llr).dual
            else
              node (rs + ls + 1) (node (rs + l.size + 1) (node rs rr.dual rx rl.dual) x l) x_2
                (node (r.size + size + 1) r lx (node lls lll llx llr).dual))
          (node lrs lrl lrx lrr).dual)
      (node lls lll llx llr).dual

Tactic:
dsimp only [dual, id]

Result:
case pos.node.node
α : Type u_1
x : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
ls : ℕ
lx : α
h✝ : ls > delta * rs
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
⊢ (if lrs < ratio * lls then
        node (ls + rs + 1) (node lls lll llx llr) lx (node (rs + lrs + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))
      else
        node (ls + rs + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
          (node (lrr.size + rs + 1) lrr x (node rs rl rx rr))).dual =
    if lrs < ratio * lls then
      node (rs + ls + 1) (node (rs + lrs + 1) (node rs rr.dual rx rl.dual) x (node lrs lrr.dual lrx lrl.dual)) lx
        (node lls llr.dual llx lll.dual)
    else
      node (rs + ls + 1) (node (rs + lrr.dual.size + 1) (node rs rr.dual rx rl.dual) x lrr.dual) lrx
        (node (lrl.dual.size + lls + 1) lrl.dual lx (node lls llr.dual llx lll.dual))

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.balanceL x r).dual = r.dual.balanceR x l.dual

Tactic:
unfold balanceL balanceR

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