feat(Filter/{NAry,Pointwise}): add missing NeBot instances (#9055)

- Add missing `Filter.NeBot` instances for `Filter.map₂` and pointwise operations, rename `Filter.prod_neBot'` to `Filter.prod.instNeBot`.
- Make `Filter.prod_eq_bot` a `simp` lemma.
- Protect some lemmas.
- Golf some proofs.
- Make `Filter.map₂_left` and `Filter.map₂_right` take `NeBot` argument as an instance.

Mathlib/Order/Filter/NAry.lean

@@ -100,94 +100,59 @@ theorem le_map₂_iff {h : Filter γ} :
 #align filter.le_map₂_iff Filter.le_map₂_iff
 
 @[simp]
-theorem map₂_bot_left : map₂ m ⊥ g = ⊥ :=
-  empty_mem_iff_bot.1 ⟨∅, univ, trivial, univ_mem, image2_empty_left.subset⟩
-#align filter.map₂_bot_left Filter.map₂_bot_left
+theorem map₂_eq_bot_iff : map₂ m f g = ⊥ ↔ f = ⊥ ∨ g = ⊥ := by simp [← map_prod_eq_map₂]
+#align filter.map₂_eq_bot_iff Filter.map₂_eq_bot_iff
 
 @[simp]
-theorem map₂_bot_right : map₂ m f ⊥ = ⊥ :=
-  empty_mem_iff_bot.1 ⟨univ, ∅, univ_mem, trivial, image2_empty_right.subset⟩
-#align filter.map₂_bot_right Filter.map₂_bot_right
+theorem map₂_bot_left : map₂ m ⊥ g = ⊥ := map₂_eq_bot_iff.2 <| .inl rfl
+#align filter.map₂_bot_left Filter.map₂_bot_left
 
 @[simp]
-theorem map₂_eq_bot_iff : map₂ m f g = ⊥ ↔ f = ⊥ ∨ g = ⊥ := by
-  simp only [← empty_mem_iff_bot, mem_map₂_iff, subset_empty_iff, image2_eq_empty_iff]
-  constructor
-  · rintro ⟨s, t, hs, ht, rfl | rfl⟩
-    · exact Or.inl hs
-    · exact Or.inr ht
-  · rintro (h | h)
-    · exact ⟨_, _, h, univ_mem, Or.inl rfl⟩
-    · exact ⟨_, _, univ_mem, h, Or.inr rfl⟩
-#align filter.map₂_eq_bot_iff Filter.map₂_eq_bot_iff
+theorem map₂_bot_right : map₂ m f ⊥ = ⊥ := map₂_eq_bot_iff.2 <| .inr rfl
+#align filter.map₂_bot_right Filter.map₂_bot_right
 
 @[simp]
-theorem map₂_neBot_iff : (map₂ m f g).NeBot ↔ f.NeBot ∧ g.NeBot := by
-  simp_rw [neBot_iff]
-  exact map₂_eq_bot_iff.not.trans not_or
+theorem map₂_neBot_iff : (map₂ m f g).NeBot ↔ f.NeBot ∧ g.NeBot := by simp [neBot_iff, not_or]
 #align filter.map₂_ne_bot_iff Filter.map₂_neBot_iff
 
-theorem NeBot.map₂ (hf : f.NeBot) (hg : g.NeBot) : (map₂ m f g).NeBot :=
+protected theorem NeBot.map₂ (hf : f.NeBot) (hg : g.NeBot) : (map₂ m f g).NeBot :=
   map₂_neBot_iff.2 ⟨hf, hg⟩
 #align filter.ne_bot.map₂ Filter.NeBot.map₂
 
--- Porting note: Why do I have to specify the `Filter` namespace for `map₂` here?
-theorem NeBot.of_map₂_left (h : (Filter.map₂ m f g).NeBot) : f.NeBot :=
+instance map₂.neBot [NeBot f] [NeBot g] : NeBot (map₂ m f g) := .map₂ ‹_› ‹_›
+
+theorem NeBot.of_map₂_left (h : (map₂ m f g).NeBot) : f.NeBot :=
   (map₂_neBot_iff.1 h).1
 #align filter.ne_bot.of_map₂_left Filter.NeBot.of_map₂_left
 
-theorem NeBot.of_map₂_right (h : (Filter.map₂ m f g).NeBot) : g.NeBot :=
+theorem NeBot.of_map₂_right (h : (map₂ m f g).NeBot) : g.NeBot :=
   (map₂_neBot_iff.1 h).2
 #align filter.ne_bot.of_map₂_right Filter.NeBot.of_map₂_right
 
 theorem map₂_sup_left : map₂ m (f₁ ⊔ f₂) g = map₂ m f₁ g ⊔ map₂ m f₂ g := by
-  ext u
-  constructor
-  · rintro ⟨s, t, ⟨h₁, h₂⟩, ht, hu⟩
-    exact ⟨mem_of_superset (image2_mem_map₂ h₁ ht) hu, mem_of_superset (image2_mem_map₂ h₂ ht) hu⟩
-  · rintro ⟨⟨s₁, t₁, hs₁, ht₁, hu₁⟩, s₂, t₂, hs₂, ht₂, hu₂⟩
-    refine' ⟨s₁ ∪ s₂, t₁ ∩ t₂, union_mem_sup hs₁ hs₂, inter_mem ht₁ ht₂, _⟩
-    rw [image2_union_left]
-    exact
-      union_subset ((image2_subset_left <| inter_subset_left _ _).trans hu₁)
-        ((image2_subset_left <| inter_subset_right _ _).trans hu₂)
+  simp_rw [← map_prod_eq_map₂, sup_prod, map_sup]
 #align filter.map₂_sup_left Filter.map₂_sup_left
 
 theorem map₂_sup_right : map₂ m f (g₁ ⊔ g₂) = map₂ m f g₁ ⊔ map₂ m f g₂ := by
-  ext u
-  constructor
-  · rintro ⟨s, t, hs, ⟨h₁, h₂⟩, hu⟩
-    exact ⟨mem_of_superset (image2_mem_map₂ hs h₁) hu, mem_of_superset (image2_mem_map₂ hs h₂) hu⟩
-  · rintro ⟨⟨s₁, t₁, hs₁, ht₁, hu₁⟩, s₂, t₂, hs₂, ht₂, hu₂⟩
-    refine' ⟨s₁ ∩ s₂, t₁ ∪ t₂, inter_mem hs₁ hs₂, union_mem_sup ht₁ ht₂, _⟩
-    rw [image2_union_right]
-    exact
-      union_subset ((image2_subset_right <| inter_subset_left _ _).trans hu₁)
-        ((image2_subset_right <| inter_subset_right _ _).trans hu₂)
+  simp_rw [← map_prod_eq_map₂, prod_sup, map_sup]
 #align filter.map₂_sup_right Filter.map₂_sup_right
 
 theorem map₂_inf_subset_left : map₂ m (f₁ ⊓ f₂) g ≤ map₂ m f₁ g ⊓ map₂ m f₂ g :=
-  le_inf (map₂_mono_right inf_le_left) (map₂_mono_right inf_le_right)
+  Monotone.map_inf_le (fun _ _ ↦ map₂_mono_right) f₁ f₂
 #align filter.map₂_inf_subset_left Filter.map₂_inf_subset_left
 
 theorem map₂_inf_subset_right : map₂ m f (g₁ ⊓ g₂) ≤ map₂ m f g₁ ⊓ map₂ m f g₂ :=
-  le_inf (map₂_mono_left inf_le_left) (map₂_mono_left inf_le_right)
+  Monotone.map_inf_le (fun _ _ ↦ map₂_mono_left) g₁ g₂
 #align filter.map₂_inf_subset_right Filter.map₂_inf_subset_right
 
 @[simp]
-theorem map₂_pure_left : map₂ m (pure a) g = g.map fun b => m a b :=
-  Filter.ext fun u =>
-    ⟨fun ⟨s, t, hs, ht, hu⟩ =>
-      mem_of_superset (image_mem_map ht) ((image_subset_image2_right <| mem_pure.1 hs).trans hu),
-      fun h => ⟨{a}, _, singleton_mem_pure, h, by rw [image2_singleton_left, image_subset_iff]⟩⟩
+theorem map₂_pure_left : map₂ m (pure a) g = g.map (m a) := by
+  rw [← map_prod_eq_map₂, pure_prod, map_map]; rfl
 #align filter.map₂_pure_left Filter.map₂_pure_left
 
 @[simp]
-theorem map₂_pure_right : map₂ m f (pure b) = f.map fun a => m a b :=
-  Filter.ext fun u =>
-    ⟨fun ⟨s, t, hs, ht, hu⟩ =>
-      mem_of_superset (image_mem_map hs) ((image_subset_image2_left <| mem_pure.1 ht).trans hu),
-      fun h => ⟨_, {b}, h, singleton_mem_pure, by rw [image2_singleton_right, image_subset_iff]⟩⟩
+theorem map₂_pure_right : map₂ m f (pure b) = f.map (m · b) := by
+  rw [← map_prod_eq_map₂, prod_pure, map_map]; rfl
 #align filter.map₂_pure_right Filter.map₂_pure_right
 
 theorem map₂_pure : map₂ m (pure a) (pure b) = pure (m a b) := by rw [map₂_pure_right, map_pure]
@@ -200,23 +165,18 @@ theorem map₂_swap (m : α → β → γ) (f : Filter α) (g : Filter β) :
 #align filter.map₂_swap Filter.map₂_swap
 
 @[simp]
-theorem map₂_left (h : g.NeBot) : map₂ (fun x _ => x) f g = f := by
-  ext u
-  refine' ⟨_, fun hu => ⟨_, _, hu, univ_mem, (image2_left <| h.nonempty_of_mem univ_mem).subset⟩⟩
-  rintro ⟨s, t, hs, ht, hu⟩
-  rw [image2_left (h.nonempty_of_mem ht)] at hu
-  exact mem_of_superset hs hu
+theorem map₂_left [NeBot g] : map₂ (fun x _ => x) f g = f := by
+  rw [← map_prod_eq_map₂, map_fst_prod]
 #align filter.map₂_left Filter.map₂_left
 
 @[simp]
-theorem map₂_right (h : f.NeBot) : map₂ (fun _ y => y) f g = g := by rw [map₂_swap, map₂_left h]
+theorem map₂_right [NeBot f] : map₂ (fun _ y => y) f g = g := by rw [map₂_swap, map₂_left]
 #align filter.map₂_right Filter.map₂_right
 
 /-- The image of a ternary function `m : α → β → γ → δ` as a function
 `Filter α → Filter β → Filter γ → Filter δ`. Mathematically this should be thought of as the image
 of the corresponding function `α × β × γ → δ`. -/
-def map₃ (m : α → β → γ → δ) (f : Filter α) (g : Filter β) (h : Filter γ) : Filter δ
-    where
+def map₃ (m : α → β → γ → δ) (f : Filter α) (g : Filter β) (h : Filter γ) : Filter δ where
   sets := { s | ∃ u v w, u ∈ f ∧ v ∈ g ∧ w ∈ h ∧ image3 m u v w ⊆ s }
   univ_sets := ⟨univ, univ, univ, univ_sets _, univ_sets _, univ_sets _, subset_univ _⟩
   sets_of_superset hs hst :=

Mathlib/Order/Filter/Pointwise.lean

@@ -102,13 +102,13 @@ theorem principal_one : 𝓟 1 = (1 : Filter α) :=
 #align filter.principal_one Filter.principal_one
 #align filter.principal_zero Filter.principal_zero
 
-@[to_additive] -- TODO: make this a scoped instance in the `Pointwise` namespace
+@[to_additive]
 theorem one_neBot : (1 : Filter α).NeBot :=
   Filter.pure_neBot
 #align filter.one_ne_bot Filter.one_neBot
 #align filter.zero_ne_bot Filter.zero_neBot
 
-scoped[Pointwise] attribute [instance] Filter.one_neBot
+scoped[Pointwise] attribute [instance] one_neBot zero_neBot
 
 @[to_additive (attr := simp)]
 protected theorem map_one' (f : α → β) : (1 : Filter α).map f = pure (f 1) :=
@@ -224,10 +224,15 @@ theorem neBot_inv_iff : f⁻¹.NeBot ↔ NeBot f :=
 #align filter.ne_bot_neg_iff Filter.neBot_neg_iff
 
 @[to_additive]
-theorem NeBot.inv : f.NeBot → f⁻¹.NeBot := fun h => h.map _
+protected theorem NeBot.inv : f.NeBot → f⁻¹.NeBot := fun h => h.map _
 #align filter.ne_bot.inv Filter.NeBot.inv
 #align filter.ne_bot.neg Filter.NeBot.neg
 
+@[to_additive neg.instNeBot]
+lemma inv.instNeBot [NeBot f] : NeBot f⁻¹ := .inv ‹_›
+
+scoped[Pointwise] attribute [instance] inv.instNeBot neg.instNeBot
+
 end Inv
 
 section InvolutiveInv
@@ -336,7 +341,7 @@ lemma mul_neBot_iff : (f * g).NeBot ↔ f.NeBot ∧ g.NeBot :=
 #align filter.add_ne_bot_iff Filter.add_neBot_iff
 
 @[to_additive]
-theorem NeBot.mul : NeBot f → NeBot g → NeBot (f * g) :=
+protected theorem NeBot.mul : NeBot f → NeBot g → NeBot (f * g) :=
   NeBot.map₂
 #align filter.ne_bot.mul Filter.NeBot.mul
 #align filter.ne_bot.add Filter.NeBot.add
@@ -353,6 +358,11 @@ theorem NeBot.of_mul_right : (f * g).NeBot → g.NeBot :=
 #align filter.ne_bot.of_mul_right Filter.NeBot.of_mul_right
 #align filter.ne_bot.of_add_right Filter.NeBot.of_add_right
 
+@[to_additive add.instNeBot]
+protected lemma mul.instNeBot [NeBot f] [NeBot g] : NeBot (f * g) := .mul ‹_› ‹_›
+
+scoped[Pointwise] attribute [instance] mul.instNeBot add.instNeBot
+
 @[to_additive (attr := simp)]
 theorem pure_mul : pure a * g = g.map (a * ·) :=
   map₂_pure_left
@@ -418,7 +428,6 @@ end Mul
 
 /-! ### Filter subtraction/division -/
 
-
 section Div
 
 variable [Div α] {f f₁ f₂ g g₁ g₂ h : Filter α} {s t : Set α} {a b : α}
@@ -470,14 +479,14 @@ theorem div_eq_bot_iff : f / g = ⊥ ↔ f = ⊥ ∨ g = ⊥ :=
 #align filter.div_eq_bot_iff Filter.div_eq_bot_iff
 #align filter.sub_eq_bot_iff Filter.sub_eq_bot_iff
 
-@[to_additive (attr := simp)] -- TODO: make this a scoped instance in the `Pointwise` namespace
+@[to_additive (attr := simp)]
 theorem div_neBot_iff : (f / g).NeBot ↔ f.NeBot ∧ g.NeBot :=
   map₂_neBot_iff
 #align filter.div_ne_bot_iff Filter.div_neBot_iff
 #align filter.sub_ne_bot_iff Filter.sub_neBot_iff
 
 @[to_additive]
-theorem NeBot.div : NeBot f → NeBot g → NeBot (f / g) :=
+protected theorem NeBot.div : NeBot f → NeBot g → NeBot (f / g) :=
   NeBot.map₂
 #align filter.ne_bot.div Filter.NeBot.div
 #align filter.ne_bot.sub Filter.NeBot.sub
@@ -494,6 +503,11 @@ theorem NeBot.of_div_right : (f / g).NeBot → g.NeBot :=
 #align filter.ne_bot.of_div_right Filter.NeBot.of_div_right
 #align filter.ne_bot.of_sub_right Filter.NeBot.of_sub_right
 
+@[to_additive sub.instNeBot]
+lemma div.instNeBot [NeBot f] [NeBot g] : NeBot (f / g) := .div ‹_› ‹_›
+
+scoped[Pointwise] attribute [instance] div.instNeBot sub.instNeBot
+
 @[to_additive (attr := simp)]
 theorem pure_div : pure a / g = g.map (a / ·) :=
   map₂_pure_left
@@ -832,7 +846,6 @@ variable [MulZeroClass α] {f g : Filter α}
 
 /-! Note that `Filter` is not a `MulZeroClass` because `0 * ⊥ ≠ 0`. -/
 
-
 theorem NeBot.mul_zero_nonneg (hf : f.NeBot) : 0 ≤ f * 0 :=
   le_mul_iff.2 fun _ h₁ _ h₂ =>
     let ⟨_, ha⟩ := hf.nonempty_of_mem h₁
@@ -1001,7 +1014,7 @@ theorem smul_neBot_iff : (f • g).NeBot ↔ f.NeBot ∧ g.NeBot :=
 #align filter.vadd_ne_bot_iff Filter.vadd_neBot_iff
 
 @[to_additive]
-theorem NeBot.smul : NeBot f → NeBot g → NeBot (f • g) :=
+protected theorem NeBot.smul : NeBot f → NeBot g → NeBot (f • g) :=
   NeBot.map₂
 #align filter.ne_bot.smul Filter.NeBot.smul
 #align filter.ne_bot.vadd Filter.NeBot.vadd
@@ -1018,6 +1031,11 @@ theorem NeBot.of_smul_right : (f • g).NeBot → g.NeBot :=
 #align filter.ne_bot.of_smul_right Filter.NeBot.of_smul_right
 #align filter.ne_bot.of_vadd_right Filter.NeBot.of_vadd_right
 
+@[to_additive vadd.instNeBot]
+lemma smul.instNeBot [NeBot f] [NeBot g] : NeBot (f • g) := .smul ‹_› ‹_›
+
+scoped[Pointwise] attribute [instance] smul.instNeBot vadd.instNeBot
+
 @[to_additive (attr := simp)]
 theorem pure_smul : (pure a : Filter α) • g = g.map (a • ·) :=
   map₂_pure_left
@@ -1117,7 +1135,7 @@ theorem vsub_neBot_iff : (f -ᵥ g : Filter α).NeBot ↔ f.NeBot ∧ g.NeBot :=
   map₂_neBot_iff
 #align filter.vsub_ne_bot_iff Filter.vsub_neBot_iff
 
-theorem NeBot.vsub : NeBot f → NeBot g → NeBot (f -ᵥ g) :=
+protected theorem NeBot.vsub : NeBot f → NeBot g → NeBot (f -ᵥ g) :=
   NeBot.map₂
 #align filter.ne_bot.vsub Filter.NeBot.vsub
 
@@ -1129,6 +1147,10 @@ theorem NeBot.of_vsub_right : (f -ᵥ g : Filter α).NeBot → g.NeBot :=
   NeBot.of_map₂_right
 #align filter.ne_bot.of_vsub_right Filter.NeBot.of_vsub_right
 
+lemma vsub.instNeBot [NeBot f] [NeBot g] : NeBot (f -ᵥ g) := .vsub ‹_› ‹_›
+
+scoped[Pointwise] attribute [instance] vsub.instNeBot
+
 @[simp]
 theorem pure_vsub : (pure a : Filter β) -ᵥ g = g.map (a -ᵥ ·) :=
   map₂_pure_left
@@ -1225,6 +1247,11 @@ theorem NeBot.of_smul_filter : (a • f).NeBot → f.NeBot :=
 #align filter.ne_bot.of_smul_filter Filter.NeBot.of_smul_filter
 #align filter.ne_bot.of_vadd_filter Filter.NeBot.of_vadd_filter
 
+@[to_additive vadd_filter.instNeBot]
+lemma smul_filter.instNeBot [NeBot f] : NeBot (a • f) := .smul_filter ‹_›
+
+scoped[Pointwise] attribute [instance] smul_filter.instNeBot vadd_filter.instNeBot
+
 @[to_additive]
 theorem smul_filter_le_smul_filter (hf : f₁ ≤ f₂) : a • f₁ ≤ a • f₂ :=
   map_mono hf
@@ -1350,7 +1377,6 @@ Note that we have neither `SMulWithZero α (Filter β)` nor `SMulWithZero (Filte
 because `0 * ⊥ ≠ 0`.
 -/
 
-
 theorem NeBot.smul_zero_nonneg (hf : f.NeBot) : 0 ≤ f • (0 : Filter β) :=
   le_smul_iff.2 fun _ h₁ _ h₂ =>
     let ⟨_, ha⟩ := hf.nonempty_of_mem h₁

Mathlib/Order/Filter/Prod.lean

@@ -413,6 +413,7 @@ theorem prod_pure_pure {a : α} {b : β} :
     (pure a : Filter α) ×ˢ (pure b : Filter β) = pure (a, b) := by simp
 #align filter.prod_pure_pure Filter.prod_pure_pure
 
+@[simp]
 theorem prod_eq_bot : f ×ˢ g = ⊥ ↔ f = ⊥ ∨ g = ⊥ := by
   simp_rw [← empty_mem_iff_bot, mem_prod_iff, subset_empty_iff, prod_eq_empty_iff, ← exists_prop,
     Subtype.exists', exists_or, exists_const, Subtype.exists, exists_prop, exists_eq_right]
@@ -428,11 +429,11 @@ theorem prod_neBot : NeBot (f ×ˢ g) ↔ NeBot f ∧ NeBot g := by
   simp only [neBot_iff, Ne, prod_eq_bot, not_or]
 #align filter.prod_ne_bot Filter.prod_neBot
 
-theorem NeBot.prod (hf : NeBot f) (hg : NeBot g) : NeBot (f ×ˢ g) := prod_neBot.2 ⟨hf, hg⟩
+protected theorem NeBot.prod (hf : NeBot f) (hg : NeBot g) : NeBot (f ×ˢ g) := prod_neBot.2 ⟨hf, hg⟩
 #align filter.ne_bot.prod Filter.NeBot.prod
 
-instance prod_neBot' [hf : NeBot f] [hg : NeBot g] : NeBot (f ×ˢ g) := hf.prod hg
-#align filter.prod_ne_bot' Filter.prod_neBot'
+instance prod.instNeBot [hf : NeBot f] [hg : NeBot g] : NeBot (f ×ˢ g) := hf.prod hg
+#align filter.prod_ne_bot' Filter.prod.instNeBot
 
 @[simp]
 lemma disjoint_prod {f' : Filter α} {g' : Filter β} :