feat(Topology/Order): Remove hypothesis in extendFrom lemmas (leanprover-community#36627)

Remove a hypothesis in some extendFrom lemmas by using cases.

Co-authored-by: NoahW314 <noahwalker3.14@gmail.com>

Author: NoahW314

Mathlib/Topology/Order/ExtendFrom.lean

@@ -24,8 +24,10 @@ section RegularSpace
 variable [RegularSpace β]
 
 theorem continuousOn_Icc_extendFrom_Ioo
-    (hab : a ≠ b) (hf : ContinuousOn f (Ioo a b)) (ha : Tendsto f (𝓝[>] a) (𝓝 la))
+    (hf : ContinuousOn f (Ioo a b)) (ha : Tendsto f (𝓝[>] a) (𝓝 la))
     (hb : Tendsto f (𝓝[<] b) (𝓝 lb)) : ContinuousOn (extendFrom (Ioo a b) f) (Icc a b) := by
+  by_cases! hab : a = b
+  · simp [hab]
   apply continuousOn_extendFrom
   · rw [closure_Ioo hab]
   · intro x x_in
@@ -35,20 +37,24 @@ theorem continuousOn_Icc_extendFrom_Ioo
     · exact ⟨f x, hf x h⟩
 
 theorem continuousOn_uIcc_extendFrom_uIoo
-    (hab : a ≠ b) (hf : ContinuousOn f (uIoo a b))
+    (hf : ContinuousOn f (uIoo a b))
     (ha : Tendsto f (𝓝[uIoo a b] a) (𝓝 la)) (hb : Tendsto f (𝓝[uIoo a b] b) (𝓝 lb)) :
     ContinuousOn (extendFrom (uIoo a b) f) (uIcc a b) := by
+  by_cases! hab : a = b
+  · simp [hab]
   obtain hab' | hba' := hab.lt_or_gt
   · simp only [hab', uIoo_of_lt, nhdsWithin_Ioo_eq_nhdsGT, nhdsWithin_Ioo_eq_nhdsLT,
       uIcc_of_lt] at ha hb hf ⊢
-    exact continuousOn_Icc_extendFrom_Ioo hab hf ha hb
+    exact continuousOn_Icc_extendFrom_Ioo hf ha hb
   · simp only [hba', uIoo_of_gt, nhdsWithin_Ioo_eq_nhdsGT, nhdsWithin_Ioo_eq_nhdsLT,
       uIcc_of_gt] at ha hb hf ⊢
-    exact continuousOn_Icc_extendFrom_Ioo hab.symm hf hb ha
+    exact continuousOn_Icc_extendFrom_Ioo hf hb ha
 
 theorem continuousOn_Ico_extendFrom_Ioo
-    (hab : a < b) (hf : ContinuousOn f (Ioo a b)) (ha : Tendsto f (𝓝[>] a) (𝓝 la)) :
+    (hf : ContinuousOn f (Ioo a b)) (ha : Tendsto f (𝓝[>] a) (𝓝 la)) :
     ContinuousOn (extendFrom (Ioo a b) f) (Ico a b) := by
+  by_cases! hab : a ≥ b
+  · simp [hab]
   apply continuousOn_extendFrom
   · rw [closure_Ioo hab.ne]
     exact Ico_subset_Icc_self
@@ -59,9 +65,10 @@ theorem continuousOn_Ico_extendFrom_Ioo
     · exact ⟨f x, hf x h⟩
 
 theorem continuousOn_Ioc_extendFrom_Ioo
-    (hab : a < b) (hf : ContinuousOn f (Ioo a b)) (hb : Tendsto f (𝓝[<] b) (𝓝 lb)) :
+    (hf : ContinuousOn f (Ioo a b)) (hb : Tendsto f (𝓝[<] b) (𝓝 lb)) :
     ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b) := by
-  have := continuousOn_Ico_extendFrom_Ioo (f := f ∘ OrderDual.ofDual) (la := lb) hab.dual
+  have := continuousOn_Ico_extendFrom_Ioo (f := f ∘ OrderDual.ofDual) (a := OrderDual.toDual b)
+    (b := OrderDual.toDual a) (la := lb)
   rw [Ico_toDual, Ioi_toDual, Ioo_toDual] at this
   exact this hf hb
 

Mathlib/Topology/Order/Rolle.lean

@@ -70,7 +70,7 @@ lemma exists_isExtrOn_Ioo_of_tendsto (hab : a < b) (hfc : ContinuousOn f (Ioo a
     ∃ c ∈ Ioo a b, IsExtrOn f (Ioo a b) c := by
   have h : EqOn (extendFrom (Ioo a b) f) f (Ioo a b) := extendFrom_extends hfc
   obtain ⟨c, hc, hfc⟩ : ∃ c ∈ Ioo a b, IsExtrOn (extendFrom (Ioo a b) f) (Icc a b) c :=
-    exists_Ioo_extr_on_Icc hab (continuousOn_Icc_extendFrom_Ioo hab.ne hfc ha hb)
+    exists_Ioo_extr_on_Icc hab (continuousOn_Icc_extendFrom_Ioo hfc ha hb)
       ((eq_lim_at_left_extendFrom_Ioo hab ha).trans (eq_lim_at_right_extendFrom_Ioo hab hb).symm)
   exact ⟨c, hc, (hfc.on_subset Ioo_subset_Icc_self).congr h (h hc)⟩
 
@@ -104,7 +104,7 @@ lemma exists_isExtrOn_uIoo_of_tendsto (hab : a ≠ b) (hfc : ContinuousOn f (uIo
     ∃ c ∈ uIoo a b, IsExtrOn f (uIoo a b) c := by
   have h : EqOn (extendFrom (uIoo a b) f) f (uIoo a b) := extendFrom_extends hfc
   obtain ⟨c, hc, hfc⟩ : ∃ c ∈ uIoo a b, IsExtrOn (extendFrom (uIoo a b) f) (uIcc a b) c :=
-    exists_uIoo_isExtrOn_uIcc hab (continuousOn_uIcc_extendFrom_uIoo hab hfc ha hb)
+    exists_uIoo_isExtrOn_uIcc hab (continuousOn_uIcc_extendFrom_uIoo hfc ha hb)
       ((eq_lim_at_left_extendFrom_uIoo hab ha).trans (eq_lim_at_right_extendFrom_uIoo hab hb).symm)
   exact ⟨c, hc, (hfc.on_subset uIoo_subset_uIcc_self).congr h (h hc)⟩