Use an equivalence
h.mp and h.mpr turn an iff into the direction you need.
In this course 6 / 11
From h : P ↔ Q you get two implications. h.mp : P → Q is the forward direction and h.mpr : Q → P is the reverse. They are the two components of the pair, and h.1 and h.2 name the same things.
Choosing the direction is the whole skill, and the goal tells you which one: you need the implication whose conclusion is the goal. If the goal is P, that is h.mpr, and it still needs a proof of Q.
Both styles work. exact h.mpr hq builds the term forwards. apply h.mpr leaves ⊢ Q to prove next. The worked example ends with rfl, because there the remaining goal is an equation rather than a hypothesis.
An ↔ is not itself a function, so h hq is a type error. You have to name a direction before you can apply anything.
Worked example
example (A : Prop) (h : A ↔ (2 + 2 = 4)) : A := by
apply h.mpr
rflAfter apply h.mpr the goal becomes ⊢ 2 + 2 = 4, which has nothing to do with A any more. Your exercise has two equivalences to travel through and uses both directions of each: forwards to reach R, and backwards to come home again.
h.mp and h.mpr are the two directions of h : P ↔ Q. Pick the one whose conclusion is your goal.
Travel through two equivalences, forwards and then backwards.
Suggested steps
- Step forwards through the first equivalence
- Reach R with the second
- Come back the other way for the implication
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