α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto (re ∘ f) l atBot ↔ Tendsto (fun x => (f x).re) l atBot
α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto (fun x => exp (f x)) l (𝓝 0) ↔ Tendsto (fun x => (f x).re) l atBot
simp_rw [←comp_apply (f := exp), ← tendsto_comap_iff, comap_exp_nhds_zero, tendsto_comap_iff]
no goals
α : Type u_1
l : Filter α
f : α → ℂ
⊢ Tendsto (re ∘ f) l atBot ↔ Tendsto (fun x => (f x).re) l atBot
rfl