Documentation

Mathlib.Tactic.Use

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.