Take a hypothesis apart
obtain ⟨hp, hq⟩ := h unpacks a conjunction so you can use both halves.
In this course 7 / 13
If h : P ∧ Q is a pair, you should be able to open it. obtain ⟨hp, hq⟩ := h does that: h leaves the context and hp : P and hq : Q arrive in its place. The brackets ⟨ ⟩ are typed \< and \>, and they are Lean’s notation for taking apart, or building, something with several components. Nested pairs open in one step: obtain ⟨hp, hq, hr⟩ := h when h : P ∧ Q ∧ R.
The same brackets build. When hq : Q and hp : P, the term ⟨hq, hp⟩ is a proof of Q ∧ P, so exact with such a pair proves a conjunction with no constructor at all. Reading this notation in both directions pays off: it comes back for ↔, for ∃, and for every structure you define.
You can also reach into a pair without unpacking it. h.1 is the left component and h.2 the right one.
The tactic version shows each intermediate goal; the term version is shorter. Neither is more correct. Pick the one that will be easier to read when you come back to the proof.
Worked example
example (A B : Prop) (h : A ∧ (A → B)) : B := by
obtain ⟨ha, hab⟩ := h
exact hab haHere the two halves have different jobs: one is an argument and the other is the function it goes into. Your exercise keeps both halves as they are and only swaps their order.
⟨ ⟩ takes conjunctions apart with obtain and builds them as terms. h.1 and h.2 reach in without unpacking.
Swap the two halves of h to prove Q ∧ P.
Suggested steps
- Open h into its two components
- Build the swapped pair
These marks only recognize text. Another correct proof may use different steps; Lean checks whether it works.
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
Knowledge check
Answer without looking back, then check your reasoning.
correct