Defines the `use`

tactic.

TODO: This does not match the full functionality of `use`

from mathlib3.
See failing tests in `test/Use.lean`

.

`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.

Examples:

```
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")
∃ 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")
∃ x : Nat, ∃ y : Nat, x = y := by use 42, 42
example : ∃ x : String × String, x.1 = x.2 := by use ("forty-two", "forty-two")
∃ y : Nat, x = y := by use 42, 42
example : ∃ x : String × String, x.1 = x.2 := by use ("forty-two", "forty-two")
∃ x : String × String, x.1 = x.2 := by use ("forty-two", "forty-two")
× String, x.1 = x.2 := by use ("forty-two", "forty-two")
```

## Equations

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