ι : Type ?u.65107
ι' : Type ?u.65110
α : Type u_1
β : Type u_2
γ : Type ?u.65119
inst✝¹ : SemilatticeSup α
inst✝ : Preorder β
u : α → β
h : Tendsto u atTop atTop
a : α
b : β
this : Nonempty α
⊢ ∃ a', a' ≥ a ∧ b ≤ u a'
ι : Type ?u.65107
ι' : Type ?u.65110
α : Type u_1
β : Type u_2
γ : Type ?u.65119
inst✝¹ : SemilatticeSup α
inst✝ : Preorder β
u : α → β
h : Tendsto u atTop atTop
a : α
b : β
⊢ ∃ a', a' ≥ a ∧ b ≤ u a'
have : Nonempty α := ⟨a⟩
ι : Type ?u.65107
ι' : Type ?u.65110
α : Type u_1
β : Type u_2
γ : Type ?u.65119
inst✝¹ : SemilatticeSup α
inst✝ : Preorder β
u : α → β
h : Tendsto u atTop atTop
a : α
b : β
this✝ : Nonempty α
this : ∀ᶠ (x : α) in atTop, a ≤ x ∧ b ≤ u x
⊢ ∃ a', a' ≥ a ∧ b ≤ u a'
ι : Type ?u.65107
ι' : Type ?u.65110
α : Type u_1
β : Type u_2
γ : Type ?u.65119
inst✝¹ : SemilatticeSup α
inst✝ : Preorder β
u : α → β
h : Tendsto u atTop atTop
a : α
b : β
this : Nonempty α
⊢ ∃ a', a' ≥ a ∧ b ≤ u a'
have : ∀ᶠ x in atTop, a ≤ x ∧ b ≤ u x :=
  (eventually_ge_atTop a).and (h.eventually <| eventually_ge_atTop b)
no goals
ι : Type ?u.65107
ι' : Type ?u.65110
α : Type u_1
β : Type u_2
γ : Type ?u.65119
inst✝¹ : SemilatticeSup α
inst✝ : Preorder β
u : α → β
h : Tendsto u atTop atTop
a : α
b : β
this✝ : Nonempty α
this : ∀ᶠ (x : α) in atTop, a ≤ x ∧ b ≤ u x
⊢ ∃ a', a' ≥ a ∧ b ≤ u a'
exact this.exists