no goals
F : Type ?u.946851
α : Type u_2
β : Type u_1
γ : Type ?u.946860
inst✝³ : Ring α
inst✝² : AddCommGroup β
inst✝¹ : Module α β
inst✝ : DecidableEq β
s : Finset α
t : Finset β
a : α
⊢ -a • t = -(a • t)
simp only [← image_smul, ← image_neg, image_image, neg_smul, Function.comp]