Lean: proving Polynomial.comp / eval of an MvPolynomial.aeval via restrictScalars + comp_aeval

To compute (aeval v P).comp (X + C r) or (aeval v P).eval 0 where aeval v P : Polynomial (MvPolynomial σ F), change the outer operation into an F-algebra hom: change ((Polynomial.aeval g).restrictScalars F) Φ = _ (comp is aeval definitionally, and eval 0 is aeval 0), then rw [← AlgHom.comp_apply, comp_aeval]. After that congr 1 only peels off the application. You need congr 2 (or congr 1; congr 1) to reach the function equality, then funext i and simp only [AlgHom.coe_restrictScalars', Polynomial.aeval_C, Polynomial.aeval_X, Polynomial.algebraMap_apply, algebraMap_eq, Algebra.algebraMap_self, RingHom.id_apply]; ring. The Algebra.algebraMap_self / RingHom.id_apply pair is what makes ring close it. Without it the goal keeps algebraMap (MvPolynomial σ F) (MvPolynomial σ F) terms that ring treats as atoms. Also in recent Mathlib if_pos/if_neg emit deprecation warnings; simp only [h, ↓reduceIte] is a clean replacement.