Lean/Mathlib: I-adically complete + A/I Noetherian ⇒ Noetherian without gr_I(A)

Mathlib (v4.35-era) has no associated graded ring, so Stacks 05GH (I f.g., A I-adically complete, A ⧸ I Noetherian ⇒ A Noetherian) seems out of reach. A ~150-line route works with leading forms in (A ⧸ I)[X₁…Xₙ], where I = span (range x) (Submodule.fg_iff_exists_fin_generating_family). For an ideal J let P = {p : MvPolynomial ι A | ∃ k, p.IsHomogeneous k ∧ eval x p ∈ J ⊔ I^(k+1)}. Ideal.span (map π '' P) is f.g. by Hilbert. Submodule.fg_span_iff_fg_span_finset_subset plus Finset.subset_set_image_iff then give a finite T ⊆ P whose images span it. For y ∈ J ∩ I^k, get a homogeneous q with q(x) = y (Ideal.mem_span_pow_iff_exists_isHomogeneous, already in Mathlib). Write map π q = ∑ rᵢ • map π pᵢ (Submodule.mem_span_range_iff_exists_fun, R explicit), lift rᵢ (MvPolynomial.map_surjective) and take degree-k parts. The degree-k part of r * p for homogeneous p comes from DirectSum.coe_decompose_mul_of_right_mem under attribute [local instance] MvPolynomial.gradedAlgebra in, then simpa only [DirectSum.decompose, Equiv.coe_fn_mk, decomposition.decompose'_apply]. The result is homogeneous of degree k with coefficients in I, so it evaluates into I^(k+1). Iterating gives coefficients cᵢ ∈ I^(k-D), D = max degree. Shift partial sums by D to apply IsPrecomplete.prec, then finish with IsHausdorff.haus (I := I) (the I must be given explicitly or the instance is stuck). Gotchas: I^m • ⊤ : Submodule A A becomes I^m with simp [smul_eq_mul, Ideal.mul_top]; IsHomogeneous gives weight 1 d = k, convert with Finsupp.degree_eq_weight_one; a missing import of IsLocalRing shows up as 'invalid binder annotation, type is not a class instance ?m' because of autoImplicit.