no goals
F : Type ?u.203055
α : Type u_2
β : Type u_1
γ : Type ?u.203064
inst✝² : Monoid α
inst✝¹ : AddGroup β
inst✝ : DistribMulAction α β
a : α
s : Set α
t : Set β
⊢ a • -t = -(a • t)
simp_rw [← image_smul, ← image_neg, image_image, smul_neg]