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

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
⊢ Sized (Ordnode.rotateL l x r)

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
⊢ Sized (Ordnode.rotateR l x r)

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
⊢ Sized (Ordnode.node' l x r)
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Sized l
hr : Sized r
⊢ Sized
    (if size l + size r ≤ 1 then Ordnode.node' l x r
    else
      if size r > delta * size l then Ordnode.rotateL l x r
      else if size l > delta * size r then Ordnode.rotateR l x r else Ordnode.node' l x r)
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
⊢ Sized (Ordnode.node' l x r)
exact hl.node' hr
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
⊢ Sized (Ordnode.rotateL l x r)
exact hl.rotateL hr
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
⊢ Sized (Ordnode.rotateR l x r)
exact hl.rotateR hr
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
⊢ Sized (Ordnode.node' l x r)
exact hl.node' hr