no goals
R : Type u_2
S : Type ?u.146839
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Module S M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
p✝ q : Submodule R M
ι : Type u_1
s : Finset ι
p : ι → Submodule R M
x : M
⊢ x ∈ Finset.inf s p ↔ ∀ (i : ι), i ∈ s → x ∈ p i
simp only [← SetLike.mem_coe, finset_inf_coe, Set.mem_iInter]