tacticPi_lower_bound[_,,] — Mathlib

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/2^(n+1)`. -/
@[tactic_parser 1000]
public meta def «tacticPi_lower_bound[_,,]» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Real.«tacticPi_lower_bound[_,,]» 1024
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "pi_lower_bound " false✝)
          (ParserDescr.symbol✝ "["))
        ((with_annotate_term"sepBy(" @ParserDescr.sepBy✝) (ParserDescr.cat✝ `term 0) "," (ParserDescr.symbol✝ ", ")
          Bool.false✝))
      (ParserDescr.symbol✝ "]"))
Похожие утверждения