α : Type u_2
β : Type ?u.5253
ι : Type u_1
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
this : Tendsto (rangeFactorization f) atTop atTop
⊢ Tendsto f atTop (𝓝 a)

case this
α : Type u_2
β : Type ?u.5253
ι : Type u_1
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto (rangeFactorization f) atTop atTop
α : Type u_2
β : Type ?u.5253
ι : Type u_1
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto f atTop (𝓝 a)
suffices : Tendsto (rangeFactorization f) atTop atTop
case this
α : Type u_2
β : Type ?u.5253
ι : Type u_1
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto (rangeFactorization f) atTop atTop
α : Type u_2
β : Type ?u.5253
ι : Type u_1
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
this : Tendsto (rangeFactorization f) atTop atTop
⊢ Tendsto f atTop (𝓝 a)

case this
α : Type u_2
β : Type ?u.5253
ι : Type u_1
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto (rangeFactorization f) atTop atTop
exact (SupConvergenceClass.tendsto_coe_atTop_isLUB _ _ ha).comp this
no goals
case this
α : Type u_2
β : Type ?u.5253
ι : Type u_1
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto (rangeFactorization f) atTop atTop
exact h_mono.rangeFactorization.tendsto_atTop_atTop fun b => b.2.imp fun a ha => ha.ge