α : Type u_1
inst✝ : Preorder α
t₁ t₂ : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
x : α
h₁ : Bounded t₁ o₁ ↑x
h₂ : Bounded t₂ (↑x) o₂
y : α
yx : y < x
⊢ All (fun z => y < z) t₂
α : Type u_1
inst✝ : Preorder α
t₁ t₂ : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
x : α
h₁ : Bounded t₁ o₁ ↑x
h₂ : Bounded t₂ (↑x) o₂
⊢ All (fun y => All (fun z => y < z) t₂) t₁
refine h₁.mem_lt.imp fun y yx => ?_
no goals
α : Type u_1
inst✝ : Preorder α
t₁ t₂ : Ordnode α
o₁ : WithBot α
o₂ : WithTop α
x : α
h₁ : Bounded t₁ o₁ ↑x
h₂ : Bounded t₂ (↑x) o₂
y : α
yx : y < x
⊢ All (fun z => y < z) t₂
exact h₂.mem_gt.imp fun z xz => lt_trans yx xz