no goals
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
ol : Bounded l o₁ ↑x
Or : Bounded r (↑x) o₂
sl : Sized l
sr : Sized r
b : BalancedSz (size l) (size r)
bl : Balanced l
br : Balanced r
ol' : Bounded (Ordnode.dual l) (↑x) o₁
sl' : Sized (Ordnode.dual l)
bl' : Balanced (Ordnode.dual l)
or' : Bounded (Ordnode.dual r) o₂ ↑x
sr' : Sized (Ordnode.dual r)
br' : Balanced (Ordnode.dual r)
⊢ size l + size r + 1 = size (Ordnode.dual r) + size (Ordnode.dual l) + 1
simp [size_dual, add_comm]
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
ol : Bounded l o₁ ↑x
Or : Bounded r (↑x) o₂
sl : Sized l
sr : Sized r
b : BalancedSz (size l) (size r)
bl : Balanced l
br : Balanced r
ol' : Bounded (Ordnode.dual l) (↑x) o₁
sl' : Sized (Ordnode.dual l)
bl' : Balanced (Ordnode.dual l)
or' : Bounded (Ordnode.dual r) o₂ ↑x
sr' : Sized (Ordnode.dual r)
br' : Balanced (Ordnode.dual r)
⊢ BalancedSz (size r) (size l)
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
ol : Bounded l o₁ ↑x
Or : Bounded r (↑x) o₂
sl : Sized l
sr : Sized r
b : BalancedSz (size l) (size r)
bl : Balanced l
br : Balanced r
ol' : Bounded (Ordnode.dual l) (↑x) o₁
sl' : Sized (Ordnode.dual l)
bl' : Balanced (Ordnode.dual l)
or' : Bounded (Ordnode.dual r) o₂ ↑x
sr' : Sized (Ordnode.dual r)
br' : Balanced (Ordnode.dual r)
⊢ BalancedSz (size (Ordnode.dual r)) (size (Ordnode.dual l))
rw [size_dual, size_dual]
no goals
α : Type u_1
inst✝ : Preorder α
l : Ordnode α
x : α
r : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
ol : Bounded l o₁ ↑x
Or : Bounded r (↑x) o₂
sl : Sized l
sr : Sized r
b : BalancedSz (size l) (size r)
bl : Balanced l
br : Balanced r
ol' : Bounded (Ordnode.dual l) (↑x) o₁
sl' : Sized (Ordnode.dual l)
bl' : Balanced (Ordnode.dual l)
or' : Bounded (Ordnode.dual r) o₂ ↑x
sr' : Sized (Ordnode.dual r)
br' : Balanced (Ordnode.dual r)
⊢ BalancedSz (size r) (size l)
exact b.symm