c : ℝ
⊢ Tendsto (fun i => ∫ (x : ℝ) in id i..c, exp x) atBot (𝓝 (exp c))
c : ℝ
⊢ (∫ (x : ℝ) in Iic c, exp x) = exp c
refine'
  tendsto_nhds_unique
    (intervalIntegral_tendsto_integral_Iic _ (integrableOn_exp_Iic _) tendsto_id) _
c : ℝ
⊢ Tendsto (fun i => exp c - exp (id i)) atBot (𝓝 (exp c - 0))
c : ℝ
⊢ Tendsto (fun i => ∫ (x : ℝ) in id i..c, exp x) atBot (𝓝 (exp c))
simp_rw [integral_exp, show 𝓝 (exp c) = 𝓝 (exp c - 0) by rw [sub_zero]]
no goals
c : ℝ
⊢ Tendsto (fun i => exp c - exp (id i)) atBot (𝓝 (exp c - 0))
exact tendsto_exp_atBot.const_sub _
no goals
c : ℝ
⊢ 𝓝 (exp c) = 𝓝 (exp c - 0)
rw [sub_zero]