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

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