no goals
F : Type ?u.937268
α : Type u_2
β : Type u_1
γ : Type ?u.937277
inst✝³ : Monoid α
inst✝² : AddGroup β
inst✝¹ : DistribMulAction α β
inst✝ : DecidableEq β
a : α
s : Finset α
t : Finset β
⊢ a • -t = -(a • t)
simp only [← image_smul, ← image_neg, Function.comp, image_image, smul_neg]