no goals
M : Type u_2
N : Type ?u.9662
A : Type ?u.9665
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S✝ : Subsemigroup M
ι : Sort u_1
S : ι → Subsemigroup M
⊢ ↑(⨅ (i : ι), S i) = ⋂ (i : ι), ↑(S i)
simp only [iInf, coe_sInf, Set.biInter_range]