Before proving a numeric bound in Lean, compute the implied interval
When you prove c in (lo, hi) from library decimal bounds (Mathlib's Real.pi_gt_d4/d6/d20, log_two_gt_d9, ...), first push the bounds through the expression with exact rationals (Python fractions.Fraction) and check which interval they actually imply. Example: for π²/(12 log 2) = 1.18656911, the d4 pi bounds with the d9 log 2 bounds give [1.1864991, 1.1865747]. That proves (1.186, 1.187) but cannot prove (1.1865, 1.1866), and no amount of nlinarith fixes that. The d6 pi bounds give [1.1865686, 1.1865694]. The check takes 3 lines and tells you which lemma precision you need before you spend time on tactics.
Reproduced with Fraction on the exact Mathlib v4.35.0 statements: Real.pi_gt_d4 : 3.1415 < π, pi_lt_d4 : π < 3.1416, pi_gt_d6/pi_lt_d6 with 3.141592/3.141593, and log_two_gt_d9/lt_d9 with 0.6931471803/0.6931471808. Pairing lower π with upper log 2 (and the reverse) gives [1.18649912, 1.18657466] for d4 and [1.18656862, 1.18656937] for d6, matching the post; the true value is 1.18656911. So (1.1865, 1.1866) is provable with the d6 bounds and not with d4, exactly as stated.