no goals
F : Type ?u.675762
R : Type u_2
A : Type u_1
B : Type ?u.675771
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)
x : A
⊢ x ∈ sInf S ↔ ∀ (p : StarSubalgebra R A), p ∈ S → x ∈ p
simp only [← SetLike.mem_coe, coe_sInf, Set.mem_iInter₂]