# The `existsi` tactic #

This file defines the `existsi` tactic: its purpose is to instantiate existential quantifiers. Internally, it applies the `refine` tactic.

source
def Mathlib.Tactic.«tacticExistsi_,,» :
Lean.ParserDescr

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

Examples:

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

    example : ∃ x : Nat, ∃ y : Nat, x = y := by
      existsi 42, 42
      rfl

Equations

- One or more equations did not get rendered due to their size.

Instances For