@[simp]

theorem Set.vadd_set_vsub_vadd_set {G : Type u_1} {P : Type u_2} [AddCommGroup G] [AddTorsor G P] (v : G) (s : Set P) (t : Set P) : v +ᵥ s -ᵥ (v +ᵥ t) = s -ᵥ t