chore(Topology/Order/LeftRight): use to_dual (#35637)

This overlaps with #35635, but the overlap is small (and that PR still needs some work, so I'd rather get this out of the way first).

Author: vihdzp

Mathlib/Order/Interval/Set/LinearOrder.lean

@@ -156,31 +156,35 @@ theorem Iio_subset_Iic_iff [DenselyOrdered α] : Iio a ⊆ Iic b ↔ a ≤ b :=
 
 /-! ### Two infinite intervals -/
 
+@[to_dual]
 theorem Iic_union_Ioi_of_le (h : a ≤ b) : Iic b ∪ Ioi a = univ :=
   eq_univ_of_forall fun x => (h.gt_or_le x).symm
 
+@[to_dual]
 theorem Iio_union_Ici_of_le (h : a ≤ b) : Iio b ∪ Ici a = univ :=
   eq_univ_of_forall fun x => (h.ge_or_lt x).symm
 
+@[to_dual]
 theorem Iic_union_Ici_of_le (h : a ≤ b) : Iic b ∪ Ici a = univ :=
   eq_univ_of_forall fun x => (h.ge_or_le x).symm
 
+@[to_dual]
 theorem Iio_union_Ioi_of_lt (h : a < b) : Iio b ∪ Ioi a = univ :=
   eq_univ_of_forall fun x => (h.gt_or_lt x).symm
 
-@[simp]
+@[to_dual (attr := simp)]
 theorem Iic_union_Ici : Iic a ∪ Ici a = univ :=
   Iic_union_Ici_of_le le_rfl
 
-@[simp]
+@[to_dual (attr := simp)]
 theorem Iio_union_Ici : Iio a ∪ Ici a = univ :=
   Iio_union_Ici_of_le le_rfl
 
-@[simp]
+@[to_dual (attr := simp)]
 theorem Iic_union_Ioi : Iic a ∪ Ioi a = univ :=
   Iic_union_Ioi_of_le le_rfl
 
-@[simp]
+@[to_dual (attr := simp)]
 theorem Iio_union_Ioi : Iio a ∪ Ioi a = {a}ᶜ :=
   ext fun _ => lt_or_lt_iff_ne
 

Mathlib/Tactic/Translate/ToDual.lean

@@ -227,6 +227,11 @@ def abbreviationDict : Std.HashMap String String := .ofList [
   ("predColimit", "PredLimit"),
   ("codirectedOrder", "DirectedOrder"),
   ("directedOrder", "CodirectedOrder"),
+  ("nhdsLT", "NhdsGT"),
+  ("nhdsGT", "NhdsLT"),
+  ("nhdsLE", "NhdsGE"),
+  ("nhdsGE", "NhdsLE"),
+  ("neTop", "NeBot")
 ]
 
 /-- The bundle of environment extensions for `to_dual` -/

Mathlib/Topology/Order/LeftRight.lean

@@ -35,35 +35,26 @@ section Preorder
 
 variable {α : Type*} [TopologicalSpace α] [Preorder α]
 
+@[to_dual frequently_gt_nhds]
 lemma frequently_lt_nhds (a : α) [NeBot (𝓝[<] a)] : ∃ᶠ x in 𝓝 a, x < a :=
   frequently_iff_neBot.2 ‹_›
 
-lemma frequently_gt_nhds (a : α) [NeBot (𝓝[>] a)] : ∃ᶠ x in 𝓝 a, a < x :=
-  frequently_iff_neBot.2 ‹_›
-
+@[to_dual exists_gt]
 theorem Filter.Eventually.exists_lt {a : α} [NeBot (𝓝[<] a)] {p : α → Prop}
     (h : ∀ᶠ x in 𝓝 a, p x) : ∃ b < a, p b :=
   ((frequently_lt_nhds a).and_eventually h).exists
 
-theorem Filter.Eventually.exists_gt {a : α} [NeBot (𝓝[>] a)] {p : α → Prop}
-    (h : ∀ᶠ x in 𝓝 a, p x) : ∃ b > a, p b :=
-  ((frequently_gt_nhds a).and_eventually h).exists
-
+@[to_dual]
 theorem nhdsWithin_Ici_neBot {a b : α} (H₂ : a ≤ b) : NeBot (𝓝[Ici a] b) :=
   nhdsWithin_neBot_of_mem H₂
 
-instance nhdsGE_neBot (a : α) : NeBot (𝓝[≥] a) := nhdsWithin_Ici_neBot (le_refl a)
-
-theorem nhdsWithin_Iic_neBot {a b : α} (H : a ≤ b) : NeBot (𝓝[Iic b] a) :=
-  nhdsWithin_neBot_of_mem H
-
+@[to_dual]
 instance nhdsLE_neBot (a : α) : NeBot (𝓝[≤] a) := nhdsWithin_Iic_neBot (le_refl a)
 
+@[to_dual]
 theorem nhdsLT_le_nhdsNE (a : α) : 𝓝[<] a ≤ 𝓝[≠] a :=
   nhdsWithin_mono a fun _ => ne_of_lt
 
-theorem nhdsGT_le_nhdsNE (a : α) : 𝓝[>] a ≤ 𝓝[≠] a := nhdsWithin_mono a fun _ => ne_of_gt
-
 -- TODO: add instances for `NeBot (𝓝[<] x)` on (indexed) product types
 
 lemma IsAntichain.interior_eq_empty [∀ x : α, (𝓝[<] x).NeBot] {s : Set α}
@@ -84,54 +75,57 @@ section PartialOrder
 
 variable {α β : Type*} [TopologicalSpace α] [PartialOrder α] [TopologicalSpace β]
 
+@[to_dual]
 theorem continuousWithinAt_Ioi_iff_Ici {a : α} {f : α → β} :
     ContinuousWithinAt f (Ioi a) a ↔ ContinuousWithinAt f (Ici a) a := by
   simp only [← Ici_diff_left, continuousWithinAt_diff_self]
 
-theorem continuousWithinAt_Iio_iff_Iic {a : α} {f : α → β} :
-    ContinuousWithinAt f (Iio a) a ↔ ContinuousWithinAt f (Iic a) a :=
-  continuousWithinAt_Ioi_iff_Ici (α := αᵒᵈ)
-
+@[to_dual]
 theorem continuousWithinAt_inter_Ioi_iff_Ici {a : α} {f : α → β} {s : Set α} :
     ContinuousWithinAt f (s ∩ Ioi a) a ↔ ContinuousWithinAt f (s ∩ Ici a) a := by
   simp [← Ici_diff_left, ← inter_diff_assoc, continuousWithinAt_diff_self]
 
-theorem continuousWithinAt_inter_Iio_iff_Iic {a : α} {f : α → β} {s : Set α} :
-    ContinuousWithinAt f (s ∩ Iio a) a ↔ ContinuousWithinAt f (s ∩ Iic a) a :=
-  continuousWithinAt_inter_Ioi_iff_Ici (α := αᵒᵈ)
-
 end PartialOrder
 
 section TopologicalSpace
 
 variable {α β : Type*} [TopologicalSpace α] [LinearOrder α] [TopologicalSpace β] {s : Set α}
 
+@[to_dual nhdsGE_sup_nhdsLE]
 theorem nhdsLE_sup_nhdsGE (a : α) : 𝓝[≤] a ⊔ 𝓝[≥] a = 𝓝 a := by
   rw [← nhdsWithin_union, Iic_union_Ici, nhdsWithin_univ]
 
+@[to_dual nhdsWithinGE_sup_nhdsWithinLE]
 theorem nhdsWithinLE_sup_nhdsWithinGE (a : α) : 𝓝[s ∩ Iic a] a ⊔ 𝓝[s ∩ Ici a] a = 𝓝[s] a := by
   rw [← nhdsWithin_union, ← inter_union_distrib_left, Iic_union_Ici, inter_univ]
 
+@[to_dual nhdsGT_sup_nhdsLE]
 theorem nhdsLT_sup_nhdsGE (a : α) : 𝓝[<] a ⊔ 𝓝[≥] a = 𝓝 a := by
   rw [← nhdsWithin_union, Iio_union_Ici, nhdsWithin_univ]
 
+@[to_dual nhdsWithinGT_sup_nhdsWithinLE]
 theorem nhdsWithinLT_sup_nhdsWithinGE (a : α) : 𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ici a] a = 𝓝[s] a := by
   rw [← nhdsWithin_union, ← inter_union_distrib_left, Iio_union_Ici, inter_univ]
 
