Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+ā†‘Ctrl+ā†“to navigate, Ctrl+šŸ–±ļøto focus. On Mac, use Cmdinstead of Ctrl.
Copyright (c) 2022 Arthur Paulino. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Arthur Paulino, Gabriel Ebner

import Lean

Defines the `use` tactic.

TODO: This does not match the full functionality of `use` from mathlib3.
See failing tests in `test/Use.lean`.

open Lean.Elab.Tactic

namespace Mathlib.Tactic

`use eā‚, eā‚‚, ā‹Æ` applies the tactic `refine āŸØeā‚, eā‚‚, ā‹Æ, ?_āŸ©` and then tries
to close the goal with `with_reducible rfl` (which may or may not close it). It's
useful, for example, to advance on existential goals, for which terms as
well as proofs of some claims about them are expected.


example : āˆƒ x : Nat, x = x := by use 42

example : āˆƒ x : Nat, āˆƒ y : Nat, x = y := by use 42, 42

example : āˆƒ x : String Ɨ String, x.1 = x.2 := by use ("forty-two", "forty-two")
-- TODO extend examples in doc-string once mathlib3 parity is achieved.
macro "use " 
es: ?m.96
:term,+ : tactic => `(tactic|(refine āŸØ$
es: ?m.96
,*, ?_āŸ©; try with_reducible rfl))