case this
y : ℝ
⊢ Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))

y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
⊢ Tendsto (fun x => log (x + y) - log x) atTop (𝓝 0)
y : ℝ
⊢ Tendsto (fun x => log (x + y) - log x) atTop (𝓝 0)
have : Tendsto (fun x ↦ 1 + y / x) atTop (𝓝 (1 + 0))
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
⊢ Tendsto (exp ∘ fun x => log (x + y) - log x) atTop (𝓝 (1 + 0))
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
⊢ Tendsto (fun x => log (x + y) - log x) atTop (𝓝 0)
rw [← comap_exp_nhds_exp, exp_zero, tendsto_comap_iff, ← add_zero (1 : ℝ)]
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
⊢ (fun x => 1 + y / x) =ᶠ[atTop] exp ∘ fun x => log (x + y) - log x
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
⊢ Tendsto (exp ∘ fun x => log (x + y) - log x) atTop (𝓝 (1 + 0))
refine' this.congr' _
case h
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 1 + y / x = (exp ∘ fun x => log (x + y) - log x) x
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
⊢ (fun x => 1 + y / x) =ᶠ[atTop] exp ∘ fun x => log (x + y) - log x
filter_upwards [eventually_gt_atTop (0 : ℝ), eventually_gt_atTop (-y)] with x hx₀ hxy
no goals
case h
y : ℝ
this : Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
x : ℝ
hx₀ : 0 < x
hxy : -y < x
⊢ 1 + y / x = (exp ∘ fun x => log (x + y) - log x) x
rw [comp_apply, exp_sub, exp_log, exp_log, one_add_div] <;> linarith
no goals
case this
y : ℝ
⊢ Tendsto (fun x => 1 + y / x) atTop (𝓝 (1 + 0))
exact tendsto_const_nhds.add (tendsto_const_nhds.div_atTop tendsto_id)