Mertens.M_eq_summand_bound

lemma M_eq_summand_bound (n : ℕ) :    |M_eq_summand n| ≤ 2 / n ^ 2 := by  unfold M_eq_summand  split_ifs with h  · trans 1 / n ^ 2 / (1 - 1 / n)    · convert abs_log_sub_add_sum_range_le (x := 1 / n) _ 1 using 1      · rw [add_comm]        simp      · rw [abs_of_nonneg (by simp)]        ring      · simpa using inv_lt_one_of_one_lt₀ (mod_cast h.one_lt)    rw [(by ring : (2 : ℝ) / n ^ 2 = 1 / n ^ 2 / (1 / 2))]    gcongr    suffices (1 : ℝ) / n ≤ 1 / 2 by linarith    gcongr    exact_mod_cast h.two_le  · rw [abs_zero]    positivity