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