-- Mathlib/Data/Ordmap/Ordset.lean
theorem balance_eq_balance' {l x r} (hl : Balanced l) (hr : Balanced r) (sl : Sized l)
    (sr : Sized r) : @balance α l x r = balance' l x r

Proof state:
case node.nil
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (ll.node' lx lr).Balanced
sl : (node ls ll lx lr).Sized
hr : nil.Balanced
sr : nil.Sized
⊢ (ll.node' lx lr).balance x nil = (ll.node' lx lr).balance' x nil

Tactic:
obtain - | ⟨lls, lll, llx, llr⟩ := ll <;> obtain - | ⟨lrs, lrl, lrx, lrr⟩ := lr <;>
  dsimp [balance, balance']

Result:
case node.nil.nil.nil
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
hl : (nil.node' lx nil).Balanced
sl : (node ls nil lx nil).Sized
⊢ node 2 (nil.node' lx nil) x nil = (nil.node' lx nil).node' x nil

case node.nil.nil.node
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (nil.node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
⊢ node 3 (Ordnode.singleton lx) lrx (Ordnode.singleton x) =
    if 0 + lrs + 1 ≤ 1 then (nil.node' lx (node lrs lrl lrx lrr)).node' x nil
    else
      if 0 + lrs + 1 > 0 then (nil.node' lx (node lrs lrl lrx lrr)).rotateR x nil
      else (nil.node' lx (node lrs lrl lrx lrr)).node' x nil

case node.nil.node.nil
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((node lls lll llx llr).node' lx nil).Balanced
sl : (node ls (node lls lll llx llr) lx nil).Sized
⊢ node 3 (node lls lll llx llr) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then ((node lls lll llx llr).node' lx nil).node' x nil
    else
      if lls + 1 > 0 then ((node lls lll llx llr).node' lx nil).rotateR x nil
      else ((node lls lll llx llr).node' lx nil).node' x nil

case node.nil.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
⊢ (if lrs < ratio * lls then
      node (lls + lrs + 1 + 1) (node lls lll llx llr) lx (node (lrs + 1) (node lrs lrl lrx lrr) x nil)
    else
      node (lls + lrs + 1 + 1) (node (lls + lrl.size + 1) (node lls lll llx llr) lx lrl) lrx
        (node (lrr.size + 1) lrr x nil)) =
    if lls + lrs + 1 ≤ 1 then ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).node' x nil
    else
      if lls + lrs + 1 > 0 then ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).rotateR x nil
      else ((node lls lll llx llr).node' lx (node lrs lrl lrx lrr)).node' x nil

Proof state:
case node.node
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
⊢ (if delta * ls < rs then
      rec nil
        (fun size l x_1 r l_ih r_ih =>
          rec nil
            (fun size_1 l_1 x_2 r_1 l_ih r_ih =>
              if size < ratio * size_1 then node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x rl) rx rr
              else
                node (ls + rs + 1) (node (ls + l.size + 1) (node ls ll lx lr) x l) x_1
                  (node (r.size + size_1 + 1) r rx rr))
            rr)
        rl
    else
      if delta * rs < ls then
        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) ll lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
                else
                  node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2
                    (node (r.size + rs + 1) r x (node rs rl rx rr)))
              lr)
          ll
      else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)) =
    if ls + rs ≤ 1 then (node ls ll lx lr).node' x (node rs rl rx rr)
    else
      if delta * ls < rs then (node ls ll lx lr).rotateL x (node rs rl rx rr)
      else
        if delta * rs < ls then (node ls ll lx lr).rotateR x (node rs rl rx rr)
        else (node ls ll lx lr).node' x (node rs rl rx rr)

Tactic:
symm

Result:
case node.node
α : Type u_1
x : α
ls : ℕ
ll : Ordnode α
lx : α
lr : Ordnode α
hl : (node ls ll lx lr).Balanced
sl : (node ls ll lx lr).Sized
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
⊢ (if ls + rs ≤ 1 then (node ls ll lx lr).node' x (node rs rl rx rr)
    else
      if delta * ls < rs then (node ls ll lx lr).rotateL x (node rs rl rx rr)
      else
        if delta * rs < ls then (node ls ll lx lr).rotateR x (node rs rl rx rr)
        else (node ls ll lx lr).node' x (node rs rl rx rr)) =
    if delta * ls < rs then
      rec nil
        (fun size l x_1 r l_ih r_ih =>
          rec nil
            (fun size_1 l_1 x_2 r_1 l_ih r_ih =>
              if size < ratio * size_1 then node (ls + rs + 1) (node (ls + size + 1) (node ls ll lx lr) x rl) rx rr
              else
                node (ls + rs + 1) (node (ls + l.size + 1) (node ls ll lx lr) x l) x_1
                  (node (r.size + size_1 + 1) r rx rr))
            rr)
        rl
    else
      if delta * rs < ls then
        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) ll lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
                else
                  node (ls + rs + 1) (node (size + l.size + 1) ll lx l) x_2
                    (node (r.size + rs + 1) r x (node rs rl rx rr)))
              lr)
          ll
      else node (ls + rs + 1) (node ls ll lx lr) x (node rs rl rx rr)

Proof state:
case node.nil.node.nil
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
hl : ((node lls lll llx llr).node' lx nil).Balanced
sl : (node ls (node lls lll llx llr) lx nil).Sized
this : lll.size = 0 ∧ llr.size = 0
⊢ node 3 (node lls lll llx llr) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then ((node lls lll llx llr).node' lx nil).node' x nil
    else
      if lls + 1 > 0 then ((node lls lll llx llr).node' lx nil).rotateR x nil
      else ((node lls lll llx llr).node' lx nil).node' x nil

Tactic:
cases sl.2.1.2.1.size_eq_zero.1 this.1

Result:
case node.nil.node.nil.refl
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lls : ℕ
llx : α
llr : Ordnode α
hl : ((node lls nil llx llr).node' lx nil).Balanced
sl : (node ls (node lls nil llx llr) lx nil).Sized
this : nil.size = 0 ∧ llr.size = 0
⊢ node 3 (node lls nil llx llr) lx (Ordnode.singleton x) =
    if lls + 1 ≤ 1 then ((node lls nil llx llr).node' lx nil).node' x nil
    else
      if lls + 1 > 0 then ((node lls nil llx llr).node' lx nil).rotateR x nil
      else ((node lls nil llx llr).node' lx nil).node' x nil

Proof state:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (nil.node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
⊢ lrl.size = 0 ∧ lrr.size = 0

Tactic:
have := balancedSz_zero.1 hl.1.symm

Result:
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (nil.node' lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls nil lx (node lrs lrl lrx lrr)).Sized
this : (node lrs lrl lrx lrr).size ≤ 1
⊢ lrl.size = 0 ∧ lrr.size = 0