refactor(order/filter/pointwise): Localize instances (#13898)

Localize pointwise `filter` instances into the `pointwise` locale, as is done for `set` and `finset`.

Author: YaelDillies

src/order/filter/pointwise.lean

@@ -30,10 +30,17 @@ distribute over pointwise operations. For example,
   `t ∈ g`.
 * `f -ᵥ g` (`filter.has_vsub`): Scalar subtraction, filter generated by all `x -ᵥ y` where `s ∈ f`
   and `t ∈ g`.
-* `f • g` (`filter.has_smul`): Scalar multiplication, filter generated by all `x • y` where `s ∈ f`
-  and `t ∈ g`.
+* `f • g` (`filter.has_scalar`): Scalar multiplication, filter generated by all `x • y` where
+  `s ∈ f` and `t ∈ g`.
 * `a +ᵥ f` (`filter.has_vadd_filter`): Translation, filter of all `a +ᵥ x` where `s ∈ f`.
-* `a • f` (`filter.has_smul_filter`): Scaling, filter of all `a • s` where `s ∈ f`.
+* `a • f` (`filter.has_scalar_filter`): Scaling, filter of all `a • s` where `s ∈ f`.
+
+## Implementation notes
+
+We put all instances in the locale `pointwise`, so that these instances are not available by
+default. Note that we do not mark them as reducible (as argued by note [reducible non-instances])
+since we expect the locale to be open whenever the instances are actually used (and making the
+instances reducible changes the behavior of `simp`.
 
 ## Tags
 
@@ -52,9 +59,12 @@ namespace filter
 section one
 variables [has_one α] {f : filter α} {s : set α}
 
-/-- `1 : filter α` is the set of sets containing `1 : α`. -/
-@[to_additive "`0 : filter α` is the set of sets containing `0 : α`."]
-instance : has_one (filter α) := ⟨principal 1⟩
+/-- `1 : filter α` is defined as the filter of sets containing `1 : α` in locale `pointwise`. -/
+@[to_additive "`0 : filter α` is defined as the filter of sets containing `0 : α` in locale
+`pointwise`."]
+protected def has_one : has_one (filter α) := ⟨principal 1⟩
+
+localized "attribute [instance] filter.has_one filter.has_zero" in pointwise
 
 @[simp, to_additive] lemma mem_one : s ∈ (1 : filter α) ↔ (1 : α) ∈ s := one_subset
 
@@ -84,7 +94,11 @@ end one
 section mul
 variables [has_mul α] [has_mul β] {f f₁ f₂ g g₁ g₂ h : filter α} {s t : set α}
 
-@[to_additive] instance : has_mul (filter α) := ⟨map₂ (*)⟩
+/-- The filter `f * g` is generated by `{s * t | s ∈ f, t ∈ g}` in locale `pointwise`. -/
+@[to_additive "The filter `f + g` is generated by `{s + t | s ∈ f, t ∈ g}` in locale `pointwise`."]
+protected def has_mul : has_mul (filter α) := ⟨map₂ (*)⟩
+
+localized "attribute [instance] filter.has_mul filter.has_add" in pointwise
 
 @[simp, to_additive] lemma map₂_mul : map₂ (*) f g = f * g := rfl
 @[to_additive] lemma mem_mul_iff : s ∈ f * g ↔ ∃ t₁ t₂, t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ * t₂ ⊆ s := iff.rfl
@@ -109,30 +123,42 @@ map_map₂_distrib $ map_mul m
 
 end mul
 
-@[to_additive]
-instance [semigroup α] : semigroup (filter α) :=
+open_locale pointwise
+
+/-- `filter α` is a `semigroup` under pointwise operations if `α` is.-/
+@[to_additive "`filter α` is an `add_semigroup` under pointwise operations if `α` is."]
+protected def semigroup [semigroup α] : semigroup (filter α) :=
 { mul := (*),
   mul_assoc := λ f g h, map₂_assoc mul_assoc }
 
-@[to_additive]
-instance [comm_semigroup α] : comm_semigroup (filter α) :=
+/-- `filter α` is a `comm_semigroup` under pointwise operations if `α` is. -/
+@[to_additive "`filter α` is an `add_comm_semigroup` under pointwise operations if `α` is."]
+protected def comm_semigroup [comm_semigroup α] : comm_semigroup (filter α) :=
 { mul_comm := λ f g, map₂_comm mul_comm,
   ..filter.semigroup }
 
-@[to_additive]
-instance [mul_one_class α] : mul_one_class (filter α) :=
+/-- `filter α` is a `mul_one_class` under pointwise operations if `α` is. -/
+@[to_additive "`filter α` is an `add_zero_class` under pointwise operations if `α` is."]
+protected def mul_one_class [mul_one_class α] : mul_one_class (filter α) :=
 { one := 1,
   mul := (*),
   one_mul := λ f, by simp only [←pure_one, ←map₂_mul, map₂_pure_left, one_mul, map_id'],
   mul_one := λ f, by simp only [←pure_one, ←map₂_mul, map₂_pure_right, mul_one, map_id'] }
 
-@[to_additive]
-instance [monoid α] : monoid (filter α) := { ..filter.mul_one_class, ..filter.semigroup }
+/-- `filter α` is a `monoid` under pointwise operations if `α` is. -/
+@[to_additive "`filter α` is an `add_monoid` under pointwise operations if `α` is."]
+protected def monoid [monoid α] : monoid (filter α) :=
+{ ..filter.mul_one_class, ..filter.semigroup }
 
-@[to_additive]
-instance [comm_monoid α] : comm_monoid (filter α) :=
+/-- `filter α` is a `comm_monoid` under pointwise operations if `α` is. -/
+@[to_additive "`filter α` is an `add_comm_monoid` under pointwise operations if `α` is."]
+protected def comm_monoid [comm_monoid α] : comm_monoid (filter α) :=
 { ..filter.mul_one_class, ..filter.comm_semigroup }
 
+localized "attribute [instance] filter.mul_one_class filter.add_zero_class filter.semigroup
+  filter.add_semigroup filter.comm_semigroup filter.add_comm_semigroup filter.monoid
+  filter.add_monoid filter.comm_monoid filter.add_comm_monoid" in pointwise
+
 section map
 
 variables [mul_one_class α] [mul_one_class β]
@@ -183,7 +209,9 @@ variables [has_involutive_inv α] {f : filter α} {s : set α}
 
 @[to_additive] lemma inv_mem_inv (hs : s ∈ f) : s⁻¹ ∈ f⁻¹ := by rwa [mem_inv, inv_preimage, inv_inv]
 
-instance : has_involutive_inv (filter α) :=
+/-- Inversion is involutive on `filter α` if it is on `α`. -/
+@[to_additive "Negation is involutive on `filter α` if it is on `α`."]
+def has_involutive_inv : has_involutive_inv (filter α) :=
 { inv_inv := λ f, map_map.trans $ by rw [inv_involutive.comp_self, map_id],
   ..filter.has_inv }
 
@@ -208,7 +236,11 @@ end group
 section div
 variables [has_div α] {f f₁ f₂ g g₁ g₂ h : filter α} {s t : set α}
 
-@[to_additive] instance : has_div (filter α) := ⟨map₂ (/)⟩
+/-- The filter `f / g` is generated by `{s / t | s ∈ f, t ∈ g}` in locale `pointwise`. -/
+@[to_additive "The filter `f - g` is generated by `{s - t | s ∈ f, t ∈ g}` in locale `pointwise`."]
+protected def has_div : has_div (filter α) := ⟨map₂ (/)⟩
+
+localized "attribute [instance] filter.has_div filter.has_sub" in pointwise
 
 @[simp, to_additive] lemma map₂_div : map₂ (/) f g = f / g := rfl
 @[to_additive] lemma mem_div : s ∈ f / g ↔ ∃ t₁ t₂, t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ / t₂ ⊆ s := iff.rfl
@@ -233,6 +265,8 @@ le_map₂_iff
 
 end div
 
+open_locale pointwise
+
 section group
 variables [group α] [group β] {f g  : filter α} {f₂ : filter β}
 
@@ -251,16 +285,20 @@ end group
 `div_inv_monoid` and `has_involutive_inv` but smaller than `group` and `group_with_zero`. -/
 
 /-- `f / g = f * g⁻¹` for all `f g : filter α` if `a / b = a * b⁻¹` for all `a b : α`. -/
-@[to_additive "`f - g = f + -g` for all `f g : filter α` if `a - b = a + -b` for all `a b : α`."]
-instance div_inv_monoid [group α] : div_inv_monoid (filter α) :=
+@[to_additive filter.sub_neg_monoid "`f - g = f + -g` for all `f g : filter α` if `a - b = a + -b`
+for all `a b : α`."]
+protected def div_inv_monoid [group α] : div_inv_monoid (filter α) :=
 { div_eq_mul_inv := λ f g, map_map₂_distrib_right div_eq_mul_inv,
   ..filter.monoid, ..filter.has_inv, ..filter.has_div }
 
 /-- `f / g = f * g⁻¹` for all `f g : filter α` if `a / b = a * b⁻¹` for all `a b : α`. -/
-instance div_inv_monoid' [group_with_zero α] : div_inv_monoid (filter α) :=
+protected def div_inv_monoid' [group_with_zero α] : div_inv_monoid (filter α) :=
 { div_eq_mul_inv := λ f g, map_map₂_distrib_right div_eq_mul_inv,
   ..filter.monoid, ..filter.has_inv, ..filter.has_div }
 
+localized "attribute [instance] filter.div_inv_monoid filter.sub_neg_monoid filter.div_inv_monoid'"
+  in pointwise
+
 /-! ### Scalar addition/multiplication of filters -/
 
 section smul
@@ -298,7 +336,10 @@ section vsub
 variables [has_vsub α β] {f f₁ f₂ g g₁ g₂ : filter β} {h : filter α} {s t : set β}
 include α
 
-instance : has_vsub (filter α) (filter β) := ⟨map₂ (-ᵥ)⟩
+/-- The filter `f -ᵥ g` is generated by `{s -ᵥ t | s ∈ f, t ∈ g}` in locale `pointwise`. -/
+protected def has_vsub : has_vsub (filter α) (filter β) := ⟨map₂ (-ᵥ)⟩
+
+localized "attribute [instance] filter.has_vsub" in pointwise
 
 @[simp] lemma map₂_vsub : map₂ (-ᵥ) f g = f -ᵥ g := rfl
 lemma mem_vsub {s : set α} : s ∈ f -ᵥ g ↔ ∃ t₁ t₂, t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ -ᵥ t₂ ⊆ s := iff.rfl
@@ -320,8 +361,12 @@ end vsub
 section smul
 variables [has_scalar α β] {f f₁ f₂ : filter β} {s : set β} {a : α}
 
-@[to_additive filter.has_vadd_filter]
-instance has_scalar_filter : has_scalar α (filter β) := ⟨λ a, map ((•) a)⟩
+/-- `a • f` is the map of `f` under `a •` in locale `pointwise`. -/
+@[to_additive filter.has_vadd_filter
+"`a +ᵥ f` is the map of `f` under `a +ᵥ` in locale `pointwise`."]
+protected def has_scalar_filter : has_scalar α (filter β) := ⟨λ a, map ((•) a)⟩
+
+localized "attribute [instance] filter.has_scalar_filter filter.has_vadd_filter" in pointwise
 
 @[simp, to_additive] lemma map_smul : map (λ b, a • b) f = a • f := rfl
 @[to_additive] lemma mem_smul_filter : s ∈ a • f ↔ (•) a ⁻¹' s ∈ f := iff.rfl
@@ -339,6 +384,8 @@ map_mono hf
 
 end smul
 
+open_locale pointwise
+
 @[to_additive]
 instance smul_comm_class_filter [has_scalar α γ] [has_scalar β γ] [smul_comm_class α β γ] :
   smul_comm_class α (filter β) (filter γ) :=