no goals
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ ↑(upperClosure (s * t)) = ↑(upperClosure s * upperClosure t)
rw [UpperSet.coe_mul, mul_upperClosure, upperClosure_mul, UpperSet.upperClosure]