case node
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : Sized (node size✝ l✝ x✝ r✝)
⊢ size (if size l✝ < ratio * size r✝ then Ordnode.node3L l x l✝ x✝ r✝ else Ordnode.node4L l x l✝ x✝ r✝) =
    size l + size✝ + 1
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hm : Sized r
⊢ size (Ordnode.rotateL l x r) = size l + size r + 1
cases r <;> simp [Ordnode.rotateL]
case node
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : Sized (node size✝ l✝ x✝ r✝)
⊢ size (if size l✝ < ratio * size r✝ then Ordnode.node3L l x l✝ x✝ r✝ else Ordnode.node4L l x l✝ x✝ r✝) =
    size l + (size l✝ + size r✝ + 1) + 1
case node
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : Sized (node size✝ l✝ x✝ r✝)
⊢ size (if size l✝ < ratio * size r✝ then Ordnode.node3L l x l✝ x✝ r✝ else Ordnode.node4L l x l✝ x✝ r✝) =
    size l + size✝ + 1
simp [size, hm.1]
no goals
case node
α : Type u_1
l : Ordnode α
x : α
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hm : Sized (node size✝ l✝ x✝ r✝)
⊢ size (if size l✝ < ratio * size r✝ then Ordnode.node3L l x l✝ x✝ r✝ else Ordnode.node4L l x l✝ x✝ r✝) =
    size l + (size l✝ + size r✝ + 1) + 1
split_ifs <;> simp [node3L_size, node4L_size hm.2.1] <;> abel