feat(topology/*): replace some a < b assumptions with a ≠ b (#11650)

src/analysis/box_integral/box/basic.lean

@@ -77,6 +77,7 @@ variables (I J : box ι) {x y : ι → ℝ}
 instance : inhabited (box ι) := ⟨⟨0, 1, λ i, zero_lt_one⟩⟩
 
 lemma lower_le_upper : I.lower ≤ I.upper := λ i, (I.lower_lt_upper i).le
+lemma lower_ne_upper (i) : I.lower i ≠ I.upper i := (I.lower_lt_upper i).ne
 
 instance : has_mem (ι → ℝ) (box ι) := ⟨λ x I, ∀ i, x i ∈ Ioc (I.lower i) (I.upper i)⟩
 instance : has_coe_t (box ι) (set $ ι → ℝ) := ⟨λ I, {x | x ∈ I}⟩
@@ -110,7 +111,9 @@ lemma le_tfae :
     J.lower ≤ I.lower ∧ I.upper ≤ J.upper] :=
 begin
   tfae_have : 1 ↔ 2, from iff.rfl,
-  tfae_have : 2 → 3, from λ h, by simpa [coe_eq_pi, closure_pi_set] using closure_mono h,
+  tfae_have : 2 → 3,
+  { intro h,
+    simpa [coe_eq_pi, closure_pi_set, lower_ne_upper] using closure_mono h },
   tfae_have : 3 ↔ 4, from Icc_subset_Icc_iff I.lower_le_upper,
   tfae_have : 4 → 2, from λ h x hx i, Ioc_subset_Ioc (h.1 i) (h.2 i) (hx i),
   tfae_finish

src/analysis/calculus/extend_deriv.lean

@@ -106,14 +106,14 @@ begin
   /- This is a specialization of `has_fderiv_at_boundary_of_tendsto_fderiv`. To be in the setting of
   this theorem, we need to work on an open interval with closure contained in `s ∪ {a}`, that we
   call `t = (a, b)`. Then, we check all the assumptions of this theorem and we apply it. -/
-  obtain ⟨b, ab, sab⟩ : ∃ b ∈ Ioi a, Ioc a b ⊆ s :=
+  obtain ⟨b, ab : a < b, sab : Ioc a b ⊆ s⟩ :=
     mem_nhds_within_Ioi_iff_exists_Ioc_subset.1 hs,
   let t := Ioo a b,
   have ts : t ⊆ s := subset.trans Ioo_subset_Ioc_self sab,
   have t_diff : differentiable_on ℝ f t := f_diff.mono ts,
   have t_conv : convex ℝ t := convex_Ioo a b,
   have t_open : is_open t := is_open_Ioo,
-  have t_closure : closure t = Icc a b := closure_Ioo ab,
+  have t_closure : closure t = Icc a b := closure_Ioo ab.ne,
   have t_cont : ∀y ∈ closure t, continuous_within_at f t y,
   { rw t_closure,
     assume y hy,
@@ -150,7 +150,7 @@ begin
   have t_diff : differentiable_on ℝ f t := f_diff.mono ts,
   have t_conv : convex ℝ t := convex_Ioo b a,
   have t_open : is_open t := is_open_Ioo,
-  have t_closure : closure t = Icc b a := closure_Ioo ba,
+  have t_closure : closure t = Icc b a := closure_Ioo (ne_of_lt ba),
   have t_cont : ∀y ∈ closure t, continuous_within_at f t y,
   { rw t_closure,
     assume y hy,

src/analysis/calculus/local_extr.lean

@@ -327,7 +327,7 @@ lemma exists_has_deriv_at_eq_zero' (hab : a < b)
   ∃ c ∈ Ioo a b, f' c = 0 :=
 begin
   have : continuous_on f (Ioo a b) := λ x hx, (hff' x hx).continuous_at.continuous_within_at,
-  have hcont := continuous_on_Icc_extend_from_Ioo hab this hfa hfb,
+  have hcont := continuous_on_Icc_extend_from_Ioo hab.ne this hfa hfb,
   obtain ⟨c, hc, hcextr⟩ : ∃ c ∈ Ioo a b, is_local_extr (extend_from (Ioo a b) f) c,
   { apply exists_local_extr_Ioo _ hab hcont,
     rw eq_lim_at_right_extend_from_Ioo hab hfb,

src/analysis/normed_space/basic.lean

@@ -590,7 +590,7 @@ begin
     ((continuous_id.smul continuous_const).add continuous_const).continuous_within_at,
   convert this.mem_closure _ _,
   { rw [one_smul, sub_add_cancel] },
-  { simp [closure_Ico (@zero_lt_one ℝ _ _), zero_le_one] },
+  { simp [closure_Ico (@zero_ne_one ℝ _ _), zero_le_one] },
   { rintros c ⟨hc0, hc1⟩,
     rw [set.mem_preimage, mem_ball, dist_eq_norm, add_sub_cancel, norm_smul, real.norm_eq_abs,
       abs_of_nonneg hc0, mul_comm, ← mul_one r],

src/analysis/special_functions/trigonometric/basic.lean

@@ -288,7 +288,7 @@ sin_pos_of_pos_of_lt_pi hx.1 hx.2
 
 lemma sin_nonneg_of_mem_Icc {x : ℝ} (hx : x ∈ Icc 0 π) : 0 ≤ sin x :=
 begin
-  rw ← closure_Ioo pi_pos at hx,
+  rw ← closure_Ioo pi_ne_zero.symm at hx,
   exact closure_lt_subset_le continuous_const continuous_sin
     (closure_mono (λ y, sin_pos_of_mem_Ioo) hx)
 end

src/measure_theory/integral/interval_integral.lean

@@ -2220,7 +2220,7 @@ begin
       (hcont.mono (Icc_subset_Icc ht.1.le (le_refl _)))
       (λ x hx, hderiv x ⟨ht.1.trans_le hx.1, hx.2⟩)
       (g'int.mono_set (Icc_subset_Icc ht.1.le (le_refl _))) },
-  rw closure_Ioc a_lt_b at A,
+  rw closure_Ioc a_lt_b.ne at A,
   exact (A (left_mem_Icc.2 hab)).1,
 end
 

src/topology/algebra/ordered/basic.lean

@@ -2201,19 +2201,21 @@ lemma closure_Iio' {a : α} (h : (Iio a).nonempty) :
 closure_Iio' nonempty_Iio
 
 /-- The closure of the open interval `(a, b)` is the closed interval `[a, b]`. -/
-@[simp] lemma closure_Ioo {a b : α} (hab : a < b) :
+@[simp] lemma closure_Ioo {a b : α} (hab : a ≠ b) :
   closure (Ioo a b) = Icc a b :=
 begin
   apply subset.antisymm,
   { exact closure_minimal Ioo_subset_Icc_self is_closed_Icc },
-  { rw [← diff_subset_closure_iff, Icc_diff_Ioo_same hab.le],
-    have hab' : (Ioo a b).nonempty, from nonempty_Ioo.2 hab,
-    simp only [insert_subset, singleton_subset_iff],
-    exact ⟨(is_glb_Ioo hab).mem_closure hab', (is_lub_Ioo hab).mem_closure hab'⟩ }
+  { cases hab.lt_or_lt with hab hab,
+    { rw [← diff_subset_closure_iff, Icc_diff_Ioo_same hab.le],
+      have hab' : (Ioo a b).nonempty, from nonempty_Ioo.2 hab,
+      simp only [insert_subset, singleton_subset_iff],
+      exact ⟨(is_glb_Ioo hab).mem_closure hab', (is_lub_Ioo hab).mem_closure hab'⟩ },
+    { rw Icc_eq_empty_of_lt hab, exact empty_subset _ } }
 end
 
 /-- The closure of the interval `(a, b]` is the closed interval `[a, b]`. -/
-@[simp] lemma closure_Ioc {a b : α} (hab : a < b) :
+@[simp] lemma closure_Ioc {a b : α} (hab : a ≠ b) :
   closure (Ioc a b) = Icc a b :=
 begin
   apply subset.antisymm,
@@ -2223,7 +2225,7 @@ begin
 end
 
 /-- The closure of the interval `[a, b)` is the closed interval `[a, b]`. -/
-@[simp] lemma closure_Ico {a b : α} (hab : a < b) :
+@[simp] lemma closure_Ico {a b : α} (hab : a ≠ b) :
   closure (Ico a b) = Icc a b :=
 begin
   apply subset.antisymm,
@@ -2283,13 +2285,13 @@ frontier_Iio' nonempty_Iio
 by simp [frontier, le_of_lt h, Icc_diff_Ioo_same]
 
 @[simp] lemma frontier_Ioo {a b : α} (h : a < b) : frontier (Ioo a b) = {a, b} :=
-by simp [frontier, h, le_of_lt h, Icc_diff_Ioo_same]
+by rw [frontier, closure_Ioo h.ne, interior_Ioo, Icc_diff_Ioo_same h.le]
 
 @[simp] lemma frontier_Ico [no_min_order α] {a b : α} (h : a < b) : frontier (Ico a b) = {a, b} :=
-by simp [frontier, h, le_of_lt h, Icc_diff_Ioo_same]
+by rw [frontier, closure_Ico h.ne, interior_Ico, Icc_diff_Ioo_same h.le]
 
 @[simp] lemma frontier_Ioc [no_max_order α] {a b : α} (h : a < b) : frontier (Ioc a b) = {a, b} :=
-by simp [frontier, h, le_of_lt h, Icc_diff_Ioo_same]
+by rw [frontier, closure_Ioc h.ne, interior_Ioc, Icc_diff_Ioo_same h.le]
 
 lemma nhds_within_Ioi_ne_bot' {a b : α} (H₁ : (Ioi a).nonempty) (H₂ : a ≤ b) :
   ne_bot (𝓝[Ioi a] b) :=

src/topology/algebra/ordered/extend_from.lean

@@ -18,18 +18,16 @@ variables {α : Type u} {β : Type v}
 
 lemma continuous_on_Icc_extend_from_Ioo [topological_space α] [linear_order α] [densely_ordered α]
   [order_topology α] [topological_space β] [regular_space β] {f : α → β} {a b : α}
-  {la lb : β} (hab : a < b) (hf : continuous_on f (Ioo a b))
+  {la lb : β} (hab : a ≠ b) (hf : continuous_on f (Ioo a b))
   (ha : tendsto f (𝓝[>] a) (𝓝 la)) (hb : tendsto f (𝓝[<] b) (𝓝 lb)) :
   continuous_on (extend_from (Ioo a b) f) (Icc a b) :=
 begin
   apply continuous_on_extend_from,
-  { rw closure_Ioo hab, },
+  { rw closure_Ioo hab },
   { intros x x_in,
     rcases mem_Ioo_or_eq_endpoints_of_mem_Icc x_in with rfl | rfl | h,
-    { use la,
-      simpa [hab] },
-    { use lb,
-      simpa [hab] },
+    { exact ⟨la, ha.mono_left $ nhds_within_mono _ Ioo_subset_Ioi_self⟩ },
+    { exact ⟨lb, hb.mono_left $ nhds_within_mono _ Ioo_subset_Iio_self⟩ },
     { use [f x, hf x h] } }
 end
 
@@ -39,7 +37,7 @@ lemma eq_lim_at_left_extend_from_Ioo [topological_space α] [linear_order α] [d
   extend_from (Ioo a b) f a = la :=
 begin
   apply extend_from_eq,
-  { rw closure_Ioo hab,
+  { rw closure_Ioo hab.ne,
     simp only [le_of_lt hab, left_mem_Icc, right_mem_Icc] },
   { simpa [hab] }
 end
@@ -50,7 +48,7 @@ lemma eq_lim_at_right_extend_from_Ioo [topological_space α] [linear_order α] [
   extend_from (Ioo a b) f b = lb :=
 begin
   apply extend_from_eq,
-  { rw closure_Ioo hab,
+  { rw closure_Ioo hab.ne,
     simp only [le_of_lt hab, left_mem_Icc, right_mem_Icc] },
   { simpa [hab] }
 end
@@ -62,7 +60,7 @@ lemma continuous_on_Ico_extend_from_Ioo [topological_space α]
   continuous_on (extend_from (Ioo a b) f) (Ico a b) :=
 begin
   apply continuous_on_extend_from,
-  { rw [closure_Ioo hab], exact Ico_subset_Icc_self, },
+  { rw [closure_Ioo hab.ne], exact Ico_subset_Icc_self, },
   { intros x x_in,
     rcases mem_Ioo_or_eq_left_of_mem_Ico x_in with rfl | h,
     { use la,