α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Bounded (Ordnode.dual t) o₂ o₁
this : Bounded (Ordnode.dual (Ordnode.dual t)) o₁ o₂
⊢ Bounded t o₁ o₂
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Bounded (Ordnode.dual t) o₂ o₁
⊢ Bounded t o₁ o₂
have := Bounded.dual h
no goals
α : Type u_1
inst✝ : Preorder α
t : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
h : Bounded (Ordnode.dual t) o₂ o₁
this : Bounded (Ordnode.dual (Ordnode.dual t)) o₁ o₂
⊢ Bounded t o₁ o₂
rwa [dual_dual, OrderDual.Preorder.dual_dual] at this