Question about the tactic "obtain"

Question

I am having difficulty activating the tactic obtain. Is it part of mathlib and where is its exact location?

Answer 1

Assuming you are on Lean 3, the best way to answer these sort of questions is via the mathlib tactic documentation (which also documents the built in tactics in core Lean).

If you look at obtain and select "Import using" you will see that either of these import commands work:

• import tactic.rcases (the specific location of the tactic)
• import tactic.basic (a curated import of common tactics)

Similarly, import tactic also works (which I think is the same as import tactic.basic but I could be mistaken).

As for whether it is in mathlib, the answer is yes, and can be found by selecting "Related declarations" to see the definition of obtain, tactic.interactive.obtain. If you click on the source you see it is in mathlib. This means you need mathlib to use it, but most Lean 3 projects require mathlib and it is easy to add to your project.

Here is an example.

import tactic

example (p q : Prop) (h : true -> p ∧ q) : p :=
begin
  obtain ⟨hp, hq⟩  : p ∧ q,
    apply h,
    trivial,
  assumption
end