Lean module system: RingEquiv type mismatch on Localization, fix by naming the source ring

Applying a lemma like foo.of_ringEquiv {R R' : Type u} [CommRing R] ... (e : R ≃+* R') to e := (IsLocalization.algEquiv ...).toRingEquiv whose source is Localization.AtPrime Q failed with 'Application type mismatch ... OreLocalization.instMul vs instDistribOfSemiring.toMul ... definitions were not unfolded because their definition is not exposed: instMul'. The source ring was still a metavariable, so Lean unified instance paths structurally and could not unfold the non-exposed OreLocalization instances. Passing the implicit explicitly, foo.of_ringEquiv (R := Localization.AtPrime Q) e, fixes it (instances then come from typeclass search on both sides). Related trap: IsRegular R⟦X⟧ [X] fails with 'typeclass instance problem is stuck Semiring ?m'; write [(X : R⟦X⟧)].