-- 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 nil.node.node.nil.refl.refl.hnc
α : 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 1 nil rlx nil).size < ratio * nil.size

case nil.node.node.nil.refl.refl.hc
α : 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
⊢ 1 + 1 > 0

case nil.node.node.nil.refl.refl.hnc
α : 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
⊢ ¬0 + (1 + 1) ≤ 1

Tactic:
all_goals dsimp only [size]; decide

Result:
no goals

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
⊢ rrl.size = 0 ∧ rrr.size = 0

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

Result:
α : 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

Proof state:
case nil.node.node.node.hc
α : 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
⊢ rls + rrs + 1 > 0

Tactic:
apply Nat.zero_lt_succ

Result:
no goals

Proof state:
case pos.nil
α : 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 ≤ nil.size + rr.size
⊢ (node ls ll lx lr).rotateL x (node rs nil rx rr) =
    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 nil) 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)
      nil

Tactic:
rw [size, zero_add] at rd

Result:
case pos.nil
α : 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
⊢ (node ls ll lx lr).rotateL x (node rs nil rx rr) =
    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 nil) 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)
      nil

Proof state:
case pos.nil
α : Type u_1
x : α
ls : ℕ
lx : α
lr : Ordnode α
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
hl : (node ls nil lx lr).Balanced
sl : (node ls nil lx lr).Sized
ld : delta ≤ lr.size
⊢ (node ls nil 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) nil lx (node (size_1 + rs + 1) lr x (node rs rl rx rr))
            else
              node (ls + rs + 1) (node (size + l.size + 1) nil lx l) x_2
                (node (r.size + rs + 1) r x (node rs rl rx rr)))
          lr)
      nil

Tactic:
exact absurd (le_trans ld (balancedSz_zero.1 hl.1.symm)) (by decide)

Result:
no goals

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

Tactic:
obtain rfl : lls = 1 := sl.2.1.1

Result:
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) =
    if 1 + 1 ≤ 1 then ((node 1 nil llx nil).node' lx nil).node' x nil
    else
      if 1 + 1 > 0 then ((node 1 nil llx nil).node' lx nil).rotateR x nil
      else ((node 1 nil llx nil).node' lx nil).node' x nil

Proof state:
case pos.node.nil
α : 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 α
hr : (node rs (node rls rll rlx rlr) rx nil).Balanced
sr : (node rs (node rls rll rlx rlr) rx nil).Sized
rd : delta ≤ (node rls rll rlx rlr).size + nil.size
⊢ (node ls ll lx lr).rotateL x (node rs (node rls rll rlx rlr) rx nil) =
    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 (node rls rll rlx rlr)) rx nil
            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 nil))
          nil)
      (node rls rll rlx rlr)

Tactic:
exact absurd (le_trans rd (balancedSz_zero.1 hr.1)) (by decide)

Result:
no goals

Proof state:
case pos
α : 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
⊢ rls + 1 + rrs = rls + rrs + 1

Tactic:
abel

Result:
no goals

Proof state:
case node.node.hnc
α : 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
⊢ ¬ls + rs ≤ 1

Tactic:
exact not_le_of_gt (add_le_add (Nat.succ_le_of_lt sl.pos) (Nat.succ_le_of_lt sr.pos))

Result:
no goals