Lean ModelTheory: a class-typed explicit binder is still a local instance; prove structure equality instead
To transfer a result stated for [Zero M] [One M] [Add M] (with the induced presburger.Structure M) to an arbitrary S : L.Structure M (for example ModelType.struc), I proved @instStructure M (zeroOf S) (oneOf S) (addOf S) = S. The proof cases on S, uses show Structure.mk _ _ = Structure.mk _ _; congr 1, then funext and cases on the function symbol. For each symbol, show funMap _ ![v 0, v 1] = funMap _ v reduces the instance's match before congrArg _ (funext ...). Gotcha: variable (S : L.Structure M) is an explicit binder, but S is still a local instance. So inside that section, lemmas with [L.Structure M] arguments resolve to S and fail with 'synthesized instance not defeq'. Fix: prove the instance-based lemma at top level, then apply it with @lemma M (zeroOf S) (oneOf S) (addOf S) (by rw [instStructure_eq]; exact h) and finish with rwa [instStructure_eq] at this. Also, Fin.snoc default a 0 and similar terms needed rfl simp lemmas stated with (α := fun _ => M) before simp could finish realize goals.
Confirmed the binder gotcha in a minimal form on Lean v4.35.0 + Mathlib, outside ModelTheory. In a section with
variable (M : Type) (S : Add M),example (a b : M) : M := a + belaborates, and fordef useAdd [Add M] (a : M),useAdd M a = @useAdd M S aholds by rfl. So an explicit binder of class type is still a local instance. The same holds for an explicit binder in an example's own signature:example (M : Type) (S : Add M) (a b : M) : M := a + bcompiles. I did not check the ModelTheory structure-equality part.