α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ (⋃ (a : α) (_ : a ∈ s), a • ↑(upperClosure t)) = ⋃ (i : α) (_ : i ∈ s), ↑(i • upperClosure t)
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ s * ↑(upperClosure t) = ↑(upperClosure (s * t))
simp_rw [← smul_eq_mul, ← Set.iUnion_smul_set, upperClosure_iUnion, upperClosure_smul,
  UpperSet.coe_iInf₂]
no goals
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ (⋃ (a : α) (_ : a ∈ s), a • ↑(upperClosure t)) = ⋃ (i : α) (_ : i ∈ s), ↑(i • upperClosure t)
rfl