Understanding `apply`

Stream: lean4

[Damiano Testa]

Dear All,

why do the following not work?

example : 0 < 1 := by
  apply Nat.succ_pos ?_

example : 0 < Nat.succ 0 := by
  apply Nat.succ_pos ?_

example {n : Nat} : 0 < Nat.succ n := by
  apply Nat.succ_pos ?_

They do work if you remove the ?_, if you replace it with _, or, of course, if you use exact.

I know that apply "does not use the expected type", but these examples are still unclear to me.

Thanks!

[Patrick Massot]

The ?_ explicitly ask Lean not to infer the corresponding term..

[Damiano Testa]

Ok, I'll try to come to terms with the fact that refine and exact both close the goals above. Thanks!