The existsi tactic

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

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

existsi e₁, e₂, ⋯ instantiates existential quantifiers in the main goal by using e₁, e₂, ... as witnesses. existsi e₁, e₂, ⋯ is equivalent to refine ⟨e₁, e₂, ⋯, ?_⟩.

See also exists: exists e₁, e₂, ⋯ is equivalent to existsi e₁, e₂, ⋯; try trivial.

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.