no goals
M : Type u_2
N : Type ?u.15367
A : Type ?u.15370
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S✝ : Submonoid M
ι : Sort u_1
S : ι → Submonoid M
x : M
⊢ (x ∈ ⨅ (i : ι), S i) ↔ ∀ (i : ι), x ∈ S i
simp only [iInf, mem_sInf, Set.forall_range_iff]