α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
H₂ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
⊢ Valid' o₁
    (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)
    o₂
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
H₂ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
⊢ Valid' o₁ (balance' l x r) o₂
rw [balance']
case inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
H₂ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
h : size l + size r ≤ 1
⊢ Valid' o₁ (Ordnode.node' l x r) o₂

case inr.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
H₂ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
h : ¬size l + size r ≤ 1
h_1 : size r > delta * size l
⊢ Valid' o₁ (Ordnode.rotateL l x r) o₂

case inr.inr.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
H₂ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
h : ¬size l + size r ≤ 1
h_1 : ¬size r > delta * size l
h_2 : size l > delta * size r
⊢ Valid' o₁ (Ordnode.rotateR l x r) o₂

case inr.inr.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
H₂ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
h : ¬size l + size r ≤ 1
h_1 : ¬size r > delta * size l
h_2 : ¬size l > delta * size r
⊢ Valid' o₁ (Ordnode.node' l x r) o₂
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
H₂ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
⊢ Valid' o₁
    (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)
    o₂
split_ifs with h h_1 h_2
no goals
case inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
H₂ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
h : size l + size r ≤ 1
⊢ Valid' o₁ (Ordnode.node' l x r) o₂
exact hl.node' hr (Or.inl h)
no goals
case inr.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
H₂ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
h : ¬size l + size r ≤ 1
h_1 : size r > delta * size l
⊢ Valid' o₁ (Ordnode.rotateL l x r) o₂
exact hl.rotateL hr h h_1 H₁
no goals
case inr.inr.inl
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
H₂ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
h : ¬size l + size r ≤ 1
h_1 : ¬size r > delta * size l
h_2 : size l > delta * size r
⊢ Valid' o₁ (Ordnode.rotateR l x r) o₂
exact hl.rotateR hr h h_2 H₂
no goals
case inr.inr.inr
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H₁ : 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
H₂ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
h : ¬size l + size r ≤ 1
h_1 : ¬size r > delta * size l
h_2 : ¬size l > delta * size r
⊢ Valid' o₁ (Ordnode.node' l x r) o₂
exact hl.node' hr (Or.inr ⟨not_lt.1 h_2, not_lt.1 h_1⟩)