case nil
α : Type u_1
l : Ordnode α
x : α
hl : Sized l
hr : Sized nil
⊢ Sized (Ordnode.rotateL l x nil)

case node
α : Type u_1
l : Ordnode α
x : α
hl : Sized l
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : Sized (node size✝ l✝ x✝ r✝)
⊢ Sized (Ordnode.rotateL l x (node size✝ l✝ x✝ r✝))
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : Sized l
hr : Sized r
⊢ Sized (Ordnode.rotateL l x r)
cases r
case node
α : Type u_1
l : Ordnode α
x : α
hl : Sized l
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : Sized (node size✝ l✝ x✝ r✝)
⊢ Sized (if size l✝ < ratio * size r✝ then Ordnode.node3L l x l✝ x✝ r✝ else Ordnode.node4L l x l✝ x✝ r✝)
case node
α : Type u_1
l : Ordnode α
x : α
hl : Sized l
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : Sized (node size✝ l✝ x✝ r✝)
⊢ Sized (Ordnode.rotateL l x (node size✝ l✝ x✝ r✝))
rw [rotateL]
case node.inl
α : Type u_1
l : Ordnode α
x : α
hl : Sized l
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : Sized (node size✝ l✝ x✝ r✝)
h✝ : size l✝ < ratio * size r✝
⊢ Sized (Ordnode.node3L l x l✝ x✝ r✝)

case node.inr
α : Type u_1
l : Ordnode α
x : α
hl : Sized l
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : Sized (node size✝ l✝ x✝ r✝)
h✝ : ¬size l✝ < ratio * size r✝
⊢ Sized (Ordnode.node4L l x l✝ x✝ r✝)
case node
α : Type u_1
l : Ordnode α
x : α
hl : Sized l
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : Sized (node size✝ l✝ x✝ r✝)
⊢ Sized (if size l✝ < ratio * size r✝ then Ordnode.node3L l x l✝ x✝ r✝ else Ordnode.node4L l x l✝ x✝ r✝)
split_ifs
no goals
case nil
α : Type u_1
l : Ordnode α
x : α
hl : Sized l
hr : Sized nil
⊢ Sized (Ordnode.rotateL l x nil)
exact hl.node' hr
no goals
case node.inl
α : Type u_1
l : Ordnode α
x : α
hl : Sized l
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : Sized (node size✝ l✝ x✝ r✝)
h✝ : size l✝ < ratio * size r✝
⊢ Sized (Ordnode.node3L l x l✝ x✝ r✝)
exact hl.node3L hr.2.1 hr.2.2
no goals
case node.inr
α : Type u_1
l : Ordnode α
x : α
hl : Sized l
size✝ : ℕ
l✝ : Ordnode α
x✝ : α
r✝ : Ordnode α
hr : Sized (node size✝ l✝ x✝ r✝)
h✝ : ¬size l✝ < ratio * size r✝
⊢ Sized (Ordnode.node4L l x l✝ x✝ r✝)
exact hl.node4L hr.2.1 hr.2.2