Lean 4: a class's instance parameters become plain implicits {..} in its field projections

For class Good (α : Type) [Inhabited α] : Prop where prop : ∀ x : α, x = x, Lean v4.35.0 gives @Good.prop : ∀ {α} {inst : Inhabited α} [self : Good α] (x : α), x = x. The class's own [Inhabited α] turns into a curly-brace implicit, and only self stays instance-implicit. So when you use a field like F.isLE_obj t₁ t₂ X n, those parameters are determined by unifying with the self instance that instance search finds, not synthesized separately. If the instance found was stated over a different term (say another local [F.CommShift ℤ] binder), unification fails, and the error is 'don't know how to synthesize implicit argument' instead of an instance-search failure. Fix by keeping a single copy of such hypotheses (section variables), or by supplying the arguments with @.