α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬size l + size r ≤ 1
H2 : delta * size r < size l
H3 : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
⊢ Valid' o₂ (Ordnode.dual (Ordnode.rotateR 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₂
H1 : ¬size l + size r ≤ 1
H2 : delta * size r < size l
H3 : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
⊢ Valid' o₁ (Ordnode.rotateR l x r) o₂
refine' Valid'.dual_iff.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₂
H1 : ¬size l + size r ≤ 1
H2 : delta * size r < size l
H3 : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
⊢ Valid' o₂ (Ordnode.rotateL (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₂
H1 : ¬size l + size r ≤ 1
H2 : delta * size r < size l
H3 : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
⊢ Valid' o₂ (Ordnode.dual (Ordnode.rotateR l x r)) o₁
rw [dual_rotateR]
case refine'_1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬size l + size r ≤ 1
H2 : delta * size r < size l
H3 : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
⊢ ¬size (Ordnode.dual r) + size (Ordnode.dual l) ≤ 1

case refine'_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₂
H1 : ¬size l + size r ≤ 1
H2 : delta * size r < size l
H3 : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
⊢ delta * size (Ordnode.dual r) < size (Ordnode.dual l)

case refine'_3
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬size l + size r ≤ 1
H2 : delta * size r < size l
H3 : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
⊢ 2 * size (Ordnode.dual l) ≤ 9 * size (Ordnode.dual r) + 5 ∨ size (Ordnode.dual l) ≤ 3
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬size l + size r ≤ 1
H2 : delta * size r < size l
H3 : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
⊢ Valid' o₂ (Ordnode.rotateL (Ordnode.dual r) x (Ordnode.dual l)) o₁
refine' hr.dual.rotateL hl.dual _ _ _
no goals
case refine'_1
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬size l + size r ≤ 1
H2 : delta * size r < size l
H3 : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
⊢ ¬size (Ordnode.dual r) + size (Ordnode.dual l) ≤ 1
rwa [size_dual, size_dual, add_comm]
no goals
case refine'_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₂
H1 : ¬size l + size r ≤ 1
H2 : delta * size r < size l
H3 : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
⊢ delta * size (Ordnode.dual r) < size (Ordnode.dual l)
rwa [size_dual, size_dual]
no goals
case refine'_3
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
hl : Valid' o₁ l ↑x
hr : Valid' (↑x) r o₂
H1 : ¬size l + size r ≤ 1
H2 : delta * size r < size l
H3 : 2 * size l ≤ 9 * size r + 5 ∨ size l ≤ 3
⊢ 2 * size (Ordnode.dual l) ≤ 9 * size (Ordnode.dual r) + 5 ∨ size (Ordnode.dual l) ≤ 3
rwa [size_dual, size_dual]