existsi

The existsi tactic makes progress with goals of the form ∃ x : X, P x. With this as the goal, and with t : X in the local context, the tactic existsi t will change the goal to P t.

Example

try it!

example : ∃ n : ℕ, 2 + 2 = n :=
begin
  existsi 4,
  -- goal now 2 + 2 = 4
refl
end

Note that existsi can be quite dense about types – you might have to explicitly tell it the type of the term you are trying to use. if you have mathlib installed, then the use tactic is slightly more user-friendly.

try it!

import tactic.interactive -- for use tactic
import data.real.basic -- for real numbers

example : ∃ n : ℝ, n + 3 = 3 + 7 :=
begin
  -- existsi 7, -- fails
  -- existsi (7 : ℝ), -- works
  use 7, -- works
  -- goal now 7 + 3 = 3 + 7
  apply add_comm, -- commutativity of addition closes the goal
end