what is "have key := [...]" the backwards way

Stream: new members

[Mason McBride]

If I have (h : P -> Q) and (g : Q -> R) and (p : P) how do I make an r : R without using "have q := h p" "have r := g q"? I feel like it's apply but I always think I can do "apply succ_ne_zero at H"

[Julian Berman]

import tactic
example {P Q R : Prop} (h : P → Q) (g : Q → R) (p : P) : R := by library_search
 -- Try this: exact g (h p)

[Mason McBride]

I appreciate it. So what's the difference between exact and apply?

[Julian Berman]

exact basically is you saying "I want to solve the goal now, here's a term"

[Julian Berman]

apply is your arguing backwards, but you can't do it to a hypothesis, only to the goal

[Julian Berman]

You could instead do have hr := g (h p) which will give you a new hypothesis of type R -- but then once you have that hypothesis, now you do exact hr to close the goal.

[Jireh Loreaux]

If your goal is R, then you could also do refine g _ to end up with a goal of Q. refine is like exact except that you can give it holes (underscores), and any that it can't automatically fill it will create new goals for. So, for example, if your goal is R and foo : P → Q → R, then refine foo _ _ would give you two goals, namely P and Q.