is nonminimal number not trivially positive?

Stream: lean4

[Stepan Holub]

Is it not strange that exact? fails on the following :

example (k l : ℕ) (h: ¬ k ≤ l) : 0 < k

[Aaron Liu]

This doesn't match any existing theorem, so I'm not surprised that exact? fails on this one.

example (k l : Nat) (h : ¬k ≤ l) : 0 < k := by
  apply Nat.zero_lt_of_lt
  exact Nat.lt_of_not_le h

[Stepan Holub]

Thanks.
What is the best way to find such a simple proof if exact fails?

[Kim Morrison]

If it's a linear arithmetic problem about nat and int, by omega

[Kim Morrison]

or try by hint