Can't get basic proof of transitivity of P -> Q to work out:

Stream: new members

[Daniel Donnelly]

example : (P → Q) → (Q → R) → (P → R) := by
  intro hPQ
  intro hQR
  intro hP
  apply (hPQ hP)

image.png

[Mario Carneiro]

hPQ hP is a proof of Q, you are trying to apply it when the goal is R

[Mario Carneiro]

(observe also that hQR is unused in this proof)

[Mario Carneiro]

if you meant to assert Q and add it to your context instead of trying to apply it to the goal, write

have hQ := hPQ hP

[Daniel Donnelly]

@Mario Carneiro With your help, I fixed it. Here it is:

example : (P → Q) → (Q → R) → (P → R) := by
  intro hPQ
  intro hQR
  intro hP
  have hQ := hPQ hP
  have hR := hQR hQ
  exact hR```

[Mario Carneiro]

A proof using apply works backwards from the end:

example : (P → Q) → (Q → R) → (P → R) := by
  intro hPQ
  intro hQR
  intro hP
  apply hQR
  apply hPQ
  exact hP

[Daniel Donnelly]

@Mario Carneiro I will try that proof out to make sure I understand apply