t : ℝ
h₁ : Tendsto (fun h => h⁻¹ * log (1 + t * h)) (𝓝[{0}ᶜ] 0) (𝓝 t)
⊢ Tendsto (fun x => x * log (1 + t / x)) atTop (𝓝 t)
t : ℝ
⊢ Tendsto (fun x => x * log (1 + t / x)) atTop (𝓝 t)
have h₁ : Tendsto (fun h => h⁻¹ * log (1 + t * h)) (𝓝[≠] 0) (𝓝 t) := by
  simpa [hasDerivAt_iff_tendsto_slope, slope_fun_def] using
    (((hasDerivAt_id (0 : ℝ)).const_mul t).const_add 1).log (by simp)
t : ℝ
h₁ : Tendsto (fun h => h⁻¹ * log (1 + t * h)) (𝓝[{0}ᶜ] 0) (𝓝 t)
h₂ : Tendsto (fun x => x⁻¹) atTop (𝓝[{0}ᶜ] 0)
⊢ Tendsto (fun x => x * log (1 + t / x)) atTop (𝓝 t)
t : ℝ
h₁ : Tendsto (fun h => h⁻¹ * log (1 + t * h)) (𝓝[{0}ᶜ] 0) (𝓝 t)
⊢ Tendsto (fun x => x * log (1 + t / x)) atTop (𝓝 t)
have h₂ : Tendsto (fun x : ℝ => x⁻¹) atTop (𝓝[≠] 0) :=
  tendsto_inv_atTop_zero'.mono_right (nhdsWithin_mono _ fun x hx => (Set.mem_Ioi.mp hx).ne')
no goals
t : ℝ
⊢ Tendsto (fun h => h⁻¹ * log (1 + t * h)) (𝓝[{0}ᶜ] 0) (𝓝 t)
simpa [hasDerivAt_iff_tendsto_slope, slope_fun_def] using
  (((hasDerivAt_id (0 : ℝ)).const_mul t).const_add 1).log (by simp)
no goals
t : ℝ
⊢ 1 + t * id 0 ≠ 0
simp