Inf troubles

Stream: new members

[Pim Otte]

Couple of questions about the sample below:

Why doesn't apply work as-is? I get "failed to unify", but the shape seems perfectly fine.
For the @-variant: It fails to synthesize the complete_semilattice_Inf ℕ, as I understand it, N should be one, but I'm not sure how to get that, or how to find it. Any pointers?:)

import data.mv_polynomial.basic

noncomputable theory
open_locale big_operators

example : (Inf ({n : ℕ | n ≥ 5} : set ℕ)) ≤ 5 :=
begin
    apply Inf_le,
    -- apply @Inf_le ℕ _ ({n : ℕ | n ≥ 5} : set ℕ) 5,
end

[Eric Rodriguez]

docs#cInf_le is what you need to use for nat

[Eric Rodriguez]

nat does not form a docs#complete_semilattice_inf (equivalent to a docs#complete_lattice, which requires a top element)

[Eric Rodriguez]

"c" stands for conditional, and this is because Inf {} = 0, not a hypothetical "top" element as should be required

[Pim Otte]

I see, thanks a lot!

[Anatole Dedecker]

Maybe this is solved in Lean4, but would there be a way to tell when the failure of unification is cause by lack of instances and fall back to the « failed to synthesize type class instance » error message ? Although I guess it would be pretty hard because in this case the error comes before searching for a complete lattice instance, it fails because the theorem is about inf coming from complete lattice and you want to apply it to the one coming from conditionally complete lattice, right ?