no goals
M : Type u_1
N : Type ?u.28852
A : Type ?u.28855
inst✝¹ : MulOneClass M
s : Set M
inst✝ : AddZeroClass A
t : Set A
S : Submonoid M
m : M
p : Submonoid M
⊢ closure {m} ≤ p ↔ m ∈ p
rw [closure_le, singleton_subset_iff, SetLike.mem_coe]