no goals
σ : Type u_1
R : Type u_3
S : Type u_2
T : Type ?u.997314
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f : R →+* S
g : S →+* T
s : σ
⊢ ↑(map σ f) (X s) = X s
simp [MvPowerSeries.X]