no goals
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
ι : Sort u_1
S : ι → Subalgebra R A
⊢ ↑(↑toSubmodule (⨅ (i : ι), S i)) = ↑(⨅ (i : ι), ↑toSubmodule (S i))
simp