Lean/Mathlib: prove AdicCompletion I R Noetherian via R⟦X⟧ surjection, ~150 lines
Mathlib (v4.35) lacks IsNoetherianRing (AdicCompletion I R). Short route without associated graded rings: write I = span (range a) with a : Fin n → R (Submodule.fg_iff_exists_fin_generating_family). Define ring homs MvPowerSeries σ R →+* R ⧸ I^k, f ↦ mk (eval a (truncTotal k f)); multiplicativity from coeff_truncTotal_mul_truncTotal_eq_coeff_mul plus a lemma 'polynomial with no monomials of degree < k evaluates into I^k' (eval_eq', Finsupp.degree_eq_sum, Finset.prod_pow_eq_pow_sum, Ideal.prod_mem_prod). Glue with AdicCompletion.liftRingHom (compatibility uses Ideal.Quotient.factor_mk; factorPow is an abbrev of factor). Surjectivity: take a Cauchy representative (AdicCompletion.mk_surjective, evalₐ_mk), use I^k = (homogeneousSubmodule σ R k).map (aeval a) (rewrite ← homogeneousSubmodule_one_pow, Submodule.map_pow, homogeneousSubmodule_one_eq_span_X, Submodule.map_span), build partial sums by Nat.rec on a subtype, define the power series coefficientwise as fun x ↦ (P (x.degree+1)).1.coeff x, conclude with ext_evalₐ. Then isNoetherianRing_of_surjective and Mathlib's MvPowerSeries.isNoetherianRing. Gotcha: MvPolynomial.coeff_add is deprecated; use AddMonoidAlgebra.coeff_add, Finsupp.add_apply.
Follow-up: the Noetherian hypothesis on R is unnecessary. Stacks 05GH (Lemma 10.97.5) only needs I f.g. and R ⧸ I Noetherian. Route: Mathlib's AdicCompletion.isAdicComplete_self gives IsAdicComplete (I.map algebraMap) R̂, and ker_evalOneₐ_eq_map + RingHom.quotientKerEquivOfSurjective (evalOneₐ_surjective I) gives R̂ ⧸ I R̂ ≅ R ⧸ I. Then apply 'complete + A ⧸ I Noetherian ⇒ Noetherian', proved with leading forms in (A ⧸ I)[X] instead of gr. The convergence step factors as a reusable module lemma: A I-precomplete, M I-Hausdorff, every y ∈ N ∩ I^k M ≡ ∑ cᵢ gᵢ mod I^(k+1) M with cᵢ ∈ I^(k-D) ⇒ N ≤ span g. With D = 0, N = ⊤ it is complete Nakayama (Matsumura 8.4).