α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Sized l
hr : Sized r
⊢ size
      (if size l + size r ≤ 1 then node' l x r
      else
        if size r > delta * size l then rotateL l x r
        else if size l > delta * size r then rotateR l x r else node' l x r) =
    size l + size r + 1
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Sized l
hr : Sized r
⊢ size (balance' l x r) = size l + size r + 1
unfold balance'
case inl
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Sized l
hr : Sized r
h✝ : size l + size r ≤ 1
⊢ size (node' l x r) = size l + size r + 1

case inr.inl
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Sized l
hr : Sized r
h✝¹ : ¬size l + size r ≤ 1
h✝ : size r > delta * size l
⊢ size (rotateL l x r) = size l + size r + 1

case inr.inr.inl
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Sized l
hr : Sized r
h✝² : ¬size l + size r ≤ 1
h✝¹ : ¬size r > delta * size l
h✝ : size l > delta * size r
⊢ size (rotateR l x r) = size l + size r + 1

case inr.inr.inr
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Sized l
hr : Sized r
h✝² : ¬size l + size r ≤ 1
h✝¹ : ¬size r > delta * size l
h✝ : ¬size l > delta * size r
⊢ size (node' l x r) = size l + size r + 1
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Sized l
hr : Sized r
⊢ size
      (if size l + size r ≤ 1 then node' l x r
      else
        if size r > delta * size l then rotateL l x r
        else if size l > delta * size r then rotateR l x r else node' l x r) =
    size l + size r + 1
split_ifs
no goals
case inl
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Sized l
hr : Sized r
h✝ : size l + size r ≤ 1
⊢ size (node' l x r) = size l + size r + 1
rfl
no goals
case inr.inl
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Sized l
hr : Sized r
h✝¹ : ¬size l + size r ≤ 1
h✝ : size r > delta * size l
⊢ size (rotateL l x r) = size l + size r + 1
exact hr.rotateL_size
no goals
case inr.inr.inl
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Sized l
hr : Sized r
h✝² : ¬size l + size r ≤ 1
h✝¹ : ¬size r > delta * size l
h✝ : size l > delta * size r
⊢ size (rotateR l x r) = size l + size r + 1
exact hl.rotateR_size
no goals
case inr.inr.inr
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Sized l
hr : Sized r
h✝² : ¬size l + size r ≤ 1
h✝¹ : ¬size r > delta * size l
h✝ : ¬size l > delta * size r
⊢ size (node' l x r) = size l + size r + 1
rfl