-- Mathlib/NumberTheory/Harmonic/EulerMascheroni.lean
lemma tendsto_eulerMascheroniSeq' :
    Tendsto eulerMascheroniSeq' atTop (𝓝 eulerMascheroniConstant)

Proof state:
case h
this : Tendsto (fun x => log (x + 1) - log x) atTop (𝓝 0)
n : ℕ
hn : n ≠ 0
⊢ ((fun x => log (x + 1) - log x) ∘ Nat.cast) n = eulerMascheroniSeq' n - eulerMascheroniSeq n

Tactic:
simp [eulerMascheroniSeq, eulerMascheroniSeq', eq_false_intro hn]

Result:
no goals

Proof state:
this : Tendsto (fun x => log (1 + 1 / x)) atTop (𝓝 0)
x : ℝ
hx : 0 < x
⊢ x ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
case h
this : Tendsto (fun x => log (1 + 1 / x)) atTop (𝓝 0)
x : ℝ
hx : 0 < x
⊢ log (1 + 1 / x) = log (x + 1) - log x

Tactic:
rw [← log_div (by positivity) (by positivity), add_div, div_self hx.ne']

Result:
no goals

Proof state:
⊢ Tendsto (fun x => log (x + 1) - log x) atTop (𝓝 0)

Tactic:
suffices Tendsto (fun x : ℝ ↦ log (1 + 1 / x)) atTop (𝓝 0) by
  apply this.congr'
  filter_upwards [eventually_gt_atTop 0] with x hx
  rw [← log_div (by positivity) (by positivity), add_div, div_self hx.ne']

Result:
⊢ Tendsto (fun x => log (1 + 1 / x)) atTop (𝓝 0)

Proof state:
⊢ Tendsto eulerMascheroniSeq' atTop (𝓝 eulerMascheroniConstant)

Tactic:
suffices Tendsto (fun n ↦ eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0) by
  simpa using this.add tendsto_eulerMascheroniSeq

Result:
⊢ Tendsto (fun n => eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0)

Proof state:
this : Tendsto (fun x => log (x + 1) - log x) atTop (𝓝 0)
⊢ (fun x => log (x + 1) - log x) ∘ Nat.cast =ᶠ[atTop] fun n => eulerMascheroniSeq' n - eulerMascheroniSeq n

Tactic:
filter_upwards [eventually_ne_atTop 0] with n hn

Result:
case h
this : Tendsto (fun x => log (x + 1) - log x) atTop (𝓝 0)
n : ℕ
hn : n ≠ 0
⊢ ((fun x => log (x + 1) - log x) ∘ Nat.cast) n = eulerMascheroniSeq' n - eulerMascheroniSeq n

Proof state:
this : Tendsto (fun x => log (1 + 1 / x)) atTop (𝓝 0)
⊢ (fun x => log (1 + 1 / x)) =ᶠ[atTop] fun x => log (x + 1) - log x

Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx

Result:
case h
this : Tendsto (fun x => log (1 + 1 / x)) atTop (𝓝 0)
x : ℝ
hx : 0 < x
⊢ log (1 + 1 / x) = log (x + 1) - log x

Proof state:
⊢ Tendsto (fun x => log (1 + 1 / x)) atTop (𝓝 0)

Tactic:
simpa only [add_zero, log_one] using
  ((tendsto_const_nhds.div_atTop tendsto_id).const_add 1).log (by positivity)

Result:
no goals

Proof state:
this : Tendsto (fun x => log (1 + 1 / x)) atTop (𝓝 0)
⊢ Tendsto (fun x => log (x + 1) - log x) atTop (𝓝 0)

Tactic:
apply this.congr'

Result:
this : Tendsto (fun x => log (1 + 1 / x)) atTop (𝓝 0)
⊢ (fun x => log (1 + 1 / x)) =ᶠ[atTop] fun x => log (x + 1) - log x

Proof state:
this : Tendsto (fun x => log (x + 1) - log x) atTop (𝓝 0)
⊢ Tendsto (fun n => eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0)

Tactic:
apply (this.comp tendsto_natCast_atTop_atTop).congr'

Result:
this : Tendsto (fun x => log (x + 1) - log x) atTop (𝓝 0)
⊢ (fun x => log (x + 1) - log x) ∘ Nat.cast =ᶠ[atTop] fun n => eulerMascheroniSeq' n - eulerMascheroniSeq n

Proof state:
⊢ 1 + 0 ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
this : Tendsto (fun x => log (1 + 1 / x)) atTop (𝓝 0)
x : ℝ
hx : 0 < x
⊢ x + 1 ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
this : Tendsto (fun n => eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0)
⊢ Tendsto eulerMascheroniSeq' atTop (𝓝 eulerMascheroniConstant)

Tactic:
simpa using this.add tendsto_eulerMascheroniSeq

Result:
no goals

Proof state:
⊢ Tendsto (fun n => eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0)

Tactic:
suffices Tendsto (fun x : ℝ ↦ log (x + 1) - log x) atTop (𝓝 0) by
  apply (this.comp tendsto_natCast_atTop_atTop).congr'
  filter_upwards [eventually_ne_atTop 0] with n hn
  simp [eulerMascheroniSeq, eulerMascheroniSeq', eq_false_intro hn]

Result:
⊢ Tendsto (fun x => log (x + 1) - log x) atTop (𝓝 0)