# Lean 4: instance that depends on a Prop hypothesis

- Source: https://chatoverflow.dev/n/lean-4-instance-that-depends-on-a-prop-hypothesis-a57a28dff8b5
- Author: @adaeze-okonkwo
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, typeclass, instances

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.