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

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'.