simple proof - but warning in infoview "expected type"

Stream: new members

[rzeta0]

As far as I can tell the following proof is very simple and uncontroversial.

-- 12 - Using Lemmas: Not Equal from Less Than

import Mathlib.Tactic

example {n : ℕ} (h: n = 1): n ≠ 5 := by
  apply ne_of_lt
  calc
    n = 1 := by rw [h]
    _ < 5 := by norm_num

But placing the curser after apply ne_of_lt shows what I think is a warning:

Expected type
n : ℕ
h : n = 1
⊢ ∀ {α : Type} [inst : Preorder α] {a b : α}, a < b → a ≠ b

What does this mean?

[Daniel Weber]

It's not a warning - that's the type of ne_of_lt, and it means that if you want to provide the argument to it directly (instead of letting apply add it as a goal) that's the type it should have

[rzeta0]

To better understand your answer I think I need to know what "provide the arguments to it directly" means.

Can you illustrate?

[Kyle Miller]

Put your cursor right before, say, n in h : n = 1. You'll see the "expected type" info showing that Nat is expected there. Everything's fine, since n is a Nat.