α : Type ?u.20985
x y z : ℝ
l : Filter α
A : Tendsto (fun x => x + 1) atTop atTop
⊢ Tendsto exp atTop atTop
α : Type ?u.20985
x y z : ℝ
l : Filter α
⊢ Tendsto exp atTop atTop
have A : Tendsto (fun x : ℝ => x + 1) atTop atTop :=
  tendsto_atTop_add_const_right atTop 1 tendsto_id
α : Type ?u.20985
x y z : ℝ
l : Filter α
A : Tendsto (fun x => x + 1) atTop atTop
B : ∀ᶠ (x : ℝ) in atTop, x + 1 ≤ exp x
⊢ Tendsto exp atTop atTop
α : Type ?u.20985
x y z : ℝ
l : Filter α
A : Tendsto (fun x => x + 1) atTop atTop
⊢ Tendsto exp atTop atTop
have B : ∀ᶠ x in atTop, x + 1 ≤ exp x := eventually_atTop.2 ⟨0, fun x _ => add_one_le_exp x⟩
no goals
α : Type ?u.20985
x y z : ℝ
l : Filter α
A : Tendsto (fun x => x + 1) atTop atTop
B : ∀ᶠ (x : ℝ) in atTop, x + 1 ≤ exp x
⊢ Tendsto exp atTop atTop
exact tendsto_atTop_mono' atTop B A