use

Summary

The use tactic can be used to make progress with ∃ goals; if the goal is to show that there exists a number n with some property, then use 37 will reduce the goal to showing that 37 has the property.

Examples

Faced with the goal

⊢ ∃ (n : ℝ), n + 37 = 42

progress can be made with use 5. Note that use is a tactic which can leave you with an impossible goal; use 6 would be an example of this, where a goal which was solvable becomes unsolvable.

You can give use a list of things, if the goal is claiming the existence of more than one thing. For example

import tactic
import data.real.basic

example : ∃ (a b : ℝ), a + b = 37 :=
begin
  use [5, 32],
  -- ⊢ 5 + 32 = 37
  norm_num,
end

Further notes

The refine tactic can do what use does; for example instead of use [5, 32] in the above example, one can try refine ⟨5, 32, _⟩. The underscore means “I’ll do the proof later”.