no goals
M : Type u_1
N : Type ?u.21166
A : Type ?u.21169
inst✝¹ : Mul M
s : Set M
inst✝ : Add A
t : Set A
S : Subsemigroup M
m : M
p : Subsemigroup M
⊢ closure {m} ≤ p ↔ m ∈ p
rw [closure_le, singleton_subset_iff, SetLike.mem_coe]