Can I shadow/specify instance to use in def?

Stream: lean4

[Zhuanhao Wu]

In the example, I want to shadow the default LT Nat instance with my sampleInst (i: Info). The catch here is that this instance is dependent on some extra info i, and I'm not sure if default_instance is appropriate.
One thing I tried is useInst, but to use it I have to do the @useInst to pass the instance in the first example.

Is there someway I could achieve the syntax of the second example, but still get sampleInst as LT when defining useInst'?

import Mathlib

structure Info where
  s: Nat

instance sampleInst (i: Info) : LT Nat where
  lt x y := x + y = i.s


def useInst [inst: LT Nat] : Prop :=
  ∀(x y: Nat), x < y

-- usage:
example (I: Info): (@useInst (sampleInst I)) := sorry

-- What I want to achieve

def useInst' (I: Info)  : Prop := -- some magic code here or in the `def` to make this def use (sampleInst I) as the LT instance for x and y?
  ∀(x y: Nat), x < y

example (I: Info): (useInst' I) := by sorry -- or some magic here?

[Kyle Miller]

You can use explicit binders (def useInst (inst: LT Nat)) and it will use inst inside the body of the function.

You can also write

example (I: Info) : letI inst := sampleInst i; ∀(x y: Nat), x < y := sorry

The I in letI means "inline" — it will substitute in sampleInst i wherever inst is used. If you use let, then it will keep a let expression around.

[Zhuanhao Wu]

Thanks, this works!