M : Type u_2
N : Type ?u.21456
A : Type ?u.21459
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
ι : Sort u_1
p : ι → Subsemigroup M
m : M
⊢ (∀ (b : Subsemigroup M), (∀ (i : ι), p i ≤ b) → closure {m} ≤ b) ↔
    ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N
M : Type u_2
N : Type ?u.21456
A : Type ?u.21459
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
ι : Sort u_1
p : ι → Subsemigroup M
m : M
⊢ (m ∈ ⨆ (i : ι), p i) ↔ ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N
rw [← closure_singleton_le_iff_mem, le_iSup_iff]
no goals
M : Type u_2
N : Type ?u.21456
A : Type ?u.21459
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
ι : Sort u_1
p : ι → Subsemigroup M
m : M
⊢ (∀ (b : Subsemigroup M), (∀ (i : ι), p i ≤ b) → closure {m} ≤ b) ↔
    ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N
simp only [closure_singleton_le_iff_mem]