filterUpwards — Mathlib

Lean4
/-- `filter_upwards [h₁, ⋯, hₙ]` replaces a goal of the form `s ∈ f` and terms
`h₁ : t₁ ∈ f, ⋯, hₙ : tₙ ∈ f` with `∀ x, x ∈ t₁ → ⋯ → x ∈ tₙ → x ∈ s`.
The list is an optional parameter, `[]` being its default value.

`filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ` is a short form for
`{ filter_upwards [h₁, ⋯, hₙ], intro a₁ a₂ ⋯ aₖ }`.

`filter_upwards [h₁, ⋯, hₙ] using e` is a short form for
`{ filter_upwards [h1, ⋯, hn], exact e }`.

Combining both shortcuts is done by writing `filter_upwards [h₁, ⋯, hₙ] with a₁ a₂ ⋯ aₖ using e`.
Note that in this case, the `aᵢ` terms can be used in `e`.
-/
@[tactic_parser 1000]
public meta def filterUpwards : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.filterUpwards 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "filter_upwards" false✝)
          (ParserDescr.unary✝ `optional
            (ParserDescr.binary✝ `andthen
              (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " [")
                ((with_annotate_term"sepBy(" @ParserDescr.sepBy✝) (ParserDescr.cat✝ `term 0) ","
                  (ParserDescr.symbol✝ ", ") Bool.false✝))
              (ParserDescr.symbol✝ "]"))))
        (ParserDescr.unary✝ `optional
          (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " with")
            (ParserDescr.unary✝ `many
              (ParserDescr.binary✝ `andthen
                (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `colGt))
                (ParserDescr.cat✝ `term 1024))))))
      (ParserDescr.unary✝ `optional
        (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " using ") (ParserDescr.cat✝ `term 0))))
Похожие утверждения