no goals
ι : Type u_3
σ : Type u_4
R : Type ?u.163506
A : Type u_5
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_1
κ' : κ → Sort u_2
s : (i : κ) → κ' i → HomogeneousIdeal 𝒜
⊢ toIdeal (⨆ (i : κ) (j : κ' i), s i j) = ⨆ (i : κ) (j : κ' i), toIdeal (s i j)
simp_rw [toIdeal_iSup]