## Stream: new members

#### Antoine Labelle (Nov 25 2020 at 21:30):

Hi! I'm currently learning lean and I'm trying to figure out what is the problem with this tactic

have h₀ : 0 < 1 + exp a,


Lean says

type mismatch at application
term
zero_lt_one
has type
0 < 1
but is expected to have type
0 < ?m_3


What does that mean?

#### Kevin Buzzard (Nov 25 2020 at 21:31):

Can you post a #mwe, i.e. fully working code that we can just cut and paste?

#### Kevin Buzzard (Nov 25 2020 at 21:32):

oh -- you could try exact add_pos zero_lt_one exp_pos,, that might do it.

#### Antoine Labelle (Nov 25 2020 at 21:34):

Thanks, exact works with (exp_pos a) instead of exp_pos. What was the problem with apply?

#### Kevin Buzzard (Nov 25 2020 at 21:35):

Using exact is being a bit more friendly towards the unifier, saying "this is the whole proof". apply is supposed to guess a lot more about what's going on.

Ok, thanks!

#### Kevin Buzzard (Nov 25 2020 at 21:36):

apply isn't really the correct tactic to use here -- if h : P -> Q then apply h turns a goal of Q into a goal of P. That's apply's job. That's not what is happening in your proof.

#### Kevin Buzzard (Nov 25 2020 at 21:36):

You're writing down the exact proof term here, so exact is the tactic to use. But apply does sometimes work in this situation, it's just a bit more hit-and-miss :-)

Last updated: May 18 2021 at 16:25 UTC