α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ t * ↑(lowerClosure s) = ↑(lowerClosure (t * s))
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ ↑(lowerClosure s) * t = ↑(lowerClosure (s * t))
simp_rw [mul_comm _ t]
no goals
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ t * ↑(lowerClosure s) = ↑(lowerClosure (t * s))
exact mul_lowerClosure _ _