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.