chore(order/filter/pointwise): Better definitional unfolding (#13941)

Tweak pointwise operation definitions to make them easier to work with:
* `1` is now `pure 1` instead of `principal 1`. This changes defeq.
* Binary operations unfold to the set operation instead exposing a bare `set.image2` (`obtain ⟨t₁, t₂, h₁, h₂, h⟩ : s ∈ f * g` now gives `h : t₁ * t₂ ⊆ s` instead of `h : set.image2 (*) t₁ t₂ ⊆ s`. This does not change defeq.

Author: YaelDillies

src/order/filter/pointwise.lean

@@ -17,8 +17,8 @@ distribute over pointwise operations. For example,
 
 ## Main declarations
 
-* `0` (`filter.has_zero`): Principal filter at `0 : α`.
-* `1` (`filter.has_one`): Principal filter at `1 : α`.
+* `0` (`filter.has_zero`): Pure filter at `0 : α`, or alternatively principal filter at `0 : set α`.
+* `1` (`filter.has_one`): Pure filter at `1 : α`, or alternatively principal filter at `1 : set α`.
 * `f + g` (`filter.has_add`): Addition, filter generated by all `s + t` where `s ∈ f` and `t ∈ g`.
 * `f * g` (`filter.has_mul`): Multiplication, filter generated by all `s * t` where `s ∈ f` and
   `t ∈ g`.
@@ -63,30 +63,27 @@ variables [has_one α] {f : filter α} {s : set α}
 /-- `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⟩
+protected def has_one : has_one (filter α) := ⟨pure 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
-
-@[to_additive] lemma one_mem_one : (1 : set α) ∈ (1 : filter α) := mem_principal_self _
-
-@[simp, to_additive] lemma principal_one : 𝓟 1 = (1 : filter α) := rfl
-@[simp, to_additive] lemma le_one_iff : f ≤ 1 ↔ (1 : set α) ∈ f := le_principal_iff
-@[simp, to_additive] lemma pure_one : pure 1 = (1 : filter α) := (principal_singleton _).symm
-@[simp, to_additive] lemma eventually_one {p : α → Prop} : (∀ᶠ x in 1, p x) ↔ p 1 :=
-by rw [←pure_one, eventually_pure]
+@[simp, to_additive] lemma mem_one : s ∈ (1 : filter α) ↔ (1 : α) ∈ s := mem_pure
+@[to_additive] lemma one_mem_one : (1 : set α) ∈ (1 : filter α) := mem_pure.2 one_mem_one
+@[simp, to_additive] lemma pure_one : pure 1 = (1 : filter α) := rfl
+@[simp, to_additive] lemma principal_one : 𝓟 1 = (1 : filter α) := principal_singleton _
+@[to_additive] lemma one_ne_bot : (1 : filter α).ne_bot := filter.pure_ne_bot
+@[simp, to_additive] protected lemma map_one' (f : α → β) : (1 : filter α).map f = pure (f 1) := rfl
+@[simp, to_additive] lemma le_one_iff : f ≤ 1 ↔ (1 : set α) ∈ f := le_pure_iff
+@[simp, to_additive] lemma eventually_one {p : α → Prop} : (∀ᶠ x in 1, p x) ↔ p 1 := eventually_pure
 @[simp, to_additive] lemma tendsto_one {a : filter β} {f : β → α} :
    tendsto f a 1 ↔ ∀ᶠ x in a, f x = 1 :=
-by rw [←pure_one, tendsto_pure]
+tendsto_pure
 
 variables [has_one β]
 
 @[simp, to_additive]
 protected lemma map_one [one_hom_class F α β] (φ : F) : map φ 1 = 1 :=
-le_antisymm
-  (le_principal_iff.2 $ mem_map_iff_exists_image.2 ⟨1, one_mem_one, λ x, by simp [map_one φ]⟩)
-  (le_map $ λ s hs, mem_one.2 ⟨1, mem_one.1 hs, map_one φ⟩)
+by rw [filter.map_one', map_one, pure_one]
 
 end one
 
@@ -97,7 +94,10 @@ variables [has_mul α] [has_mul β] {f f₁ f₂ g g₁ g₂ h : filter α} {s t
 
 /-- 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₂ (*)⟩
+protected def has_mul : has_mul (filter α) :=
+/- This is defeq to `map₂ (*) f g`, but the hypothesis unfolds to `t₁ * t₂ ⊆ s` rather than all the
+way to `set.image2 (*) t₁ t₂ ⊆ s`. -/
+⟨λ f g, { sets := {s | ∃ t₁ t₂, t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ * t₂ ⊆ s}, ..map₂ (*) f g }⟩
 
 localized "attribute [instance] filter.has_mul filter.has_add" in pointwise
 
@@ -246,7 +246,10 @@ variables [has_div α] {f f₁ f₂ g g₁ g₂ h : filter α} {s t : set α} {a
 
 /-- 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₂ (/)⟩
+protected def has_div : has_div (filter α) :=
+/- This is defeq to `map₂ (/) f g`, but the hypothesis unfolds to `t₁ / t₂ ⊆ s` rather than all the
+way to `set.image2 (/) t₁ t₂ ⊆ s`. -/
+⟨λ f g, { sets := {s | ∃ t₁ t₂, t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ / t₂ ⊆ s}, ..map₂ (/) f g }⟩
 
 localized "attribute [instance] filter.has_div filter.has_sub" in pointwise
 
@@ -318,7 +321,10 @@ section smul
 variables [has_scalar α β] {f f₁ f₂ : filter α} {g g₁ g₂ h : filter β} {s : set α} {t : set β}
   {a : α} {b : β}
 
-@[to_additive filter.has_vadd] instance : has_scalar (filter α) (filter β) := ⟨map₂ (•)⟩
+@[to_additive filter.has_vadd] instance : has_scalar (filter α) (filter β) :=
+/- This is defeq to `map₂ (•) f g`, but the hypothesis unfolds to `t₁ • t₂ ⊆ s` rather than all the
+way to `set.image2 (•) t₁ t₂ ⊆ s`. -/
+⟨λ f g, { sets := {s | ∃ t₁ t₂, t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ • t₂ ⊆ s}, ..map₂ (•) f g }⟩
 
 @[simp, to_additive] lemma map₂_smul : map₂ (•) f g = f • g := rfl
 @[to_additive] lemma mem_smul : t ∈ f • g ↔ ∃ t₁ t₂, t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ • t₂ ⊆ t := iff.rfl
@@ -357,7 +363,10 @@ variables [has_vsub α β] {f f₁ f₂ g g₁ g₂ : filter β} {h : filter α}
 include α
 
 /-- 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₂ (-ᵥ)⟩
+protected def has_vsub : has_vsub (filter α) (filter β) :=
+/- This is defeq to `map₂ (-ᵥ) f g`, but the hypothesis unfolds to `t₁ -ᵥ t₂ ⊆ s` rather than all
+the way to `set.image2 (-ᵥ) t₁ t₂ ⊆ s`. -/
+⟨λ f g, { sets := {s | ∃ t₁ t₂, t₁ ∈ f ∧ t₂ ∈ g ∧ t₁ -ᵥ t₂ ⊆ s}, ..map₂ (-ᵥ) f g }⟩
 
 localized "attribute [instance] filter.has_vsub" in pointwise