Question about Nat.le.refl

Stream: new members

[Adam Kurkiewicz]

I'm trying to show that k ≤ k + 2.

My strategy is to first use Nat.le.refl and then use Nat.le.step twice.

But somehow I can't get anything involving Nat.le.refl to work.

For example, the simplest:

#eval (@Nat.le.refl (4: ℕ))

Gives me:

invalid universe level, 0 is not greater than 0Lean 4
Nat.le.refl {n : ℕ} : Nat.le n n
Less-equal is reflexive: n ≤ n

import Init.Prelude

No quick fixes available

Does anybody know what I'm doing wrong?

[Adam Kurkiewicz]

Ha, interesting, this seems to work:

theorem k_le_k_add_2 (k : ℕ) : k ≤ k + 2 :=
  Nat.le.step (Nat.le.step (@Nat.le.refl k))

[Ruben Van de Velde]

Yeah, the issue is with #eval - what would it mean to evaluate a term like that? #check (@Nat.le.refl (4: Nat)) also works

[Adam Kurkiewicz]

Ah makes sense. I just misremembered how this works. I think I got thrown off by the implicit k, and then got entangled in the #eval thing. Thank you!