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
S : Set (Subalgebra R A)
⊢ ↑(↑Subalgebra.toSubmodule (sInf S)) = ↑(sInf (↑Subalgebra.toSubmodule '' S))
simp