rsuffices — Mathlib

Lean4
/-- The `rsuffices` tactic is an alternative version of `suffices`, that allows the usage
of any syntax that would be valid in an `obtain` block. This tactic just calls `obtain`
on the expression, and then `rotate_left`.
-/
@[tactic_parser 1000]
public meta def rsuffices : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.rsuffices 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "rsuffices" false✝)
          (ParserDescr.unary✝ `optional
            (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) Lean.Parser.Tactic.rcasesPatMed)))
        (ParserDescr.unary✝ `optional
          (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " : ") (ParserDescr.cat✝ `term 0))))
      (ParserDescr.unary✝ `optional
        (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " := ")
          ((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) (ParserDescr.cat✝ `term 0) "," (ParserDescr.symbol✝ ", ")
            Bool.false✝))))
Похожие утверждения