α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ (⋃ (a : α) (_ : a ∈ s), a • ↑(lowerClosure t)) = ⋃ (i : α) (_ : i ∈ s), ↑(i • lowerClosure t)
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ s * ↑(lowerClosure t) = ↑(lowerClosure (s * t))
simp_rw [← smul_eq_mul, ← Set.iUnion_smul_set, lowerClosure_iUnion, lowerClosure_smul,
  LowerSet.coe_iSup₂]
no goals
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
a : α
⊢ (⋃ (a : α) (_ : a ∈ s), a • ↑(lowerClosure t)) = ⋃ (i : α) (_ : i ∈ s), ↑(i • lowerClosure t)
rfl