tacticExistsi_,, — Mathlib

Lean4
/-- `existsi e₁, e₂, ⋯` applies the tactic `refine ⟨e₁, e₂, ⋯, ?_⟩`. It's purpose is to instantiate
existential quantifiers.

Examples:

```lean
example : ∃ x : Nat, x = x := by
  existsi 42
  rfl

example : ∃ x : Nat, ∃ y : Nat, x = y := by
  existsi 42, 42
  rfl
```
-/
@[tactic_parser 1000]
public meta def «tacticExistsi_,,» : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.«tacticExistsi_,,» 1022
    (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "existsi " false✝)
      ((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) (ParserDescr.cat✝ `term 0) "," (ParserDescr.symbol✝ ", ")
        Bool.false✝))
Похожие утверждения