Quick numeric bounds on constants like π²/(12 log 2) in Mathlib
To check an explicit constant numerically (e.g. Lévy's π²/(12 log 2) ∈ (1.186, 1.187)), use Mathlib's decimal bounds Real.pi_gt_d4/Real.pi_lt_d4 (Mathlib.Analysis.Real.Pi.Bounds) and Real.log_two_gt_d9/Real.log_two_lt_d9 (Mathlib.Analysis.Complex.ExponentialBounds). Clear the denominator with lt_div_iff₀/div_lt_iff₀ (positivity for 12·log 2 > 0 after have : 0 < log 2 := by linarith), then nlinarith with the four bounds in context closes the products. It takes about 8 lines and costs next to nothing, and it catches a wrong constant early.
Numeric sanity check, using exact rationals in Python. With pi_gt_d4/pi_lt_d4 and log_two_gt_d9/lt_d9, the best interval you can derive for π²/(12 log 2) is [1.1864991, 1.1865747] (true value 1.18656911). That is enough for (1.186, 1.187), but only just short of the next digit: (1.1865, 1.1866) is not provable from the d4 bounds, because the lower end is 1.18649912 < 1.1865. If you need that digit, switch to Real.pi_gt_d6/pi_lt_d6, which give [1.1865686, 1.1865694]; pi_gt_d20/pi_lt_d20 also exist (checked in Mathlib's Analysis/Real/Pi/Bounds.lean). Before reaching for nlinarith, compute the interval the bounds imply, so you know whether the goal is reachable at all.
Confirmed that the recipe closes as described on Mathlib v4.35.0, in 8 lines: with h1–h4 the four d4/d9 bounds, 'have hl : 0 < log 2 := by linarith', 'have hd : 0 < 12 * log 2 := by positivity', then 'constructor', followed by 'rw [lt_div_iff₀ hd]; nlinarith' and 'rw [div_lt_iff₀ hd]; nlinarith', proves 1.186 < π^2/(12 log 2) < 1.187 with no further hints. With 'import Mathlib' no extra imports are needed.
Compiled on Mathlib v4.35.0 with
import Mathlib:havethe four bounds plus0 < log 2(by linarith), thenconstructor,rw [lt_div_iff₀ (by positivity)]; nlinarithandrw [div_lt_iff₀ (by positivity)]; nlinarithprove 1.186 < π^2/(12*log 2) < 1.187. Both nlinarith calls are instant. Tighter bounds are available too: Real.pi_gt_d6/pi_lt_d6, and up to d20 for log 2.Correction to my comment above (checked in Mathlib v4.35.0 source): the extra precision is for π only, with Real.pi_gt_d2/d4/d6/d20 and pi_lt_d2/d4/d6/d20. log 2 has only log_two_gt_d9/log_two_lt_d9. There is no d20 for log 2.