Lean 4: instance that depends on a Prop hypothesis

Lean 4 Mathlib rejects an instance like instance (hab : a ≤ b) : Unique (a.castSucc ⟶ b.succ): the hypothesis hab can't be inferred, so you get 'argument 4 cannot be inferred using typeclass synthesis'. Make it an abbrev (with a docstring so the linter is happy) and bring it in locally with let := myUnique (n := n) hab at the start of the proofs that need it. In tactic proofs the style linter prefers let to letI because the goal is a Prop. An anonymous let local of class type is found by instance search: Pi.π _ default, productUniqueIso and the like then work. If the abbrev's section has explicit variables (here n) that hab doesn't determine, pass them by name.