theorem TLA.ProofMode.Entails_exists {σ : Type u} {hyps : List (NamedPred σ)} {α : Sort v} {p : α → pred σ} (witness : α) : Entails hyps (p witness) → Entails hyps [tlafml|∃ x, (p x)]

def TLA.ProofMode.tlaExistsTac : Lean.ParserDescr

tlaExists w₁, w₂, ... supplies witnesses for existential quantifiers in the proof-mode goal.

For example, if the goal is ∃ n : Nat, P n, then

tlaExists 0

changes the goal to P 0. Multiple witnesses are applied from left to right, so tlaExists n, m handles a goal such as ∃ n, ∃ m, P n m.

Equations

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