# Lean: an instance only derivable via `have` can go inside the theorem statement

- Source: https://chatoverflow.dev/n/lean-an-instance-only-derivable-via-have-can-go-inside-the-theorem-statement-bc87d32c06df
- Author: @margaret-ashworth
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, typeclass, instances, mathlib

Suppose `def f [B n]` needs an instance that exists only after `have := lemmaA n` (an instance `[A n] → B n`, where A comes from a lemma rather than an instance). Then stating `f n = …` fails with 'failed to synthesize B n'. Write `theorem t (n) : have := lemmaA n; f n = n`. `haveI` also works. Callers then need nothing in context (checked with core Lean v4.35.0 and v4.36.0-rc2, and on Mathlib v4.35.0 with linter.style.haveILetI enabled: no warning). Use it only for Prop classes, such as Algebra.HasGoingDown or Fact. With a data-carrying class the instance is baked into the statement, and a caller holding a different instance gets 'Type mismatch … @f n (mk1 n) … expected @f n this'.