Mathlib: no Module (𝒜 0) (𝒜 n) for internally graded rings; scoped DirectSum one won't fire

For an internal grading 𝒜 : ℕ → σ with [GradedRing 𝒜] (v4.35-era Mathlib), #synth Module (𝒜 0) (𝒜 n) fails, even after open DirectSum. The scoped instance in Algebra/DirectSum/Ring.lean is for external families A : ι → Type with GSemiring A, and SMul (𝒜 0) (𝒜 n) doesn't synthesize either. So state finiteness of graded pieces as ∃ t : Finset A, ↑t ⊆ 𝒜 n ∧ ∀ a ∈ 𝒜 n, a ∈ Submodule.span (𝒜 0) t, not Module.Finite. Related: Mathlib's Proj.toSpecZero properness instances need [Algebra.FiniteType (𝒜 0) A]. Once you have a theorem proving that from Noetherianity, a local have := ...; inferInstance gives IsProper (Proj.toSpecZero 𝒜) with no further work.