+@[to_dual nhdsGE_sup_nhdsLT]
 theorem nhdsLE_sup_nhdsGT (a : α) : 𝓝[≤] a ⊔ 𝓝[>] a = 𝓝 a := by
   rw [← nhdsWithin_union, Iic_union_Ioi, nhdsWithin_univ]
 
+@[to_dual nhdsWithinGE_sup_nhdsWithinLT]
 theorem nhdsWithinLE_sup_nhdsWithinGT (a : α) : 𝓝[s ∩ Iic a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[s] a := by
   rw [← nhdsWithin_union, ← inter_union_distrib_left, Iic_union_Ioi, inter_univ]
 
+@[to_dual nhdsGT_sup_nhdsLT]
 theorem nhdsLT_sup_nhdsGT (a : α) : 𝓝[<] a ⊔ 𝓝[>] a = 𝓝[≠] a := by
   rw [← nhdsWithin_union, Iio_union_Ioi]
 
+@[to_dual nhdsWithinGT_sup_nhdsWithinLT]
 theorem nhdsWithinLT_sup_nhdsWithinGT (a : α) :
     𝓝[s ∩ Iio a] a ⊔ 𝓝[s ∩ Ioi a] a = 𝓝[s \ {a}] a := by
   rw [← nhdsWithin_union, ← inter_union_distrib_left, Iio_union_Ioi, compl_eq_univ_diff,
     inter_sdiff_left_comm, univ_inter]
 
+@[to_dual nhdsLT_sup_nhdsWithin_singleton]
 lemma nhdsGT_sup_nhdsWithin_singleton (a : α) :
     𝓝[>] a ⊔ 𝓝[{a}] a = 𝓝[≥] a := by
   simp only [union_singleton, Ioi_insert, ← nhdsWithin_union]
@@ -142,20 +136,24 @@ lemma nhdsWithin_uIoo_left_le_nhdsNE {a b : α} : 𝓝[uIoo a b] a ≤ 𝓝[≠]
 lemma nhdsWithin_uIoo_right_le_nhdsNE {a b : α} : 𝓝[uIoo a b] b ≤ 𝓝[≠] b :=
   nhdsWithin_mono _ (by simp)
 
+@[to_dual none]
 theorem continuousAt_iff_continuous_left_right {a : α} {f : α → β} :
     ContinuousAt f a ↔ ContinuousWithinAt f (Iic a) a ∧ ContinuousWithinAt f (Ici a) a := by
   simp only [ContinuousWithinAt, ContinuousAt, ← tendsto_sup, nhdsLE_sup_nhdsGE]
 
+@[to_dual none]
 theorem continuousAt_iff_continuous_left'_right' {a : α} {f : α → β} :
     ContinuousAt f a ↔ ContinuousWithinAt f (Iio a) a ∧ ContinuousWithinAt f (Ioi a) a := by
   rw [continuousWithinAt_Ioi_iff_Ici, continuousWithinAt_Iio_iff_Iic,
     continuousAt_iff_continuous_left_right]
 
+@[to_dual none]
 theorem continuousWithinAt_iff_continuous_left_right {a : α} {f : α → β} :
     ContinuousWithinAt f s a ↔
       ContinuousWithinAt f (s ∩ Iic a) a ∧ ContinuousWithinAt f (s ∩ Ici a) a := by
   simp only [ContinuousWithinAt, ← tendsto_sup, nhdsWithinLE_sup_nhdsWithinGE]
 
+@[to_dual none]
 theorem continuousWithinAt_iff_continuous_left'_right' {a : α} {f : α → β} :
     ContinuousWithinAt f s a ↔
       ContinuousWithinAt f (s ∩ Iio a) a ∧ ContinuousWithinAt f (s ∩ Ioi a) a := by