chore(Order/Interval/Set/WithBotTop): use to_dual (leanprover-community#38240)

Author: vihdzp

Mathlib/Order/Cover.lean

@@ -315,6 +315,7 @@ instance CovBy.irrefl : @Std.Irrefl α (· ⋖ ·) :=
 theorem CovBy.Ioo_eq (h : a ⋖ b) : Ioo a b = ∅ :=
   h.wcovBy.Ioo_eq
 
+@[to_dual self]
 theorem covBy_iff_Ioo_eq : a ⋖ b ↔ a < b ∧ Ioo a b = ∅ :=
   and_congr_right' <| by simp [eq_empty_iff_forall_notMem]
 
@@ -739,44 +740,26 @@ namespace WithTop
 
 variable [Preorder α] {a b : α}
 
-@[simp, norm_cast] lemma coe_wcovBy_coe : (a : WithTop α) ⩿ b ↔ a ⩿ b :=
+@[to_dual (attr := simp, norm_cast)]
+lemma coe_wcovBy_coe : (a : WithTop α) ⩿ b ↔ a ⩿ b :=
   Set.OrdConnected.apply_wcovBy_apply_iff WithTop.coeOrderHom <| by
     simp [WithTop.range_coe, ordConnected_Iio]
 
-@[simp, norm_cast] lemma coe_covBy_coe : (a : WithTop α) ⋖ b ↔ a ⋖ b :=
+@[to_dual (attr := simp, norm_cast)]
+lemma coe_covBy_coe : (a : WithTop α) ⋖ b ↔ a ⋖ b :=
   Set.OrdConnected.apply_covBy_apply_iff WithTop.coeOrderHom <| by
     simp [WithTop.range_coe, ordConnected_Iio]
 
-@[simp] lemma coe_covBy_top : (a : WithTop α) ⋖ ⊤ ↔ IsMax a := by
-  simp only [covBy_iff_Ioo_eq, ← image_coe_Ioi, coe_lt_top, image_eq_empty,
-    true_and, Ioi_eq_empty_iff]
+@[to_dual (attr := simp) bot_covBy_coe]
+lemma coe_covBy_top : (a : WithTop α) ⋖ ⊤ ↔ IsMax a := by
+  simp [covBy_iff_Ioo_eq, ← image_coe_Ioi]
 
-@[simp] lemma coe_wcovBy_top : (a : WithTop α) ⩿ ⊤ ↔ IsMax a := by
+@[to_dual (attr := simp) bot_wcovBy_coe]
+lemma coe_wcovBy_top : (a : WithTop α) ⩿ ⊤ ↔ IsMax a := by
   simp only [wcovBy_iff_Ioo_eq, ← image_coe_Ioi, le_top, image_eq_empty, true_and, Ioi_eq_empty_iff]
 
 end WithTop
 
-namespace WithBot
-
-variable [Preorder α] {a b : α}
-
-@[simp, norm_cast] lemma coe_wcovBy_coe : (a : WithBot α) ⩿ b ↔ a ⩿ b :=
-  Set.OrdConnected.apply_wcovBy_apply_iff WithBot.coeOrderHom <| by
-    simp [WithBot.range_coe, ordConnected_Ioi]
-
-@[simp, norm_cast] lemma coe_covBy_coe : (a : WithBot α) ⋖ b ↔ a ⋖ b :=
-  Set.OrdConnected.apply_covBy_apply_iff WithBot.coeOrderHom <| by
-    simp [WithBot.range_coe, ordConnected_Ioi]
-
-@[simp] lemma bot_covBy_coe : ⊥ ⋖ (a : WithBot α) ↔ IsMin a := by
-  simp only [covBy_iff_Ioo_eq, ← image_coe_Iio, bot_lt_coe, image_eq_empty,
-    true_and, Iio_eq_empty_iff]
-
-@[simp] lemma bot_wcovBy_coe : ⊥ ⩿ (a : WithBot α) ↔ IsMin a := by
-  simp only [wcovBy_iff_Ioo_eq, ← image_coe_Iio, bot_le, image_eq_empty, true_and, Iio_eq_empty_iff]
-
-end WithBot
-
 section WellFounded
 
 variable [Preorder α]

Mathlib/Order/Interval/Set/Defs.lean

@@ -88,6 +88,7 @@ class OrdConnected (s : Set α) : Prop where
   /-- `s : Set α` is `OrdConnected` if for all `x y ∈ s` it includes the interval `[[x, y]]`. -/
   out' ⦃x : α⦄ (hx : x ∈ s) ⦃y : α⦄ (hy : y ∈ s) : Icc x y ⊆ s
 
+attribute [to_dual self (reorder := out' (x y, hx hy))] OrdConnected.mk
 attribute [to_dual self (reorder := x y, hx hy)] OrdConnected.out'
 
 end Set

Mathlib/Order/Interval/Set/OrdConnected.lean

@@ -165,36 +165,24 @@ instance ordConnected_pi' {ι : Type*} {α : ι → Type*} [∀ i, Preorder (α
     {t : ∀ i, Set (α i)} [h : ∀ i, OrdConnected (t i)] : OrdConnected (s.pi t) :=
   ordConnected_pi fun i _ => h i
 
-@[instance]
-theorem ordConnected_Ici {a : α} : OrdConnected (Ici a) :=
+@[to_dual]
+instance ordConnected_Ici {a : α} : OrdConnected (Ici a) :=
   ⟨fun _ hx _ _ _ hz => le_trans hx hz.1⟩
 
-@[instance]
-theorem ordConnected_Iic {a : α} : OrdConnected (Iic a) :=
-  ⟨fun _ _ _ hy _ hz => le_trans hz.2 hy⟩
-
-@[instance]
-theorem ordConnected_Ioi {a : α} : OrdConnected (Ioi a) :=
+@[to_dual]
+instance ordConnected_Ioi {a : α} : OrdConnected (Ioi a) :=
   ⟨fun _ hx _ _ _ hz => lt_of_lt_of_le hx hz.1⟩
 
-@[instance]
-theorem ordConnected_Iio {a : α} : OrdConnected (Iio a) :=
-  ⟨fun _ _ _ hy _ hz => lt_of_le_of_lt hz.2 hy⟩
-
-@[instance]
-theorem ordConnected_Icc {a b : α} : OrdConnected (Icc a b) :=
+@[to_dual self]
+instance ordConnected_Icc {a b : α} : OrdConnected (Icc a b) :=
   ordConnected_Ici.inter ordConnected_Iic
 
-@[instance]
-theorem ordConnected_Ico {a b : α} : OrdConnected (Ico a b) :=
+@[to_dual]
+instance ordConnected_Ico {a b : α} : OrdConnected (Ico a b) :=
   ordConnected_Ici.inter ordConnected_Iio
 
-@[instance]
-theorem ordConnected_Ioc {a b : α} : OrdConnected (Ioc a b) :=
-  ordConnected_Ioi.inter ordConnected_Iic
-
-@[instance]
-theorem ordConnected_Ioo {a b : α} : OrdConnected (Ioo a b) :=
+@[to_dual self]
+instance ordConnected_Ioo {a b : α} : OrdConnected (Ioo a b) :=
   ordConnected_Ioi.inter ordConnected_Iio
 
 @[instance]

Mathlib/Order/Interval/Set/WithBotTop.lean

@@ -22,212 +22,122 @@ open Set
 
 variable {α : Type*}
 
-/-! ### `WithTop` -/
-
 namespace WithTop
 
-@[simp]
+@[to_dual (attr := simp)]
 theorem preimage_coe_top : (some : α → WithTop α) ⁻¹' {⊤} = (∅ : Set α) :=
   eq_empty_of_subset_empty fun _ => coe_ne_top
 
 variable [Preorder α] {a b : α}
 
+@[to_dual]
 theorem range_coe : range (some : α → WithTop α) = Iio ⊤ := by
   ext; simp [mem_range, WithTop.lt_top_iff_ne_top, ne_top_iff_exists]
 
-@[simp]
+@[to_dual (attr := simp)]
 theorem preimage_coe_Ioi : (some : α → WithTop α) ⁻¹' Ioi a = Ioi a :=
   ext fun _ => coe_lt_coe
 
-@[simp]
+@[to_dual (attr := simp)]
 theorem preimage_coe_Ici : (some : α → WithTop α) ⁻¹' Ici a = Ici a :=
   ext fun _ => coe_le_coe
 
-@[simp]
+@[to_dual (attr := simp)]
 theorem preimage_coe_Iio : (some : α → WithTop α) ⁻¹' Iio a = Iio a :=
   ext fun _ => coe_lt_coe
 
-@[simp]
+@[to_dual (attr := simp)]
 theorem preimage_coe_Iic : (some : α → WithTop α) ⁻¹' Iic a = Iic a :=
   ext fun _ => coe_le_coe
 
-@[simp]
+@[to_dual (attr := simp)]
 theorem preimage_coe_Icc : (some : α → WithTop α) ⁻¹' Icc a b = Icc a b := by simp [← Ici_inter_Iic]
 
-@[simp]
+@[to_dual (attr := simp)]
 theorem preimage_coe_Ico : (some : α → WithTop α) ⁻¹' Ico a b = Ico a b := by simp [← Ici_inter_Iio]
 
-@[simp]
+@[to_dual (attr := simp)]
 theorem preimage_coe_Ioc : (some : α → WithTop α) ⁻¹' Ioc a b = Ioc a b := by simp [← Ioi_inter_Iic]
 
-@[simp]
+@[to_dual (attr := simp)]
 theorem preimage_coe_Ioo : (some : α → WithTop α) ⁻¹' Ioo a b = Ioo a b := by simp [← Ioi_inter_Iio]
 
-@[simp]
+@[to_dual (attr := simp)]
 theorem preimage_coe_Iio_top : (some : α → WithTop α) ⁻¹' Iio ⊤ = univ := by
   rw [← range_coe, preimage_range]
 
-@[simp]
+@[to_dual (attr := simp)]
 theorem preimage_coe_Ico_top : (some : α → WithTop α) ⁻¹' Ico a ⊤ = Ici a := by
   simp [← Ici_inter_Iio]
 
-@[simp]
+@[to_dual (attr := simp)]
 theorem preimage_coe_Ioo_top : (some : α → WithTop α) ⁻¹' Ioo a ⊤ = Ioi a := by
   simp [← Ioi_inter_Iio]
 
+@[to_dual]
 theorem image_coe_Ioi : (some : α → WithTop α) '' Ioi a = Ioo (a : WithTop α) ⊤ := by
   rw [← preimage_coe_Ioi, image_preimage_eq_inter_range, range_coe, Ioi_inter_Iio]
 
+@[to_dual]
 theorem image_coe_Ici : (some : α → WithTop α) '' Ici a = Ico (a : WithTop α) ⊤ := by
   rw [← preimage_coe_Ici, image_preimage_eq_inter_range, range_coe, Ici_inter_Iio]
 
+@[to_dual]
 theorem image_coe_Iio : (some : α → WithTop α) '' Iio a = Iio (a : WithTop α) := by
   rw [← preimage_coe_Iio, image_preimage_eq_inter_range, range_coe,
     inter_eq_self_of_subset_left (Iio_subset_Iio le_top)]
 
+@[to_dual]
 theorem image_coe_Iic : (some : α → WithTop α) '' Iic a = Iic (a : WithTop α) := by
   rw [← preimage_coe_Iic, image_preimage_eq_inter_range, range_coe,
     inter_eq_self_of_subset_left (Iic_subset_Iio.2 <| coe_lt_top a)]
 
+@[to_dual]
 theorem image_coe_Icc : (some : α → WithTop α) '' Icc a b = Icc (a : WithTop α) b := by
   rw [← preimage_coe_Icc, image_preimage_eq_inter_range, range_coe,
     inter_eq_self_of_subset_left
       (Subset.trans Icc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]
 
+@[to_dual]
 theorem image_coe_Ico : (some : α → WithTop α) '' Ico a b = Ico (a : WithTop α) b := by
   rw [← preimage_coe_Ico, image_preimage_eq_inter_range, range_coe,
     inter_eq_self_of_subset_left (Subset.trans Ico_subset_Iio_self <| Iio_subset_Iio le_top)]
 
+@[to_dual]
 theorem image_coe_Ioc : (some : α → WithTop α) '' Ioc a b = Ioc (a : WithTop α) b := by
   rw [← preimage_coe_Ioc, image_preimage_eq_inter_range, range_coe,
     inter_eq_self_of_subset_left
       (Subset.trans Ioc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]
 
+@[to_dual]
 theorem image_coe_Ioo : (some : α → WithTop α) '' Ioo a b = Ioo (a : WithTop α) b := by
   rw [← preimage_coe_Ioo, image_preimage_eq_inter_range, range_coe,
     inter_eq_self_of_subset_left (Subset.trans Ioo_subset_Iio_self <| Iio_subset_Iio le_top)]
 
+@[to_dual]
 theorem Ioi_coe : Ioi (a : WithTop α) = (↑) '' (Ioi a) ∪ {⊤} := by
   ext x; induction x <;> simp
 
+@[to_dual]
 theorem Ici_coe : Ici (a : WithTop α) = (↑) '' (Ici a) ∪ {⊤} := by
   ext x; induction x <;> simp
 
+@[to_dual]
 theorem Iio_coe : Iio (a : WithTop α) = (↑) '' (Iio a) := image_coe_Iio.symm
 
+@[to_dual]
 theorem Iic_coe : Iic (a : WithTop α) = (↑) '' (Iic a) := image_coe_Iic.symm
 
+@[to_dual]
 theorem Icc_coe : Icc (a : WithTop α) b = (↑) '' (Icc a b) := image_coe_Icc.symm
 
+@[to_dual]
 theorem Ico_coe : Ico (a : WithTop α) b = (↑) '' (Ico a b) := image_coe_Ico.symm
 
+@[to_dual]
 theorem Ioc_coe : Ioc (a : WithTop α) b = (↑) '' (Ioc a b) := image_coe_Ioc.symm
 
+@[to_dual]
 theorem Ioo_coe : Ioo (a : WithTop α) b = (↑) '' (Ioo a b) := image_coe_Ioo.symm
 
 end WithTop
-
-/-! ### `WithBot` -/
-
-namespace WithBot
-
-@[simp]
-theorem preimage_coe_bot : (some : α → WithBot α) ⁻¹' {⊥} = (∅ : Set α) :=
-  @WithTop.preimage_coe_top αᵒᵈ
-
-variable [Preorder α] {a b : α}
-
-theorem range_coe : range (some : α → WithBot α) = Ioi ⊥ := by
-  ext; simp [mem_range, WithBot.bot_lt_iff_ne_bot, ne_bot_iff_exists]
-
-@[simp]
-theorem preimage_coe_Ioi : (some : α → WithBot α) ⁻¹' Ioi a = Ioi a :=
-  ext fun _ => coe_lt_coe
-
-@[simp]
-theorem preimage_coe_Ici : (some : α → WithBot α) ⁻¹' Ici a = Ici a :=
-  ext fun _ => coe_le_coe
-
-@[simp]
-theorem preimage_coe_Iio : (some : α → WithBot α) ⁻¹' Iio a = Iio a :=
-  ext fun _ => coe_lt_coe
-
-@[simp]
-theorem preimage_coe_Iic : (some : α → WithBot α) ⁻¹' Iic a = Iic a :=
-  ext fun _ => coe_le_coe
-
-@[simp]
-theorem preimage_coe_Icc : (some : α → WithBot α) ⁻¹' Icc a b = Icc a b := by simp [← Ici_inter_Iic]
-
-@[simp]
-theorem preimage_coe_Ico : (some : α → WithBot α) ⁻¹' Ico a b = Ico a b := by simp [← Ici_inter_Iio]
-
-@[simp]
-theorem preimage_coe_Ioc : (some : α → WithBot α) ⁻¹' Ioc a b = Ioc a b := by simp [← Ioi_inter_Iic]
-
-@[simp]
-theorem preimage_coe_Ioo : (some : α → WithBot α) ⁻¹' Ioo a b = Ioo a b := by simp [← Ioi_inter_Iio]
-
-@[simp]
-theorem preimage_coe_Ioi_bot : (some : α → WithBot α) ⁻¹' Ioi ⊥ = univ := by
-  rw [← range_coe, preimage_range]
-
-@[simp]
-theorem preimage_coe_Ioc_bot : (some : α → WithBot α) ⁻¹' Ioc ⊥ a = Iic a := by
-  simp [← Ioi_inter_Iic]
-
-@[simp]
-theorem preimage_coe_Ioo_bot : (some : α → WithBot α) ⁻¹' Ioo ⊥ a = Iio a := by
-  simp [← Ioi_inter_Iio]
-
-theorem image_coe_Iio : (some : α → WithBot α) '' Iio a = Ioo (⊥ : WithBot α) a := by
-  rw [← preimage_coe_Iio, image_preimage_eq_inter_range, range_coe, inter_comm, Ioi_inter_Iio]
-
-theorem image_coe_Iic : (some : α → WithBot α) '' Iic a = Ioc (⊥ : WithBot α) a := by
-  rw [← preimage_coe_Iic, image_preimage_eq_inter_range, range_coe, inter_comm, Ioi_inter_Iic]
-
-theorem image_coe_Ioi : (some : α → WithBot α) '' Ioi a = Ioi (a : WithBot α) := by
-  rw [← preimage_coe_Ioi, image_preimage_eq_inter_range, range_coe,
-    inter_eq_self_of_subset_left (Ioi_subset_Ioi bot_le)]
-
-theorem image_coe_Ici : (some : α → WithBot α) '' Ici a = Ici (a : WithBot α) := by
-  rw [← preimage_coe_Ici, image_preimage_eq_inter_range, range_coe,
-    inter_eq_self_of_subset_left (Ici_subset_Ioi.2 <| bot_lt_coe a)]
-
-theorem image_coe_Icc : (some : α → WithBot α) '' Icc a b = Icc (a : WithBot α) b := by
-  rw [← preimage_coe_Icc, image_preimage_eq_inter_range, range_coe,
-    inter_eq_self_of_subset_left
-      (Subset.trans Icc_subset_Ici_self <| Ici_subset_Ioi.2 <| bot_lt_coe a)]
-
-theorem image_coe_Ioc : (some : α → WithBot α) '' Ioc a b = Ioc (a : WithBot α) b := by
-  rw [← preimage_coe_Ioc, image_preimage_eq_inter_range, range_coe,
-    inter_eq_self_of_subset_left (Subset.trans Ioc_subset_Ioi_self <| Ioi_subset_Ioi bot_le)]
-
-theorem image_coe_Ico : (some : α → WithBot α) '' Ico a b = Ico (a : WithBot α) b := by
-  rw [← preimage_coe_Ico, image_preimage_eq_inter_range, range_coe,
-    inter_eq_self_of_subset_left
-      (Subset.trans Ico_subset_Ici_self <| Ici_subset_Ioi.2 <| bot_lt_coe a)]
-
-theorem image_coe_Ioo : (some : α → WithBot α) '' Ioo a b = Ioo (a : WithBot α) b := by
-  rw [← preimage_coe_Ioo, image_preimage_eq_inter_range, range_coe,
-    inter_eq_self_of_subset_left (Subset.trans Ioo_subset_Ioi_self <| Ioi_subset_Ioi bot_le)]
-
-theorem Ioi_coe : Ioi (a : WithBot α) = (↑) '' (Ioi a) := image_coe_Ioi.symm
-
-theorem Ici_coe : Ici (a : WithBot α) = (↑) '' (Ici a) := image_coe_Ici.symm
-
-theorem Iio_coe : Iio (a : WithBot α) = (↑) '' (Iio a) ∪ {⊥} := by
-  ext x; induction x <;> simp
-
-theorem Iic_coe : Iic (a : WithBot α) = (↑) '' (Iic a) ∪ {⊥} := by
-  ext x; induction x <;> simp
-
-theorem Icc_coe : Icc (a : WithBot α) b = (↑) '' (Icc a b) := image_coe_Icc.symm
-
-theorem Ico_coe : Ico (a : WithBot α) b = (↑) '' (Ico a b) := image_coe_Ico.symm
-
-theorem Ioc_coe : Ioc (a : WithBot α) b = (↑) '' (Ioc a b) := image_coe_Ioc.symm
-
-theorem Ioo_coe : Ioo (a : WithBot α) b = (↑) '' (Ioo a b) := image_coe_Ioo.symm
-
-end WithBot