no goals
ι : Type u_2
σ : Type u_3
R : Type ?u.161617
A : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_1
s : κ → HomogeneousIdeal 𝒜
⊢ toIdeal (⨅ (i : κ), s i) = ⨅ (i : κ), toIdeal (s i)
rw [iInf, toIdeal_sInf, iInf_range]