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 Mathlib.Tactic
example : ∃ (a b : ℝ), a + b = 37 := by
use 5, 32
-- ⊢ 5 + 32 = 37
norm_num
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”.