feat(data/finset/pointwise): -s • t = -(s • t) (#16138)

and copy over other pointwise `set` lemmas. Generalize the `set` lemmas. `set.smul_neg`, `set.neg_smul`, `set.smul_set_neg`, `set.neg_smul_set` now have explicit arguments.

src/analysis/locally_convex/basic.lean

@@ -176,10 +176,10 @@ variables [add_comm_group E] [module 𝕜 E] {s s₁ s₂ t t₁ t₂ : set E}
 
 lemma absorbs.neg : absorbs 𝕜 s t → absorbs 𝕜 (-s) (-t) :=
 Exists.imp $ λ r, and.imp_right $ forall₂_imp $ λ _ _ h,
-  (neg_subset_neg.2 h).trans set.smul_set_neg.superset
+  (neg_subset_neg.2 h).trans (smul_set_neg _ _).superset
 
 lemma balanced.neg : balanced 𝕜 s → balanced 𝕜 (-s) :=
-forall₂_imp $ λ _ _ h, smul_set_neg.subset.trans $ neg_subset_neg.2 h
+forall₂_imp $ λ _ _ h, (smul_set_neg _ _).subset.trans $ neg_subset_neg.2 h
 
 lemma absorbs.add : absorbs 𝕜 s₁ t₁ → absorbs 𝕜 s₂ t₂ → absorbs 𝕜 (s₁ + s₂) (t₁ + t₂) :=
 λ ⟨r₁, hr₁, h₁⟩ ⟨r₂, hr₂, h₂⟩, ⟨max r₁ r₂, lt_max_of_lt_left hr₁, λ a ha, (add_subset_add

src/data/finset/pointwise.lean

@@ -985,4 +985,66 @@ lemma smul_finset_univ₀ [fintype β] (ha : a ≠ 0) : a • (univ : finset β)
 coe_injective $ by {  push_cast, exact set.smul_set_univ₀ ha }
 
 end group_with_zero
+
+section smul_with_zero
+variables [has_zero α] [has_zero β] [smul_with_zero α β] [decidable_eq β] {s : finset α}
+  {t : finset β}
+
+/-!
+Note that we have neither `smul_with_zero α (finset β)` nor `smul_with_zero (finset α) (finset β)`
+because `0 * ∅ ≠ 0`.
+-/
+
+lemma smul_zero_subset (s : finset α) : s • (0 : finset β) ⊆ 0 := by simp [subset_iff, mem_smul]
+lemma zero_smul_subset (t : finset β) : (0 : finset α) • t ⊆ 0 := by simp [subset_iff, mem_smul]
+
+lemma nonempty.smul_zero (hs : s.nonempty) : s • (0 : finset β) = 0 :=
+s.smul_zero_subset.antisymm $ by simpa [mem_smul] using hs
+
+lemma nonempty.zero_smul (ht : t.nonempty) : (0 : finset α) • t = 0 :=
+t.zero_smul_subset.antisymm $ by simpa [mem_smul] using ht
+
+/-- A nonempty set is scaled by zero to the singleton set containing 0. -/
+lemma zero_smul_finset {s : finset β} (h : s.nonempty) : (0 : α) • s = (0 : finset β) :=
+coe_injective $ by simpa using set.zero_smul_set h
+
+lemma zero_smul_finset_subset (s : finset β) : (0 : α) • s ⊆ 0 :=
+image_subset_iff.2 $ λ x _, mem_zero.2 $ zero_smul α x
+
+lemma zero_mem_smul_finset {t : finset β} {a : α} (h : (0 : β) ∈ t) : (0 : β) ∈ a • t :=
+mem_smul_finset.2 ⟨0, h, smul_zero' _ _⟩
+
+variables [no_zero_smul_divisors α β] {a : α}
+
+lemma zero_mem_smul_iff : (0 : β) ∈ s • t ↔ (0 : α) ∈ s ∧ t.nonempty ∨ (0 : β) ∈ t ∧ s.nonempty :=
+by { rw [←mem_coe, coe_smul, set.zero_mem_smul_iff], refl }
+
+lemma zero_mem_smul_finset_iff (ha : a ≠ 0) : (0 : β) ∈ a • t ↔ (0 : β) ∈ t :=
+by { rw [←mem_coe, coe_smul_finset, set.zero_mem_smul_set_iff ha, mem_coe], apply_instance }
+
+end smul_with_zero
+
+section monoid
+variables [monoid α] [add_group β] [distrib_mul_action α β] [decidable_eq β] (a : α) (s : finset α)
+  (t : finset β)
+
+@[simp] lemma smul_finset_neg : a • -t = -(a • t) :=
+by simp only [←image_smul, ←image_neg, function.comp, image_image, smul_neg]
+
+@[simp] protected lemma smul_neg : s • -t = -(s • t) :=
+by { simp_rw ←image_neg, exact image_image₂_right_comm smul_neg }
+
+end monoid
+
+section ring
+variables [ring α] [add_comm_group β] [module α β] [decidable_eq β] {s : finset α} {t : finset β}
+  {a : α}
+
+@[simp] lemma neg_smul_finset : -a • t = -(a • t) :=
+by simp only [←image_smul, ←image_neg, image_image, neg_smul]
+
+@[simp] protected lemma neg_smul [decidable_eq α] : -s • t = -(s • t) :=
+by { simp_rw ←image_neg, exact image₂_image_left_comm neg_smul }
+
+end ring
 end finset

src/data/set/pointwise.lean

@@ -1194,23 +1194,6 @@ end vsub
 
 open_locale pointwise
 
-section ring
-variables [ring α] [add_comm_group β] [module α β] {s : set α} {t : set β} {a : α}
-
-@[simp] lemma neg_smul_set : -a • t = -(a • t) :=
-by simp_rw [←image_smul, ←image_neg, image_image, neg_smul]
-
-@[simp] lemma smul_set_neg : a • -t = -(a • t) :=
-by simp_rw [←image_smul, ←image_neg, image_image, smul_neg]
-
-@[simp] protected lemma neg_smul : -s • t = -(s • t) :=
-by { simp_rw ←image_neg, exact image2_image_left_comm neg_smul }
-
-@[simp] protected lemma smul_neg : s • -t = -(s • t) :=
-by { simp_rw ←image_neg, exact image_image2_right_comm smul_neg }
-
-end ring
-
 section smul_with_zero
 variables [has_zero α] [has_zero β] [smul_with_zero α β] {s : set α} {t : set β}
 
@@ -1351,6 +1334,28 @@ eq_univ_of_forall $ λ b, ⟨a⁻¹ • b, trivial, smul_inv_smul₀ ha _⟩
 
 end group_with_zero
 
+section monoid
+variables [monoid α] [add_group β] [distrib_mul_action α β] (a : α) (s : set α) (t : set β)
+
+@[simp] lemma smul_set_neg : a • -t = -(a • t) :=
+by simp_rw [←image_smul, ←image_neg, image_image, smul_neg]
+
+@[simp] protected lemma smul_neg : s • -t = -(s • t) :=
+by { simp_rw ←image_neg, exact image_image2_right_comm smul_neg }
+
+end monoid
+
+section ring
+variables [ring α] [add_comm_group β] [module α β] (a : α) (s : set α) (t : set β)
+
+@[simp] lemma neg_smul_set : -a • t = -(a • t) :=
+by simp_rw [←image_smul, ←image_neg, image_image, neg_smul]
+
+@[simp] protected lemma neg_smul : -s • t = -(s • t) :=
+by { simp_rw ←image_neg, exact image2_image_left_comm neg_smul }
+
+end ring
+
 end set
 
 /-! ### Miscellaneous -/