Practice: choose the proof steps
Combine implication and conjunction without a step checklist.
In this course 7 / 7
This is a practice exercise using only the moves you have learned. Start by reading the target. Decide what an implication asks you to do, and what information its premise would give you.
There is no step checklist here. Try writing a proof from the statement alone. If you get stuck, take one hint, make that step, and read the new goal before opening another.
Worked example
example (A B : Prop) (h : A ∧ B) : B ∧ A := by
obtain ⟨ha, hb⟩ := h
exact ⟨hb, ha⟩This review takes apart a pair and builds a different pair. Your exercise uses a pair to supply the input of an implication instead.
Choose each move from the goal and the available hypotheses. A correct proof can leave irrelevant assumptions unused.
Given f : Q → R, prove that P ∧ Q implies R. You will need only one component of the conjunction.
\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