-- 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:
α : 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 : ℕ
rx : α
rr : Ordnode α
h : delta * ls < rs
hr : (node rs nil rx rr).Balanced
sr : (node rs nil rx rr).Sized
rd : delta ≤ rr.size
⊢ ¬delta ≤ 1

Tactic:
decide

Result:
no goals

Proof state:
case nil.node.node.nil.refl.refl
α : Type u_1
x : α
hl : nil.Balanced
sl : nil.Sized
rs : ℕ
rx rlx : α
this : nil.size = 0 ∧ nil.size = 0
hr : ((node 1 nil rlx nil).node' rx nil).Balanced
sr : (node rs (node 1 nil rlx nil) rx nil).Sized
⊢ node 3 (Ordnode.singleton x) rlx (Ordnode.singleton rx) = nil.node4L x (node 1 nil rlx nil) rx nil

Tactic:
rfl

Result:
no goals

Proof state:
case pos
α : 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
h : ¬delta * ls < rs
h_1 : delta * rs < ls
⊢ (node ls ll lx lr).rotateR x (node rs rl rx rr) =
    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

Tactic:
have ld : delta ≤ size ll + size lr := by
  have := lt_of_le_of_lt (Nat.mul_le_mul_left _ sr.pos) h_1
  rwa [sl.1, Nat.lt_succ_iff] at this

Result:
case pos
α : 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
h : ¬delta * ls < rs
h_1 : delta * rs < ls
ld : delta ≤ ll.size + lr.size
⊢ (node ls ll lx lr).rotateR x (node rs rl rx rr) =
    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

Proof state:
case node.nil.node.nil.refl.refl
α : 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
⊢ node 3 (node 1 nil llx nil) lx (Ordnode.singleton x) = (node 1 nil llx nil).node3R lx nil x nil

Tactic:
rfl

Result:
no goals

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

Tactic:
dsimp only [size]

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

Proof state:
α : 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 : (node rrs rrl rrx rrr).size ≤ 1
⊢ rrl.size = 0 ∧ rrr.size = 0

Tactic:
rwa [size, sr.2.2.1, Nat.succ_le_succ_iff, Nat.le_zero, add_eq_zero] at this

Result:
no goals

Proof state:
case pos.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 : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
rd : delta ≤ (node rls rll rlx rlr).size + (node rrs rrl rrx rrr).size
⊢ (if rls < ratio * rrs then (node ls ll lx lr).node3L x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)
    else (node ls ll lx lr).node4L x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)) =
    if rls < ratio * rrs then
      node (ls + rs + 1) (node (ls + rls + 1) (node ls ll lx lr) x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)
    else
      node (ls + rs + 1) (node (ls + rll.size + 1) (node ls ll lx lr) x rll) rlx
        (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))

Tactic:
split_ifs

Result:
case pos
α : 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 : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
rd : delta ≤ (node rls rll rlx rlr).size + (node rrs rrl rrx rrr).size
h✝ : rls < ratio * rrs
⊢ (node ls ll lx lr).node3L x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (ls + rs + 1) (node (ls + rls + 1) (node ls ll lx lr) x (node rls rll rlx rlr)) rx (node rrs rrl rrx rrr)

case neg
α : 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 : ℕ
rx : α
h : delta * ls < rs
rls : ℕ
rll : Ordnode α
rlx : α
rlr : Ordnode α
rrs : ℕ
rrl : Ordnode α
rrx : α
rrr : Ordnode α
hr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Balanced
sr : (node rs (node rls rll rlx rlr) rx (node rrs rrl rrx rrr)).Sized
rd : delta ≤ (node rls rll rlx rlr).size + (node rrs rrl rrx rrr).size
h✝ : ¬rls < ratio * rrs
⊢ (node ls ll lx lr).node4L x (node rls rll rlx rlr) rx (node rrs rrl rrx rrr) =
    node (ls + rs + 1) (node (ls + rll.size + 1) (node ls ll lx lr) x rll) rlx
      (node (rlr.size + rrs + 1) rlr rx (node rrs rrl rrx rrr))