no goals
α : Type ?u.247712
G : Type ?u.247715
M✝ : Type ?u.247718
R : Type u_1
A : Type ?u.247724
inst✝² : Monoid M✝
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
⊢ M * N = closure (↑M * ↑N)
rw [← closure_mul_closure, closure_eq, closure_eq]