chore(data/set/intervals): relax linear_order to preorder in the proo…

…fs of `Ixx_eq_empty_iff` (#8071)

The previous formulations of `Ixx_eq_empty(_iff)` are basically a chaining of this formulation plus `not_lt` or `not_le`. But `not_lt` and `not_le` require `linear_order`. Removing them allows relaxing the typeclasses assumptions on `Ixx_eq_empty_iff` and slightly generalising `Ixx_eq_empty`.

src/analysis/calculus/tangent_cone.lean

@@ -402,12 +402,12 @@ unique_diff_on_convex (convex_Icc a b) $ by simp only [interior_Icc, nonempty_Io
 lemma unique_diff_on_Ico (a b : ℝ) : unique_diff_on ℝ (Ico a b) :=
 if hab : a < b
 then unique_diff_on_convex (convex_Ico a b) $ by simp only [interior_Ico, nonempty_Ioo, hab]
-else by simp only [Ico_eq_empty (le_of_not_lt hab), unique_diff_on_empty]
+else by simp only [Ico_eq_empty hab, unique_diff_on_empty]
 
 lemma unique_diff_on_Ioc (a b : ℝ) : unique_diff_on ℝ (Ioc a b) :=
 if hab : a < b
 then unique_diff_on_convex (convex_Ioc a b) $ by simp only [interior_Ioc, nonempty_Ioo, hab]
-else by simp only [Ioc_eq_empty (le_of_not_lt hab), unique_diff_on_empty]
+else by simp only [Ioc_eq_empty hab, unique_diff_on_empty]
 
 lemma unique_diff_on_Ioo (a b : ℝ) : unique_diff_on ℝ (Ioo a b) :=
 is_open_Ioo.unique_diff_on

src/data/set/intervals/basic.lean

@@ -156,21 +156,33 @@ nonempty.to_subtype nonempty_Ioi
 instance nonempty_Iio_subtype [no_bot_order α] : nonempty (Iio a) :=
 nonempty.to_subtype nonempty_Iio
 
-@[simp] lemma Ioo_eq_empty (h : b ≤ a) : Ioo a b = ∅ :=
-eq_empty_iff_forall_not_mem.2 $ λ x ⟨h₁, h₂⟩, (h₁.trans h₂).not_le h
+@[simp] lemma Icc_eq_empty (h : ¬a ≤ b) : Icc a b = ∅ :=
+eq_empty_iff_forall_not_mem.2 $ λ x ⟨ha, hb⟩, h (ha.trans hb)
 
-@[simp] lemma Ico_eq_empty (h : b ≤ a) : Ico a b = ∅ :=
-eq_empty_iff_forall_not_mem.2 $ λ x ⟨h₁, h₂⟩, (h₁.trans_lt h₂).not_le h
+@[simp] lemma Ico_eq_empty (h : ¬a < b) : Ico a b = ∅ :=
+eq_empty_iff_forall_not_mem.2 $ λ x ⟨ha, hb⟩, h (ha.trans_lt hb)
 
-@[simp] lemma Icc_eq_empty (h : b < a) : Icc a b = ∅ :=
-eq_empty_iff_forall_not_mem.2 $ λ x ⟨h₁, h₂⟩, (h₁.trans h₂).not_lt h
+@[simp] lemma Ioc_eq_empty (h : ¬a < b) : Ioc a b = ∅ :=
+eq_empty_iff_forall_not_mem.2 $ λ x ⟨ha, hb⟩, h (ha.trans_le hb)
 
-@[simp] lemma Ioc_eq_empty (h : b ≤ a) : Ioc a b = ∅ :=
-eq_empty_iff_forall_not_mem.2 $ λ x ⟨h₁, h₂⟩, (h₂.trans h).not_lt h₁
+@[simp] lemma Ioo_eq_empty (h : ¬a < b) : Ioo a b = ∅ :=
+eq_empty_iff_forall_not_mem.2 $ λ x ⟨ha, hb⟩,  h (ha.trans hb)
 
-@[simp] lemma Ioo_self (a : α) : Ioo a a = ∅ := Ioo_eq_empty $ le_refl _
-@[simp] lemma Ico_self (a : α) : Ico a a = ∅ := Ico_eq_empty $ le_refl _
-@[simp] lemma Ioc_self (a : α) : Ioc a a = ∅ := Ioc_eq_empty $ le_refl _
+@[simp] lemma Icc_eq_empty_of_lt (h : b < a) : Icc a b = ∅ :=
+Icc_eq_empty h.not_le
+
+@[simp] lemma Ico_eq_empty_of_le (h : b ≤ a) : Ico a b = ∅ :=
+Ico_eq_empty h.not_lt
+
+@[simp] lemma Ioc_eq_empty_of_le (h : b ≤ a) : Ioc a b = ∅ :=
+Ioc_eq_empty h.not_lt
+
+@[simp] lemma Ioo_eq_empty_of_le (h : b ≤ a) : Ioo a b = ∅ :=
+Ioo_eq_empty h.not_lt
+
+@[simp] lemma Ico_self (a : α) : Ico a a = ∅ := Ico_eq_empty $ lt_irrefl _
+@[simp] lemma Ioc_self (a : α) : Ioc a a = ∅ := Ioc_eq_empty $ lt_irrefl _
+@[simp] lemma Ioo_self (a : α) : Ioo a a = ∅ := Ioo_eq_empty $ lt_irrefl _
 
 lemma Ici_subset_Ici : Ici a ⊆ Ici b ↔ b ≤ a :=
 ⟨λ h, h $ left_mem_Ici, λ h x hx, h.trans hx⟩
@@ -347,6 +359,18 @@ lemma mem_Icc_of_Ioc (h : x ∈ Ioc a b) : x ∈ Icc a b := Ioc_subset_Icc_self
 lemma mem_Ici_of_Ioi (h : x ∈ Ioi a) : x ∈ Ici a := Ioi_subset_Ici_self h
 lemma mem_Iic_of_Iio (h : x ∈ Iio a) : x ∈ Iic a := Iio_subset_Iic_self h
 
+lemma Icc_eq_empty_iff : Icc a b = ∅ ↔ ¬a ≤ b :=
+by rw [←not_nonempty_iff_eq_empty, not_iff_not, nonempty_Icc]
+
+lemma Ico_eq_empty_iff : Ico a b = ∅ ↔ ¬a < b :=
+by rw [←not_nonempty_iff_eq_empty, not_iff_not, nonempty_Ico]
+
+lemma Ioc_eq_empty_iff : Ioc a b = ∅ ↔ ¬a < b :=
+by rw [←not_nonempty_iff_eq_empty, not_iff_not, nonempty_Ioc]
+
+lemma Ioo_eq_empty_iff [densely_ordered α] : Ioo a b = ∅ ↔ ¬a < b :=
+by rw [←not_nonempty_iff_eq_empty, not_iff_not, nonempty_Ioo]
+
 end intervals
 
 section partial_order
@@ -570,20 +594,6 @@ by rw [diff_eq, compl_Iio, inter_comm, Ici_inter_Iic]
 @[simp] lemma Iio_diff_Iio : Iio b \ Iio a = Ico a b :=
 by rw [diff_eq, compl_Iio, inter_comm, Ici_inter_Iio]
 
-lemma Ioo_eq_empty_iff [densely_ordered α] : Ioo a b = ∅ ↔ b ≤ a :=
-⟨λ eq, le_of_not_lt $ λ h,
-  let ⟨x, h₁, h₂⟩ := exists_between h in
-  eq_empty_iff_forall_not_mem.1 eq x ⟨h₁, h₂⟩,
-Ioo_eq_empty⟩
-
-lemma Ico_eq_empty_iff : Ico a b = ∅ ↔ b ≤ a :=
-⟨λ eq, le_of_not_lt $ λ h, eq_empty_iff_forall_not_mem.1 eq a ⟨le_rfl, h⟩,
- Ico_eq_empty⟩
-
-lemma Icc_eq_empty_iff : Icc a b = ∅ ↔ b < a :=
-⟨λ eq, lt_of_not_ge $ λ h, eq_empty_iff_forall_not_mem.1 eq a ⟨le_rfl, h⟩,
- Icc_eq_empty⟩
-
 lemma Ico_subset_Ico_iff (h₁ : a₁ < b₁) :
   Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂ :=
 ⟨λ h, have a₂ ≤ a₁ ∧ a₁ < b₂ := h ⟨le_rfl, h₁⟩,
@@ -635,7 +645,7 @@ begin
 end
 
 @[simp] lemma Iio_subset_Iic_iff [densely_ordered α] : Iio a ⊆ Iic b ↔ a ≤ b :=
-by rw [← diff_eq_empty, Iio_diff_Iic, Ioo_eq_empty_iff]
+by rw [←diff_eq_empty, Iio_diff_Iic, Ioo_eq_empty_iff, not_lt]
 
 /-! ### Unions of adjacent intervals -/
 
@@ -1049,7 +1059,7 @@ begin
   cases le_or_lt a b with hab hab; cases le_or_lt c d with hcd hcd;
     simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, min_eq_left_of_lt,
     min_eq_right_of_lt, max_eq_left_of_lt, max_eq_right_of_lt, hab, hcd] at h₁ h₂,
-  { exact Icc_union_Icc' (le_of_lt h₂) (le_of_lt h₁) },
+  { exact Icc_union_Icc' h₂.le h₁.le },
   all_goals { simp [*, min_eq_left_of_lt, max_eq_left_of_lt, min_eq_right_of_lt,
     max_eq_right_of_lt] },
 end

src/data/set/intervals/disjoint.lean

@@ -41,8 +41,8 @@ section linear_order
 variables [linear_order α] {a₁ a₂ b₁ b₂ : α}
 
 @[simp] lemma Ico_disjoint_Ico : disjoint (Ico a₁ a₂) (Ico b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁ :=
-by simp only [set.disjoint_iff, subset_empty_iff, Ico_inter_Ico, Ico_eq_empty_iff,
-  inf_eq_min, sup_eq_max]
+by simp_rw [set.disjoint_iff_inter_eq_empty, Ico_inter_Ico, Ico_eq_empty_iff,
+  inf_eq_min, sup_eq_max, not_lt]
 
 @[simp] lemma Ioc_disjoint_Ioc : disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁ :=
 by simpa only [dual_Ico] using @Ico_disjoint_Ico (order_dual α) _ a₂ a₁ b₂ b₁

src/data/set/intervals/surj_on.lean

@@ -25,8 +25,7 @@ begin
   classical,
   intros p hp,
   rcases h_surj p with ⟨x, rfl⟩,
-  refine ⟨x, _, rfl⟩,
-  simp only [mem_Ioo],
+  refine ⟨x, mem_Ioo.2 _, rfl⟩,
   by_contra h,
   cases not_and_distrib.mp h with ha hb,
   { exact has_lt.lt.false (lt_of_lt_of_le hp.1 (h_mono (not_lt.mp ha))) },
@@ -37,16 +36,16 @@ lemma surj_on_Ico_of_monotone_surjective
   (h_mono : monotone f) (h_surj : function.surjective f) (a b : α) :
   surj_on f (Ico a b) (Ico (f a) (f b)) :=
 begin
-  rcases lt_or_ge a b with hab|hab,
+  obtain hab | hab := lt_or_le a b,
   { intros p hp,
     rcases mem_Ioo_or_eq_left_of_mem_Ico hp with hp'|hp',
     { rw hp',
-      refine ⟨a, left_mem_Ico.mpr hab, rfl⟩ },
+      exact ⟨a, left_mem_Ico.mpr hab, rfl⟩ },
     { have := surj_on_Ioo_of_monotone_surjective h_mono h_surj a b hp',
       cases this with x hx,
       exact ⟨x, Ioo_subset_Ico_self hx.1, hx.2⟩ } },
-  { rw Ico_eq_empty (h_mono hab),
-    exact surj_on_empty f _ },
+  { rw Ico_eq_empty (h_mono hab).not_lt,
+    exact surj_on_empty f _ }
 end
 
 lemma surj_on_Ioc_of_monotone_surjective

src/measure_theory/interval_integral.lean

@@ -721,7 +721,7 @@ begin
   cases le_total a b with hab hab,
   { rw [integral_of_le hab, ← integral_indicator measurable_set_Ioc, indicator_eq_self.2 h];
     apply_instance },
-  { rw [Ioc_eq_empty hab, subset_empty_iff, function.support_eq_empty_iff] at h,
+  { rw [Ioc_eq_empty hab.not_lt, subset_empty_iff, function.support_eq_empty_iff] at h,
     simp [h] }
 end
 
@@ -907,18 +907,18 @@ lemma continuous_on_primitive {f : α → E} {a b : α} [has_no_atoms μ]
   (h_int : integrable_on f (Icc a b) μ) :
   continuous_on (λ x, ∫ t in Ioc a x, f t ∂ μ) (Icc a b) :=
 begin
-  cases le_or_lt a b with H H,
+  by_cases h : a ≤ b,
   { have : ∀ x ∈ Icc a b, ∫ (t : α) in Ioc a x, f t ∂μ = ∫ (t : α) in a..x, f t ∂μ,
     { intros x x_in,
-      simp_rw [← interval_oc_of_le H, integral_of_le x_in.1] },
+      simp_rw [← interval_oc_of_le h, integral_of_le x_in.1] },
     rw continuous_on_congr this,
     intros x₀ hx₀,
     refine continuous_within_at_primitive (measure_singleton x₀) _,
     rw interval_integrable_iff,
-    simp only [H, max_eq_right, min_eq_left],
+    simp only [h, max_eq_right, min_eq_left],
     exact h_int.mono Ioc_subset_Icc_self le_rfl },
-  { rw Icc_eq_empty H,
-    apply continuous_on_empty },
+  { rw Icc_eq_empty h,
+    exact continuous_on_empty _ },
 end
 
 lemma continuous_on_primitive' {f : α → E} {a b : α} [has_no_atoms μ]
@@ -968,7 +968,7 @@ lemma integral_eq_zero_iff_of_nonneg_ae
   ∫ x in a..b, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict (Ioc a b ∪ Ioc b a)] 0 :=
 begin
   cases le_total a b with hab hab;
-    simp only [Ioc_eq_empty hab, empty_union, union_empty] at hf ⊢,
+    simp only [Ioc_eq_empty hab.not_lt, empty_union, union_empty] at hf ⊢,
   { exact integral_eq_zero_iff_of_le_of_nonneg_ae hab hf hfi },
   { rw [integral_symm, neg_eq_zero, integral_eq_zero_iff_of_le_of_nonneg_ae hab hf hfi.symm] }
 end
@@ -977,13 +977,16 @@ lemma integral_pos_iff_support_of_nonneg_ae'
   (hf : 0 ≤ᵐ[μ.restrict (Ioc a b ∪ Ioc b a)] f) (hfi : interval_integrable f μ a b) :
   0 < ∫ x in a..b, f x ∂μ ↔ a < b ∧ 0 < μ (function.support f ∩ Ioc a b) :=
 begin
-  cases le_total a b with hab hab;
-    simp only [integral_of_le, integral_of_ge, Ioc_eq_empty, hab, union_empty, empty_union] at hf ⊢,
-  { rw [set_integral_pos_iff_support_of_nonneg_ae hf hfi.1, iff.comm, and_iff_right_iff_imp],
-    contrapose!,
-    intro h,
-    rw [Ioc_eq_empty h, inter_empty, measure_empty, nonpos_iff_eq_zero] },
-  { simp [integral_nonneg_of_ae hf] }
+  obtain hab | hab := le_total b a;
+    simp only [Ioc_eq_empty hab.not_lt, empty_union, union_empty] at hf ⊢,
+  { rw [←not_iff_not, not_and_distrib, not_lt, not_lt, integral_of_ge hab, neg_nonpos],
+    exact iff_of_true (integral_nonneg_of_ae hf) (or.intro_left _ hab) },
+  rw [integral_of_le hab, set_integral_pos_iff_support_of_nonneg_ae hf hfi.1, iff.comm,
+    and_iff_right_iff_imp],
+  contrapose!,
+  intro h,
+  rw [Ioc_eq_empty h.not_lt, inter_empty, measure_empty],
+  exact le_refl 0,
 end
 
 lemma integral_pos_iff_support_of_nonneg_ae