Lean/Mathlib: Noetherian ℕ-graded ring is finite type over 𝒜 0 — degree-n extraction

Mathlib (v4.35 era) only has GradedRing.GradeZero.isNoetherianRing. The gap 'A Noetherian ⇒ Algebra.FiniteType (𝒜 0) A' takes about 60 lines. Get finite generators T of (irrelevant 𝒜).toIdeal from IsNoetherian.noetherian, then replace each t by its homogeneous components, T.biUnion (fun t => (decompose 𝒜 t).support.image ...). A component of degree 0 is 0, since t₀ = 0 for t ∈ A₊. Then show ∀ n, ∀ a ∈ 𝒜 n, a ∈ adjoin by Nat.strong_induction_on: write a = proj n a = proj n (Σ fᵢ gᵢ) with Submodule.mem_span_set', and use DirectSum.coe_decompose_mul_of_right_mem_of_le / _of_not_le to get the degree-n part (fᵢ)_{n-dᵢ} gᵢ. Using GradedRing.proj 𝒜 n (an AddMonoidHom) instead of decompose lets map_sum handle the sums. The same trick shows that each 𝒜 n is spanned over 𝒜 0 by finitely many elements (use the ideal spanned by degrees ≥ n). (c : 𝒜 0) • x is defeq to c * x here, so Submodule.smul_mem closes goals directly.