no goals
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ ↑(lowerClosure (s * t)) = ↑(lowerClosure s * lowerClosure t)
rw [LowerSet.coe_mul, mul_lowerClosure, lowerClosure_mul, LowerSet.lowerClosure]