no goals
M : Type u_2
N : Type ?u.22167
A : Type ?u.22170
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
ι : Sort u_1
p : ι → Subsemigroup M
⊢ (⨆ (i : ι), p i) = closure (⋃ (i : ι), ↑(p i))
simp_rw [Subsemigroup.closure_iUnion, Subsemigroup.closure_eq]