refactor(data/real/pi): add tactics for pi computation (#2641)
refactor(data/real/pi): add tactics for pi computation (#2641)

Depends on #2589. Moves pi bounds from @fpvandoorn's gist to mathlib, and also adds a small tactic to uniformize the proofs (and also skip some unsqueezed proofs), making the compilation even faster (just around 1 second for the longest proofs).



leanprover-community/mathlib,leanprover-community/mathlib