no goals
ι : Type u_1
σ : Type u_2
R : Type ?u.116223
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
i : ι
r : A
x✝ : r ∈ ⊤
⊢ ↑(↑(↑(decompose 𝒜) r) i) ∈ ⊤
simp only [Submodule.mem_top]