-- 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 pos.node.node
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
ld : delta ≤ (node lls lll llx llr).size + (node lrs lrl lrx lrr).size
⊢ (if lrs < ratio * lls then (node lls lll llx llr).node3R lx (node lrs lrl lrx lrr) x (node rs rl rx rr)
    else (node lls lll llx llr).node4R lx (node lrs lrl lrx lrr) x (node rs rl rx rr)) =
    if lrs < ratio * lls then
      node (ls + rs + 1) (node lls lll llx llr) lx (node (lrs + rs + 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))

Tactic:
split_ifs

Result:
case pos
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
ld : delta ≤ (node lls lll llx llr).size + (node lrs lrl lrx lrr).size
h✝ : lrs < ratio * lls
⊢ (node lls lll llx llr).node3R lx (node lrs lrl lrx lrr) x (node rs rl rx rr) =
    node (ls + rs + 1) (node lls lll llx llr) lx (node (lrs + rs + 1) (node lrs lrl lrx lrr) x (node rs rl rx rr))

case neg
α : Type u_1
x : α
ls : ℕ
lx : α
rs : ℕ
rl : Ordnode α
rx : α
rr : Ordnode α
hr : (node rs rl rx rr).Balanced
sr : (node rs rl rx rr).Sized
h : ¬delta * ls < rs
h_1 : delta * rs < ls
lls : ℕ
lll : Ordnode α
llx : α
llr : Ordnode α
lrs : ℕ
lrl : Ordnode α
lrx : α
lrr : Ordnode α
hl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Balanced
sl : (node ls (node lls lll llx llr) lx (node lrs lrl lrx lrr)).Sized
ld : delta ≤ (node lls lll llx llr).size + (node lrs lrl lrx lrr).size
h✝ : ¬lrs < ratio * lls
⊢ (node lls lll llx llr).node4R lx (node lrs lrl lrx lrr) x (node rs rl rx rr) =
    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))

Proof state:
case node.nil.node.nil.refl.refl.hc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
llx : α
this : nil.size = 0 ∧ nil.size = 0
hl : ((node 1 nil llx nil).node' lx nil).Balanced
sl : (node ls (node 1 nil llx nil) lx nil).Sized
⊢ nil.size < ratio * (node 1 nil llx nil).size

case node.nil.node.nil.refl.refl.hc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
llx : α
this : nil.size = 0 ∧ nil.size = 0
hl : ((node 1 nil llx nil).node' lx nil).Balanced
sl : (node ls (node 1 nil llx nil) lx nil).Sized
⊢ 1 + 1 > 0

case node.nil.node.nil.refl.refl.hnc
α : Type u_1
x : α
ls : ℕ
lx : α
hr : nil.Balanced
sr : nil.Sized
llx : α
this : nil.size = 0 ∧ nil.size = 0
hl : ((node 1 nil llx nil).node' lx nil).Balanced
sl : (node ls (node 1 nil llx nil) lx nil).Sized
⊢ ¬1 + 1 ≤ 1

Tactic:
all_goals dsimp only [size]; decide

Result:
no goals

Proof state:
case neg
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
h✝ : ¬rls < ratio * rrs
⊢ nil.node4L x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (rls + rrs + 1 + 1) (node (rll.size + 1) nil x rll) rlx
      (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))

Tactic:
simp [node4L, node', sr.2.1.1]

Result:
case neg
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : ((node rls rll rlx rlr).node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
h✝ : ¬rls < ratio * rrs
⊢ rll.size + 1 + (rlr.size + rrs + 1) = rll.size + rlr.size + 1 + rrs + 1

Proof state:
case nil.node.nil.node
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (nil.node' rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs nil rx (node rrs rrl rrx rrr)).Sized
this : rrl.size = 0 ∧ rrr.size = 0
⊢ node 3 (Ordnode.singleton x) rx (node rrs rrl rrx rrr) =
    if 0 + (0 + rrs + 1) ≤ 1 then nil.node' x (nil.node' rx (node rrs rrl rrx rrr))
    else
      if 0 + rrs + 1 > 0 then nil.rotateL x (nil.node' rx (node rrs rrl rrx rrr))
      else nil.node' x (nil.node' rx (node rrs rrl rrx rrr))

Tactic:
cases sr.2.2.2.1.size_eq_zero.1 this.1

Result:
case nil.node.nil.node.refl
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx : α
rrs : ℕ
rrx : α
rrr : Ordnode α
hr : (nil.node' rx (node rrs nil rrx rrr)).Balanced
sr : (node rs nil rx (node rrs nil rrx rrr)).Sized
this : nil.size = 0 ∧ rrr.size = 0
⊢ node 3 (Ordnode.singleton x) rx (node rrs nil rrx rrr) =
    if 0 + (0 + rrs + 1) ≤ 1 then nil.node' x (nil.node' rx (node rrs nil rrx rrr))
    else
      if 0 + rrs + 1 > 0 then nil.rotateL x (nil.node' rx (node rrs nil rrx rrr))
      else nil.node' x (nil.node' rx (node rrs nil rrx rrr))

Proof state:
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

Tactic:
rfl

Result:
no goals

Proof state:
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

Tactic:
have : size lrl = 0 ∧ size lrr = 0 := by
  have := balancedSz_zero.1 hl.1.symm
  rwa [size, sl.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this

Result:
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
this : lrl.size = 0 ∧ lrr.size = 0
⊢ 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