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₂, ⋯ 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.