no goals
F : Type ?u.218829
α : Type u_2
β : Type u_1
γ : Type ?u.218838
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
a : α
s : Set α
t : Set β
⊢ -a • t = -(a • t)
simp_rw [← image_smul, ← image_neg, image_image, neg_smul]