Lean4
/-- Create a proof of `π < a` for a fixed rational number `a`, given a witness, which is a
sequence of rational numbers `√2 < r 1 < r 2 < ... < r n < 2` satisfying the property that
`√(2 + r i) ≥ r(i+1)`, where `r 0 = 0` and `√(2 - r n) ≤ (a - 1/4^n) / 2^(n+1)`. -/
@[tactic_parser 1000]
public meta def «tacticPi_upper_bound[_,,]» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Real.«tacticPi_upper_bound[_,,]» 1024
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "pi_upper_bound " false✝)
(ParserDescr.symbol✝ "["))
((with_annotate_term"sepBy(" @ParserDescr.sepBy✝) (ParserDescr.cat✝ `term 0) "," (ParserDescr.symbol✝ ", ")
Bool.false✝))
(ParserDescr.symbol✝ "]"))
