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)
x : A
⊢ x ∈ sInf S ↔ ∀ (p : Subalgebra R A), p ∈ S → x ∈ p
simp only [← SetLike.mem_coe, coe_sInf, Set.mem_iInter₂]