no goals
α : Type ?u.9470
G : Type ?u.9473
M : Type u_1
R : Type ?u.9479
A : Type ?u.9482
inst✝¹ : Monoid M
inst✝ : AddMonoid A
s t u : Set M
H K : Submonoid M
⊢ closure ↑H ⊔ closure ↑K ≤ H ⊔ K
rw [closure_eq, closure_eq]