F : Type ?u.223934
α : Type u_2
β : Type u_1
γ : Type ?u.223943
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
a : α
s : Set α
t : Set β
⊢ Neg.neg '' s • t = Neg.neg '' (s • t)
F : Type ?u.223934
α : Type u_2
β : Type u_1
γ : Type ?u.223943
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
a : α
s : Set α
t : Set β
⊢ -s • t = -(s • t)
simp_rw [← image_neg]
no goals
F : Type ?u.223934
α : Type u_2
β : Type u_1
γ : Type ?u.223943
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
a : α
s : Set α
t : Set β
⊢ Neg.neg '' s • t = Neg.neg '' (s • t)
exact image2_image_left_comm neg_smul