feat(algebra/pointwise): add to_additive attributes for pointwise smul (

#8878)

I wanted this to generalize some definitions in #2819 but it should be independent.

src/algebra/add_torsor.lean

@@ -208,9 +208,9 @@ end vsub
 open_locale pointwise
 
 instance add_action : add_action (set G) (set P) :=
-{ vadd := set.image2 (+ᵥ),
-  zero_vadd := λ s, by simp [← singleton_zero],
-  add_vadd := λ s t p, by { apply image2_assoc, intros, apply add_vadd } }
+{ zero_vadd := λ s, by simp [has_vadd.vadd, ←singleton_zero, image2_singleton_left],
+  add_vadd := λ s t p, by { apply image2_assoc, intros, apply add_vadd },
+  ..(show has_vadd (set G) (set P), by apply_instance) }
 
 variables {s s' : set G} {t t' : set P}
 
@@ -219,9 +219,6 @@ image2_subset hs ht
 
 @[simp] lemma vadd_singleton (s : set G) (p : P) : s +ᵥ {p} = (+ᵥ p) '' s := image2_singleton_right
 
-@[simp] lemma singleton_vadd (v : G) (s : set P) : ({v} : set G) +ᵥ s = ((+ᵥ) v) '' s :=
-image2_singleton_left
-
 lemma finite.vadd (hs : finite s) (ht : finite t) : finite (s +ᵥ t) := hs.image2 _ ht
 
 end set

src/algebra/pointwise.lean

@@ -400,64 +400,80 @@ hs.preimage $ inv_injective.inj_on _
 
 /-- The scaling of a set `(x • s : set β)` by a scalar `x ∶ α` is defined as `{x • y | y ∈ s}`
 in locale `pointwise`. -/
+@[to_additive has_vadd_set "The translation of a set `(x +ᵥ s : set β)` by a scalar `x ∶ α` is
+defined as `{x +ᵥ y | y ∈ s}` in locale `pointwise`."]
 protected def has_scalar_set [has_scalar α β] : has_scalar α (set β) :=
 ⟨λ a, image (has_scalar.smul a)⟩
 
 /-- The pointwise scalar multiplication `(s • t : set β)` by a set of scalars `s ∶ set α`
 is defined as `{x • y | x ∈ s, y ∈ t}` in locale `pointwise`. -/
+@[to_additive has_vadd "The pointwise translation `(s +ᵥ t : set β)` by a set of constants
+`s ∶ set α` is defined as `{x +ᵥ y | x ∈ s, y ∈ t}` in locale `pointwise`."]
 protected def has_scalar [has_scalar α β] : has_scalar (set α) (set β) :=
 ⟨image2 has_scalar.smul⟩
 
 localized "attribute [instance] set.has_scalar_set set.has_scalar" in pointwise
+localized "attribute [instance] set.has_vadd_set set.has_vadd" in pointwise
 
-@[simp]
+@[simp, to_additive]
 lemma image_smul [has_scalar α β] {t : set β} : (λ x, a • x) '' t = a • t := rfl
 
+@[to_additive]
 lemma mem_smul_set [has_scalar α β] {t : set β} : x ∈ a • t ↔ ∃ y, y ∈ t ∧ a • y = x := iff.rfl
 
+@[to_additive]
 lemma smul_mem_smul_set [has_scalar α β] {t : set β} (hy : y ∈ t) : a • y ∈ a • t :=
 ⟨y, hy, rfl⟩
 
+@[to_additive]
 lemma smul_set_union [has_scalar α β] {s t : set β} : a • (s ∪ t) = a • s ∪ a • t :=
 by simp only [← image_smul, image_union]
 
-@[simp]
+@[simp, to_additive]
 lemma smul_set_empty [has_scalar α β] (a : α) : a • (∅ : set β) = ∅ :=
 by rw [← image_smul, image_empty]
 
+@[to_additive]
 lemma smul_set_mono [has_scalar α β] {s t : set β} (h : s ⊆ t) : a • s ⊆ a • t :=
 by { simp only [← image_smul, image_subset, h] }
 
-@[simp]
+@[simp, to_additive]
 lemma image2_smul [has_scalar α β] {t : set β} : image2 has_scalar.smul s t = s • t := rfl
 
+@[to_additive]
 lemma mem_smul [has_scalar α β] {t : set β} : x ∈ s • t ↔ ∃ a y, a ∈ s ∧ y ∈ t ∧ a • y = x :=
 iff.rfl
 
+@[to_additive]
 lemma image_smul_prod [has_scalar α β] {t : set β} :
   (λ x : α × β, x.fst • x.snd) '' s.prod t = s • t :=
 image_prod _
 
+@[to_additive]
 theorem range_smul_range [has_scalar α β] {ι κ : Type*} (b : ι → α) (c : κ → β) :
   range b • range c = range (λ p : ι × κ, b p.1 • c p.2) :=
 ext $ λ x, ⟨λ hx, let ⟨p, q, ⟨i, hi⟩, ⟨j, hj⟩, hpq⟩ := set.mem_smul.1 hx in
   ⟨(i, j), hpq ▸ hi ▸ hj ▸ rfl⟩,
 λ ⟨⟨i, j⟩, h⟩, set.mem_smul.2 ⟨b i, c j, ⟨i, rfl⟩, ⟨j, rfl⟩, h⟩⟩
 
+@[simp, to_additive]
 lemma singleton_smul [has_scalar α β] {t : set β} : ({a} : set α) • t = a • t :=
 image2_singleton_left
 
+@[to_additive]
 instance smul_comm_class_set {γ : Type*}
   [has_scalar α γ] [has_scalar β γ] [smul_comm_class α β γ] :
   smul_comm_class α (set β) (set γ) :=
 { smul_comm := λ a T T',
     by simp only [←image2_smul, ←image_smul, image2_image_right, image_image2, smul_comm] }
 
+@[to_additive]
 instance smul_comm_class_set' {γ : Type*}
   [has_scalar α γ] [has_scalar β γ] [smul_comm_class α β γ] :
   smul_comm_class (set α) β (set γ) :=
 by haveI := smul_comm_class.symm α β γ; exact smul_comm_class.symm _ _ _
 
+@[to_additive]
 instance smul_comm_class {γ : Type*}
   [has_scalar α γ] [has_scalar β γ] [smul_comm_class α β γ] :
   smul_comm_class (set α) (set β) (set γ) :=