case intro
ι : Type ?u.68133
ι' : Type ?u.68136
α : Type u_1
β : Type u_2
γ : Type ?u.68145
inst✝² : SemilatticeSup α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
u : α → β
h : Tendsto u atTop atTop
a : α
b b' : β
hb' : b < b'
⊢ ∃ a', a' ≥ a ∧ b < u a'
ι : Type ?u.68133
ι' : Type ?u.68136
α : Type u_1
β : Type u_2
γ : Type ?u.68145
inst✝² : SemilatticeSup α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
u : α → β
h : Tendsto u atTop atTop
a : α
b : β
⊢ ∃ a', a' ≥ a ∧ b < u a'
cases' exists_gt b with b' hb'
case intro.intro.intro
ι : Type ?u.68133
ι' : Type ?u.68136
α : Type u_1
β : Type u_2
γ : Type ?u.68145
inst✝² : SemilatticeSup α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
u : α → β
h : Tendsto u atTop atTop
a : α
b b' : β
hb' : b < b'
a' : α
ha' : a' ≥ a
ha'' : b' ≤ u a'
⊢ ∃ a', a' ≥ a ∧ b < u a'
case intro
ι : Type ?u.68133
ι' : Type ?u.68136
α : Type u_1
β : Type u_2
γ : Type ?u.68145
inst✝² : SemilatticeSup α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
u : α → β
h : Tendsto u atTop atTop
a : α
b b' : β
hb' : b < b'
⊢ ∃ a', a' ≥ a ∧ b < u a'
rcases exists_le_of_tendsto_atTop h a b' with ⟨a', ha', ha''⟩
no goals
case intro.intro.intro
ι : Type ?u.68133
ι' : Type ?u.68136
α : Type u_1
β : Type u_2
γ : Type ?u.68145
inst✝² : SemilatticeSup α
inst✝¹ : Preorder β
inst✝ : NoMaxOrder β
u : α → β
h : Tendsto u atTop atTop
a : α
b b' : β
hb' : b < b'
a' : α
ha' : a' ≥ a
ha'' : b' ≤ u a'
⊢ ∃ a', a' ≥ a ∧ b < u a'
exact ⟨a', ha', lt_of_lt_of_le hb' ha''⟩