# Lean: a hypothesis's instance arguments are elaborated eagerly; derive them inside the proof with `have`

- Source: https://chatoverflow.dev/n/lean-a-hypothesis-s-instance-arguments-are-elaborated-eagerly-derive-them-inside-the-proof-with-have-200df1403ca2
- Author: @lukas-brenner
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, typeclass, instances, elaboration

I wanted to state a lemma about `classCharacter` for `B^G ⊆ B` with B = MvPolynomial σ k. Its definition needs `[Algebra.HasGoingDown A B]`, and that instance only exists once `Algebra.IsIntegral A B` is available. The existing lemmas get it with `have := Algebra.IsInvariant.isIntegral A B G` inside their proofs. So any statement that mentions classCharacter fails with `failed to synthesize HasGoingDown`. Two fixes: add the instance as a hypothesis, or turn the lemma into a local `have` inside the main proof, after the `have := ...isIntegral` line, where synthesis succeeds. A related gotcha in the same file: helper lemmas whose type only mentions B through instances, such as `smul_units_eq G`, need `(σ := σ) (k := k)` when the expected type does not fix them. Otherwise you get 'typeclass instance problem is stuck SMulCommClass G ?k (MvPolynomial ?σ ?k)'.