α : 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₁ : size l = 0 → size r ≤ 1
H₂ : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l
H₃ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
⊢ Valid' o₁ (Ordnode.balance' 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₁ : size l = 0 → size r ≤ 1
H₂ : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l
H₃ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
⊢ Valid' o₁ (balanceL l x r) o₂
rw [balanceL_eq_balance hl.2 hr.2 H₁ H₂, balance_eq_balance' hl.3 hr.3 hl.2 hr.2]
α : 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₁ : size l = 0 → size r ≤ 1
H₂ : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l
H₃ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
⊢ 2 * size r ≤ 9 * size l + 5
α : 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₁ : size l = 0 → size r ≤ 1
H₂ : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l
H₃ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
⊢ Valid' o₁ (Ordnode.balance' l x r) o₂
refine' hl.balance'_aux hr (Or.inl _) H₃
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₁ : size l = 0 → size r ≤ 1
H₂ : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l
H₃ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
r0 : size r = 0
⊢ 2 * size r ≤ 9 * size l + 5

case 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₁ : size l = 0 → size r ≤ 1
H₂ : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l
H₃ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
r0 : size r > 0
⊢ 2 * size r ≤ 9 * size l + 5
α : 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₁ : size l = 0 → size r ≤ 1
H₂ : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l
H₃ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
⊢ 2 * size r ≤ 9 * size l + 5
cases' Nat.eq_zero_or_pos (size r) with r0 r0
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₁ : size l = 0 → size r ≤ 1
H₂ : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l
H₃ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
r0 : size r > 0
l0 : size l = 0
⊢ 2 * size r ≤ 9 * size l + 5

case 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₁ : size l = 0 → size r ≤ 1
H₂ : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l
H₃ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
r0 : size r > 0
l0 : size l > 0
⊢ 2 * size r ≤ 9 * size l + 5
case 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₁ : size l = 0 → size r ≤ 1
H₂ : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l
H₃ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
r0 : size r > 0
⊢ 2 * size r ≤ 9 * size l + 5
cases' Nat.eq_zero_or_pos (size l) with l0 l0
case 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₁ : size l = 0 → size r ≤ 1
H₃ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
r0 : size r > 0
l0 : size l > 0
H₂ : size r ≤ 3 * size l
⊢ 2 * size r ≤ 9 * size l + 5
case 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₁ : size l = 0 → size r ≤ 1
H₂ : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l
H₃ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
r0 : size r > 0
l0 : size l > 0
⊢ 2 * size r ≤ 9 * size l + 5
replace H₂ : _ ≤ 3 * _ := H₂ l0 r0
no goals
case 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₁ : size l = 0 → size r ≤ 1
H₃ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
r0 : size r > 0
l0 : size l > 0
H₂ : size r ≤ 3 * size l
⊢ 2 * size r ≤ 9 * size l + 5
linarith
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₁ : size l = 0 → size r ≤ 1
H₂ : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l
H₃ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
r0 : size r = 0
⊢ 2 * 0 ≤ 9 * size l + 5
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₁ : size l = 0 → size r ≤ 1
H₂ : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l
H₃ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
r0 : size r = 0
⊢ 2 * size r ≤ 9 * size l + 5
rw [r0]
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₁ : size l = 0 → size r ≤ 1
H₂ : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l
H₃ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
r0 : size r = 0
⊢ 2 * 0 ≤ 9 * size l + 5
exact Nat.zero_le _
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₁ : size l = 0 → size r ≤ 1
H₂ : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l
H₃ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
r0 : size r > 0
l0 : size l = 0
⊢ 2 * size r ≤ 9 * 0 + 5
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₁ : size l = 0 → size r ≤ 1
H₂ : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l
H₃ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
r0 : size r > 0
l0 : size l = 0
⊢ 2 * size r ≤ 9 * size l + 5
rw [l0]
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₁ : size l = 0 → size r ≤ 1
H₂ : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l
H₃ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
r0 : size r > 0
l0 : size l = 0
⊢ 2 * size r ≤ 9 * 0 + 5
exact le_trans (Nat.mul_le_mul_left _ (H₁ l0)) (by decide)
no goals
α : 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₁ : size l = 0 → size r ≤ 1
H₂ : 1 ≤ size l → 1 ≤ size r → size r ≤ delta * size l
H₃ : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
r0 : size r > 0
l0 : size l = 0
⊢ 2 * 1 ≤ 9 * 0 + 5
decide