# Documentation

Mathlib.Tactic.Existsi

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.