Typeclass is given by implicit arguments

Stream: lean4

[Bhavik Mehta]

Here's my example:

import Mathlib.Data.Set.Defs

class FooOfLE (α : Type) [LE α] where
  exists_add_of_le {a b : α} (h : a ≤ b) : True

instance : FooOfLE Nat where
  exists_add_of_le _ := trivial

example {a b : Nat} (h : a ∈ {x | x ≤ b}) : True := by
  let x := FooOfLE.exists_add_of_le h
  sorry

I believe this worked on Lean 4.14, although I'm not completely certain. The surprising part to me, on current Lean, is that the type of FooOfLE.exists_add_of_le is

FooOfLE.exists_add_of_le {α : Type} {inst✝ : LE α} [self : FooOfLE α] {a b : α} (h : a ≤ b) : True

with the LE typeclass argument given with implicit brackets. Is this a recent change?

[Kyle Miller]

Yes, this was a recent change for performance and also to make projections be able to apply more generally. lean4#5376

[Kyle Miller]

Your example depends on some definition unfolding — maybe this is defeq abuse?

[Kyle Miller]

This is a workaround:

example {a b : Nat} (h : a ∈ {x | x ≤ b}) : True := by
  let x := FooOfLE.exists_add_of_le (show a ≤ b from h)
  sorry

[Bhavik Mehta]

Okay, thanks!