α : 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 r = 0 → size l ≤ 1
H₂ : 1 ≤ size r → 1 ≤ size l → size l ≤ delta * size r
H₃ : 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
⊢ Valid' o₂ (Ordnode.balanceL (Ordnode.dual r) x (Ordnode.dual l)) 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 r = 0 → size l ≤ 1
H₂ : 1 ≤ size r → 1 ≤ size l → size l ≤ delta * size r
H₃ : 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
⊢ Valid' o₁ (balanceR l x r) o₂
rw [Valid'.dual_iff, dual_balanceR]
α : 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 r = 0 → size l ≤ 1
H₂ : 1 ≤ size r → 1 ≤ size l → size l ≤ delta * size r
H₃ : 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
this :
  (size (Ordnode.dual r) = 0 → size (Ordnode.dual l) ≤ 1) →
    (1 ≤ size (Ordnode.dual r) → 1 ≤ size (Ordnode.dual l) → size (Ordnode.dual l) ≤ delta * size (Ordnode.dual r)) →
      2 * size (Ordnode.dual r) ≤ 9 * size (Ordnode.dual l) + 5 ∨ size (Ordnode.dual r) ≤ 3 →
        Valid' o₂ (Ordnode.balanceL (Ordnode.dual r) x (Ordnode.dual l)) o₁
⊢ Valid' o₂ (Ordnode.balanceL (Ordnode.dual r) x (Ordnode.dual l)) 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 r = 0 → size l ≤ 1
H₂ : 1 ≤ size r → 1 ≤ size l → size l ≤ delta * size r
H₃ : 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
⊢ Valid' o₂ (Ordnode.balanceL (Ordnode.dual r) x (Ordnode.dual l)) o₁
have := hr.dual.balanceL_aux hl.dual
α : 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 r = 0 → size l ≤ 1
H₂ : 1 ≤ size r → 1 ≤ size l → size l ≤ delta * size r
H₃ : 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
this :
  (size r = 0 → size l ≤ 1) →
    (1 ≤ size r → 1 ≤ size l → size l ≤ delta * size r) →
      2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3 → Valid' o₂ (Ordnode.balanceL (Ordnode.dual r) x (Ordnode.dual l)) o₁
⊢ Valid' o₂ (Ordnode.balanceL (Ordnode.dual r) x (Ordnode.dual l)) 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 r = 0 → size l ≤ 1
H₂ : 1 ≤ size r → 1 ≤ size l → size l ≤ delta * size r
H₃ : 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
this :
  (size (Ordnode.dual r) = 0 → size (Ordnode.dual l) ≤ 1) →
    (1 ≤ size (Ordnode.dual r) → 1 ≤ size (Ordnode.dual l) → size (Ordnode.dual l) ≤ delta * size (Ordnode.dual r)) →
      2 * size (Ordnode.dual r) ≤ 9 * size (Ordnode.dual l) + 5 ∨ size (Ordnode.dual r) ≤ 3 →
        Valid' o₂ (Ordnode.balanceL (Ordnode.dual r) x (Ordnode.dual l)) o₁
⊢ Valid' o₂ (Ordnode.balanceL (Ordnode.dual r) x (Ordnode.dual l)) o₁
rw [size_dual, size_dual] at this
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 r = 0 → size l ≤ 1
H₂ : 1 ≤ size r → 1 ≤ size l → size l ≤ delta * size r
H₃ : 2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3
this :
  (size r = 0 → size l ≤ 1) →
    (1 ≤ size r → 1 ≤ size l → size l ≤ delta * size r) →
      2 * size r ≤ 9 * size l + 5 ∨ size r ≤ 3 → Valid' o₂ (Ordnode.balanceL (Ordnode.dual r) x (Ordnode.dual l)) o₁
⊢ Valid' o₂ (Ordnode.balanceL (Ordnode.dual r) x (Ordnode.dual l)) o₁
exact this H₁ H₂ H₃