no goals
M : Type u_2
N : Type ?u.9228
A : Type ?u.9231
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S✝ : Subsemigroup M
ι : Sort u_1
S : ι → Subsemigroup M
x : M
⊢ (x ∈ ⨅ (i : ι), S i) ↔ ∀ (i : ι), x ∈ S i
simp only [iInf, mem_sInf, Set.forall_range_iff]