no goals
R : Type u
S✝ : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S✝
inst✝ : Ring T
ι : Sort u_1
S : ι → Subring R
⊢ ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)
simp only [iInf, coe_sInf, Set.biInter_range]