no goals
F : Type ?u.678241
R : Type u_2
A : Type u_1
B : Type ?u.678250
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : Semiring A
inst✝⁶ : Algebra R A
inst✝⁵ : StarRing A
inst✝⁴ : StarModule R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : StarRing B
inst✝ : StarModule R B
S : Set (StarSubalgebra R A)
⊢ ↑(sInf S).toSubalgebra = ↑(sInf (toSubalgebra '' S))
simp