Symptom

NumberField.InfiniteAdeleRing is a pi-type synonym

def InfiniteAdeleRing (K : Type*) [Field K] := (v : InfinitePlace K) → v.Completion
deriving CommRing, Inhabited, TopologicalSpace, IsTopologicalRing, Algebra K

deriving emits machine-generated auxiliary field definitions (…_aux_1, …_aux_13, …) for the structure fields. Downstream (e.g. ImperialCollegeLondon/FLT), instance-implicit unification then has to prove goals like

f i * g i =?= instCommRingInfiniteAdeleRing._aux_13 K f g i
f i + g i =?= instCommRingInfiniteAdeleRing._aux_1 K f g i

which fail at instances transparency (backward.isDefEq.respectTransparency := true, the default since Lean v4.29), because those _aux_* definitions are not reducible there. Tagging individual aux names @[implicit_reducible] is not viable (unstable names; fixing one shifts the failure). See FLT#1132 / FLT#889 for traces and the remaining local set_option workaround.

What does not work / is undesirable

Proposed fix

Keep the semi-reducible def (so the custom product Norm stays the only norm API), drop deriving, and install only the algebraic/topological instances via transparent pi re-export:

instance : CommRing (InfiniteAdeleRing K) :=
  show CommRing ((v : InfinitePlace K) → v.Completion) from inferInstance
-- same pattern for Inhabited, TopologicalSpace, IsTopologicalRing, Algebra

#print then shows have this := inferInstance; this (no _aux_*). MetaM canary on (f * g) i vs f i * g i for InfiniteAdeleRing ℚ: instances: true.

PR

#42130

(Earlier #42120 used a similar instance shape but without the norm-boundary rationale and was closed; #42130 keeps def and documents why not abbrev.)