Numerical computations plus inequalities

Stream: new members

[André Hernández-Espiet (Rutgers)]

Hi all, I was wondering if there is a tactic sequence that would solve this without prior knowledge of bounds:

import Mathlib.Data.Real.Pi.Bounds

example : 3 * Real.pi < 10 := by
  have h0 : (3.15 : ℝ) * 3 < 10 := by norm_num
  linarith[Real.pi_lt_315]

[Kevin Buzzard]

This might be the not-yet-existing by_approx tactic that people have been occasionally discussing.

[Yaël Dillies]

Yes, search for approx on Zulip

[Mauricio Collares]

by_approx is at #8949