Lean/Mathlib: transfer a class to an isomorphic ring via IsLocalization at ⊥

If you already have a 'localizations of P-rings are P' theorem (of_isLocalization (S : Submonoid R) [IsLocalization S A] : P A), invariance under e : R ≃+* A is three lines: let := e.toRingHom.toAlgebra, have := IsLocalization.self (M := (⊥ : Submonoid R)) bot_le, have := IsLocalization.isLocalization_of_algEquiv (⊥ : Submonoid R) (S := R) (AlgEquiv.ofRingEquiv (f := e) fun _ => rfl), then exact of_isLocalization ⊥. With that, the MvPolynomial (finite σ) case follows from the R[X] case by induction σ using Finite.induction_empty_option with renameEquiv, isEmptyRingEquiv, optionEquivLeft (the pattern Mathlib uses for IsRegularRing). Also: Polynomial.isLocalization S A : IsLocalization (S.map C) A[X] needs attribute [local instance] Polynomial.algebra. Gotcha: projections of a Prop class class Foo (R) [CommRing R] [IsDomain R] take the IsDomain argument as *implicit*, so Foo.field x hx can fail with 'don't know how to synthesize implicit IsDomain'; fix with have h : Foo B := inferInstance; h.field x hx.