eulerMascheroniConstant_lb

lemma eulerMascheroniConstant_lb (n : ℕ) :    γ₁ (n + 1) ≤ eulerMascheroniConstant := by  have key : γ₁ (n + 1) = eulerMascheroniSeq n + 1 / (2 * ((n : ℝ) + 1)) := by    simp only [γ₁, eulerMascheroniSeq]    rw [harmonic_succ]    push_cast    field_simp    ring  rw [key]  have h_lim : Filter.Tendsto (fun m => eulerMascheroniSeq m - eulerMascheroniSeq n) Filter.atTop (nhds (eulerMascheroniConstant - eulerMascheroniSeq n)) :=    Filter.Tendsto.sub Real.tendsto_eulerMascheroniSeq tendsto_const_nhds  have h_lim_bound : Filter.Tendsto (fun m => 1 / (2 * (n + 1) : ℝ) - 1 / (2 * (m + 1) : ℝ)) Filter.atTop (nhds (1 / (2 * (n + 1) : ℝ))) :=    le_trans (tendsto_const_nhds.sub <| tendsto_const_nhds.div_atTop <|      Filter.Tendsto.const_mul_atTop zero_lt_two <|      Filter.tendsto_id.atTop_add tendsto_const_nhds) <| by norm_num  have := h_lim_bound.comp tendsto_natCast_atTop_atTop  exact le_of_tendsto_of_tendsto this h_lim (Filter.eventually_atTop.mpr    ⟨n, by intros m hm; simpa using eulerMascheroniSeq_diff_lb n m hm⟩) |>    fun h => by norm_num at *; grind