1. FormalConjectures
  2. Mathoverflow
  3. «235893»
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Mathoverflow 235893

Reference: mathoverflow/235893 asked by user Willie Wong

open scoped EuclideanGeometry namespace Mathoverflow235893 variable (n : ℕ)

For topological spaces $X$ and $Y$ we say a function $f : X → Y$ is connected is it sends connected sets to connected sets.

def IsConnectedMap {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) : Prop := ∀ ⦃s : Set X⦄, IsConnected s → IsConnected (f '' s)

By a standard result, every continuous map is connected

@[category test, AMS 54] theorem Continuous.isConnectedMap {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] {f : X → Y} (hf : Continuous f) : IsConnectedMap f := fun _ h ↦ IsConnected.image h f (Continuous.continuousOn hf)

A set in $\mathbb{R}$ is connected if and only if it is order-connected and non-empty.

@[category test, AMS 54] lemma isConnected_iff_ordConnected_and_nonempty {s : Set ℝ} : IsConnected s ↔ s.OrdConnected ∧ s.Nonempty := s:Set ℝ⊢ IsConnected s ↔ s.OrdConnected ∧ s.Nonempty /- We prove this by combining the facts that connected sets in $\mathbb{R}$ are exactly the order-connected sets, and that connected sets are by definition non-empty. -/ s:Set ℝ⊢ IsConnected s → s.OrdConnected ∧ s.Nonemptys:Set ℝ⊢ s.OrdConnected ∧ s.Nonempty → IsConnected s s:Set ℝ⊢ IsConnected s → s.OrdConnected ∧ s.Nonempty s:Set ℝh1:s.Nonemptyh2:IsPreconnected s⊢ s.OrdConnected ∧ s.Nonempty All goals completed! 🐙 s:Set ℝ⊢ s.OrdConnected ∧ s.Nonempty → IsConnected s s:Set ℝh1:s.OrdConnectedh2:s.Nonempty⊢ IsConnected s All goals completed! 🐙

If $f : \mathbb{R} \to \mathbb{R}$ is a connected bijection, then its inverse is also a connected bijection.

@[category test, AMS 54] lemma isConnectedMap_symm_of_R (f : ℝ ≃ ℝ) (hf : IsConnectedMap f) : IsConnectedMap f.symm := f:ℝ ≃ ℝhf:IsConnectedMap ⇑f⊢ IsConnectedMap ⇑f.symm /- We prove this by contradiction. Suppose the inverse is not connected. Then it maps some connected set to a disconnected set. By the characterization of connected sets in $\mathbb{R}$, this means there are points $a, c$ in the image and a point $b$ between them that is not in the image. We then use the connectedness of $f$ on the intervals $[a, b]$ and $[b, c]$ to derive a contradiction, as $f(b)$ must be either less than or greater than both $f(a)$ and $f(c)$, which violates the intermediate value property. -/ intro s f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝhs:IsConnected s⊢ IsConnected (⇑f.symm '' s) f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝhs:s.OrdConnected ∧ s.Nonempty⊢ (⇑f.symm '' s).OrdConnected ∧ (⇑f.symm '' s).Nonempty f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonempty⊢ (⇑f.symm '' s).OrdConnected ∧ (⇑f.symm '' s).Nonempty have h_nonempty' : (f.symm '' s).Nonempty := f:ℝ ≃ ℝhf:IsConnectedMap ⇑f⊢ IsConnectedMap ⇑f.symm f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedy:ℝhy:y ∈ s⊢ (⇑f.symm '' s).Nonempty f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedy:ℝhy:y ∈ s⊢ f.symm y ∈ ⇑f.symm '' s All goals completed! 🐙 f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)⊢ (⇑f.symm '' s).OrdConnected f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)⊢ ∀ ⦃x : ℝ⦄, x ∈ ⇑f.symm '' s → ∀ ⦃y : ℝ⦄, y ∈ ⇑f.symm '' s → Set.Icc x y ⊆ ⇑f.symm '' s intro a f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f.symm '' s⊢ ∀ ⦃y : ℝ⦄, y ∈ ⇑f.symm '' s → Set.Icc a y ⊆ ⇑f.symm '' s f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f.symm '' sc:ℝ⊢ c ∈ ⇑f.symm '' s → Set.Icc a c ⊆ ⇑f.symm '' s f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f.symm '' sc:ℝhc:c ∈ ⇑f.symm '' s⊢ Set.Icc a c ⊆ ⇑f.symm '' s f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f.symm '' sc:ℝhc:c ∈ ⇑f.symm '' sb:ℝ⊢ b ∈ Set.Icc a c → b ∈ ⇑f.symm '' s f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f.symm '' sc:ℝhc:c ∈ ⇑f.symm '' sb:ℝhb:b ∈ Set.Icc a c⊢ b ∈ ⇑f.symm '' s f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a c⊢ b ∈ ⇑f ⁻¹' s f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' s⊢ False have h_not_mem : f b ∉ Set.uIcc (f a) (f c) := f:ℝ ≃ ℝhf:IsConnectedMap ⇑f⊢ IsConnectedMap ⇑f.symm f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh:f b ∈ Set.uIcc (f a) (f c)⊢ False cases le_total (f a) (f c) with f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh:f b ∈ Set.uIcc (f a) (f c)hle:f a ≤ f c⊢ False f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh:f b ∈ Set.Icc (f a) (f c)hle:f a ≤ f c⊢ False All goals completed! 🐙 f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh:f b ∈ Set.uIcc (f a) (f c)hle:f c ≤ f a⊢ False f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh:f b ∈ Set.Icc (f c) (f a)hle:f c ≤ f a⊢ False All goals completed! 🐙 have hI1 : IsConnected (Set.Icc a b) := f:ℝ ≃ ℝhf:IsConnectedMap ⇑f⊢ IsConnectedMap ⇑f.symm f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))⊢ (Set.Icc a b).OrdConnected ∧ (Set.Icc a b).Nonempty All goals completed! 🐙 have hI2 : IsConnected (Set.Icc b c) := f:ℝ ≃ ℝhf:IsConnectedMap ⇑f⊢ IsConnectedMap ⇑f.symm f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩⊢ (Set.Icc b c).OrdConnected ∧ (Set.Icc b c).Nonempty All goals completed! 🐙 f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:IsConnected (⇑f '' Set.Icc a b) := hf hI1⊢ False f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:IsConnected (⇑f '' Set.Icc a b) := hf hI1hfI2:IsConnected (⇑f '' Set.Icc b c) := hf hI2⊢ False f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonempty⊢ False have h_uIcc1 : Set.uIcc (f a) (f b) ⊆ f '' Set.Icc a b := f:ℝ ≃ ℝhf:IsConnectedMap ⇑f⊢ IsConnectedMap ⇑f.symm f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonempty⊢ f a ∈ ⇑f '' Set.Icc a bf:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonempty⊢ f b ∈ ⇑f '' Set.Icc a b f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonempty⊢ f a ∈ ⇑f '' Set.Icc a b All goals completed! 🐙 f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonempty⊢ f b ∈ ⇑f '' Set.Icc a b All goals completed! 🐙 have h_uIcc2 : Set.uIcc (f b) (f c) ⊆ f '' Set.Icc b c := f:ℝ ≃ ℝhf:IsConnectedMap ⇑f⊢ IsConnectedMap ⇑f.symm f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))⊢ f b ∈ ⇑f '' Set.Icc b cf:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))⊢ f c ∈ ⇑f '' Set.Icc b c f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))⊢ f b ∈ ⇑f '' Set.Icc b c All goals completed! 🐙 f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))⊢ f c ∈ ⇑f '' Set.Icc b c All goals completed! 🐙 have h_cases : f b < min (f a) (f c) ∨ max (f a) (f c) < f b := f:ℝ ≃ ℝhf:IsConnectedMap ⇑f⊢ IsConnectedMap ⇑f.symm f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b < min (f a) (f c) ∨ max (f a) (f c) < f bhI1:IsConnected (Set.Icc a b)hI2:IsConnected (Set.Icc b c)hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a bh_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c⊢ f b < min (f a) (f c) ∨ max (f a) (f c) < f b All goals completed! 🐙 f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_lt:f b < min (f a) (f c)⊢ Falsef:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_gt:max (f a) (f c) < f b⊢ False f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_lt:f b < min (f a) (f c)⊢ False f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_lt:f b < min (f a) (f c)y:ℝ := min (f a) (f c)⊢ False have hy1 : y ∈ Set.uIcc (f a) (f b) := f:ℝ ≃ ℝhf:IsConnectedMap ⇑f⊢ IsConnectedMap ⇑f.symm f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_lt:f b < min (f a) (f c)y:ℝ := min (f a) (f c)⊢ f a ≤ y ∧ y ≤ f b ∨ f b ≤ y ∧ y ≤ f a f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_lt:f b < min (f a) (f c)y:ℝ := min (f a) (f c)⊢ f b ≤ y ∧ y ≤ f a All goals completed! 🐙 have hy2 : y ∈ Set.uIcc (f b) (f c) := f:ℝ ≃ ℝhf:IsConnectedMap ⇑f⊢ IsConnectedMap ⇑f.symm f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_lt:f b < min (f a) (f c)y:ℝ := min (f a) (f c)hy1:y ∈ Set.uIcc (f a) (f b) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f a) (f b)) (Set.Icc (f b) (f a)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f b) (f a)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f a ≤ y ∧ y ≤ f b ∨ _a) (propext Set.mem_Icc))) (Or.inr ⟨LT.lt.le h_lt, min_le_left (f a) (f c)⟩))))⊢ f b ≤ y ∧ y ≤ f c ∨ f c ≤ y ∧ y ≤ f b f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_lt:f b < min (f a) (f c)y:ℝ := min (f a) (f c)hy1:y ∈ Set.uIcc (f a) (f b) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f a) (f b)) (Set.Icc (f b) (f a)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f b) (f a)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f a ≤ y ∧ y ≤ f b ∨ _a) (propext Set.mem_Icc))) (Or.inr ⟨LT.lt.le h_lt, min_le_left (f a) (f c)⟩))))⊢ f b ≤ y ∧ y ≤ f c All goals completed! 🐙 f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_lt:f b < min (f a) (f c)y:ℝ := min (f a) (f c)hy1:y ∈ Set.uIcc (f a) (f b) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f a) (f b)) (Set.Icc (f b) (f a)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f b) (f a)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f a ≤ y ∧ y ≤ f b ∨ _a) (propext Set.mem_Icc))) (Or.inr ⟨LT.lt.le h_lt, min_le_left (f a) (f c)⟩))))hy2:y ∈ Set.uIcc (f b) (f c) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f b) (f c)) (Set.Icc (f c) (f b)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f c) (f b)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f b ≤ y ∧ y ≤ f c ∨ _a) (propext Set.mem_Icc))) (Or.inl ⟨LT.lt.le h_lt, min_le_right (f a) (f c)⟩))))h_x1:∃ x1 ∈ Set.Icc a b, f x1 = y := h_uIcc1 hy1⊢ False f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_lt:f b < min (f a) (f c)y:ℝ := min (f a) (f c)hy1:y ∈ Set.uIcc (f a) (f b) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f a) (f b)) (Set.Icc (f b) (f a)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f b) (f a)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f a ≤ y ∧ y ≤ f b ∨ _a) (propext Set.mem_Icc))) (Or.inr ⟨LT.lt.le h_lt, min_le_left (f a) (f c)⟩))))hy2:y ∈ Set.uIcc (f b) (f c) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f b) (f c)) (Set.Icc (f c) (f b)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f c) (f b)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f b ≤ y ∧ y ≤ f c ∨ _a) (propext Set.mem_Icc))) (Or.inl ⟨LT.lt.le h_lt, min_le_right (f a) (f c)⟩))))h_x1:∃ x1 ∈ Set.Icc a b, f x1 = y := h_uIcc1 hy1h_x2:∃ x2 ∈ Set.Icc b c, f x2 = y := h_uIcc2 hy2⊢ False f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_lt:f b < min (f a) (f c)y:ℝ := min (f a) (f c)hy1:y ∈ Set.uIcc (f a) (f b) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f a) (f b)) (Set.Icc (f b) (f a)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f b) (f a)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f a ≤ y ∧ y ≤ f b ∨ _a) (propext Set.mem_Icc))) (Or.inr ⟨LT.lt.le h_lt, min_le_left (f a) (f c)⟩))))hy2:y ∈ Set.uIcc (f b) (f c) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f b) (f c)) (Set.Icc (f c) (f b)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f c) (f b)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f b ≤ y ∧ y ≤ f c ∨ _a) (propext Set.mem_Icc))) (Or.inl ⟨LT.lt.le h_lt, min_le_right (f a) (f c)⟩))))h_x2:∃ x2 ∈ Set.Icc b c, f x2 = y := h_uIcc2 hy2x1:ℝhx1:x1 ∈ Set.Icc a bhfx1:f x1 = y⊢ False f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_lt:f b < min (f a) (f c)y:ℝ := min (f a) (f c)hy1:y ∈ Set.uIcc (f a) (f b) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f a) (f b)) (Set.Icc (f b) (f a)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f b) (f a)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f a ≤ y ∧ y ≤ f b ∨ _a) (propext Set.mem_Icc))) (Or.inr ⟨LT.lt.le h_lt, min_le_left (f a) (f c)⟩))))hy2:y ∈ Set.uIcc (f b) (f c) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f b) (f c)) (Set.Icc (f c) (f b)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f c) (f b)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f b ≤ y ∧ y ≤ f c ∨ _a) (propext Set.mem_Icc))) (Or.inl ⟨LT.lt.le h_lt, min_le_right (f a) (f c)⟩))))x1:ℝhx1:x1 ∈ Set.Icc a bhfx1:f x1 = yx2:ℝhx2:x2 ∈ Set.Icc b chfx2:f x2 = y⊢ False f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_lt:f b < min (f a) (f c)y:ℝ := min (f a) (f c)hy1:y ∈ Set.uIcc (f a) (f b) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f a) (f b)) (Set.Icc (f b) (f a)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f b) (f a)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f a ≤ y ∧ y ≤ f b ∨ _a) (propext Set.mem_Icc))) (Or.inr ⟨LT.lt.le h_lt, min_le_left (f a) (f c)⟩))))hy2:y ∈ Set.uIcc (f b) (f c) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f b) (f c)) (Set.Icc (f c) (f b)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f c) (f b)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f b ≤ y ∧ y ≤ f c ∨ _a) (propext Set.mem_Icc))) (Or.inl ⟨LT.lt.le h_lt, min_le_right (f a) (f c)⟩))))x1:ℝhx1:x1 ∈ Set.Icc a bhfx1:f x1 = yx2:ℝhx2:x2 ∈ Set.Icc b chfx2:f x2 = yh_eq:x1 = x2 := Equiv.injective f (Eq.trans hfx1 (Eq.symm hfx2))⊢ False have h_eq_b : x1 = b := f:ℝ ≃ ℝhf:IsConnectedMap ⇑f⊢ IsConnectedMap ⇑f.symm All goals completed! 🐙 have : f b = min (f a) (f c) := f:ℝ ≃ ℝhf:IsConnectedMap ⇑f⊢ IsConnectedMap ⇑f.symm All goals completed! 🐙 All goals completed! 🐙 f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_gt:max (f a) (f c) < f b⊢ False f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_gt:max (f a) (f c) < f by:ℝ := max (f a) (f c)⊢ False have hy1 : y ∈ Set.uIcc (f a) (f b) := f:ℝ ≃ ℝhf:IsConnectedMap ⇑f⊢ IsConnectedMap ⇑f.symm f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_gt:max (f a) (f c) < f by:ℝ := max (f a) (f c)⊢ f a ≤ y ∧ y ≤ f b ∨ f b ≤ y ∧ y ≤ f a f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_gt:max (f a) (f c) < f by:ℝ := max (f a) (f c)⊢ f a ≤ y ∧ y ≤ f b All goals completed! 🐙 have hy2 : y ∈ Set.uIcc (f b) (f c) := f:ℝ ≃ ℝhf:IsConnectedMap ⇑f⊢ IsConnectedMap ⇑f.symm f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_gt:max (f a) (f c) < f by:ℝ := max (f a) (f c)hy1:y ∈ Set.uIcc (f a) (f b) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f a) (f b)) (Set.Icc (f b) (f a)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f b) (f a)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f a ≤ y ∧ y ≤ f b ∨ _a) (propext Set.mem_Icc))) (Or.inl ⟨le_max_left (f a) (f c), LT.lt.le h_gt⟩))))⊢ f b ≤ y ∧ y ≤ f c ∨ f c ≤ y ∧ y ≤ f b f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_gt:max (f a) (f c) < f by:ℝ := max (f a) (f c)hy1:y ∈ Set.uIcc (f a) (f b) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f a) (f b)) (Set.Icc (f b) (f a)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f b) (f a)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f a ≤ y ∧ y ≤ f b ∨ _a) (propext Set.mem_Icc))) (Or.inl ⟨le_max_left (f a) (f c), LT.lt.le h_gt⟩))))⊢ f c ≤ y ∧ y ≤ f b All goals completed! 🐙 f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_gt:max (f a) (f c) < f by:ℝ := max (f a) (f c)hy1:y ∈ Set.uIcc (f a) (f b) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f a) (f b)) (Set.Icc (f b) (f a)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f b) (f a)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f a ≤ y ∧ y ≤ f b ∨ _a) (propext Set.mem_Icc))) (Or.inl ⟨le_max_left (f a) (f c), LT.lt.le h_gt⟩))))hy2:y ∈ Set.uIcc (f b) (f c) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f b) (f c)) (Set.Icc (f c) (f b)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f c) (f b)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f b ≤ y ∧ y ≤ f c ∨ _a) (propext Set.mem_Icc))) (Or.inr ⟨le_max_right (f a) (f c), LT.lt.le h_gt⟩))))h_x1:∃ x1 ∈ Set.Icc a b, f x1 = y := h_uIcc1 hy1⊢ False f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_gt:max (f a) (f c) < f by:ℝ := max (f a) (f c)hy1:y ∈ Set.uIcc (f a) (f b) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f a) (f b)) (Set.Icc (f b) (f a)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f b) (f a)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f a ≤ y ∧ y ≤ f b ∨ _a) (propext Set.mem_Icc))) (Or.inl ⟨le_max_left (f a) (f c), LT.lt.le h_gt⟩))))hy2:y ∈ Set.uIcc (f b) (f c) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f b) (f c)) (Set.Icc (f c) (f b)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f c) (f b)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f b ≤ y ∧ y ≤ f c ∨ _a) (propext Set.mem_Icc))) (Or.inr ⟨le_max_right (f a) (f c), LT.lt.le h_gt⟩))))h_x1:∃ x1 ∈ Set.Icc a b, f x1 = y := h_uIcc1 hy1h_x2:∃ x2 ∈ Set.Icc b c, f x2 = y := h_uIcc2 hy2⊢ False f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_gt:max (f a) (f c) < f by:ℝ := max (f a) (f c)hy1:y ∈ Set.uIcc (f a) (f b) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f a) (f b)) (Set.Icc (f b) (f a)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f b) (f a)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f a ≤ y ∧ y ≤ f b ∨ _a) (propext Set.mem_Icc))) (Or.inl ⟨le_max_left (f a) (f c), LT.lt.le h_gt⟩))))hy2:y ∈ Set.uIcc (f b) (f c) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f b) (f c)) (Set.Icc (f c) (f b)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f c) (f b)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f b ≤ y ∧ y ≤ f c ∨ _a) (propext Set.mem_Icc))) (Or.inr ⟨le_max_right (f a) (f c), LT.lt.le h_gt⟩))))h_x2:∃ x2 ∈ Set.Icc b c, f x2 = y := h_uIcc2 hy2x1:ℝhx1:x1 ∈ Set.Icc a bhfx1:f x1 = y⊢ False f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_gt:max (f a) (f c) < f by:ℝ := max (f a) (f c)hy1:y ∈ Set.uIcc (f a) (f b) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f a) (f b)) (Set.Icc (f b) (f a)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f b) (f a)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f a ≤ y ∧ y ≤ f b ∨ _a) (propext Set.mem_Icc))) (Or.inl ⟨le_max_left (f a) (f c), LT.lt.le h_gt⟩))))hy2:y ∈ Set.uIcc (f b) (f c) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f b) (f c)) (Set.Icc (f c) (f b)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f c) (f b)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f b ≤ y ∧ y ≤ f c ∨ _a) (propext Set.mem_Icc))) (Or.inr ⟨le_max_right (f a) (f c), LT.lt.le h_gt⟩))))x1:ℝhx1:x1 ∈ Set.Icc a bhfx1:f x1 = yx2:ℝhx2:x2 ∈ Set.Icc b chfx2:f x2 = y⊢ False f:ℝ ≃ ℝhf:IsConnectedMap ⇑fs:Set ℝh_ord:s.OrdConnectedh_nonempty:s.Nonemptyh_nonempty':(⇑f.symm '' s).Nonempty := Exists.casesOn h_nonempty fun y hy => Exists.intro (f.symm y) (Set.mem_image_of_mem (⇑f.symm) hy)a:ℝha:a ∈ ⇑f ⁻¹' sc:ℝhc:c ∈ ⇑f ⁻¹' sb:ℝhb:b ∈ Set.Icc a chfb:b ∉ ⇑f ⁻¹' sh_not_mem:f b ∉ Set.uIcc (f a) (f c) := fun h => Or.casesOn (motive := fun t => le_total (f a) (f c) = t → False) (le_total (f a) (f c)) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord ha hc (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_le hle)) h))) (fun hle h_1 => hfb (Set.OrdConnected.out h_ord hc ha (Eq.mp (congrArg (fun _a => f b ∈ _a) (Set.uIcc_of_ge hle)) h))) (Eq.refl (le_total (f a) (f c)))hI1:IsConnected (Set.Icc a b) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.left⟩hI2:IsConnected (Set.Icc b c) := Eq.mpr (id (congrArg (fun _a => _a) (propext isConnected_iff_ordConnected_and_nonempty))) ⟨Set.ordConnected_Icc, Set.nonempty_Icc.mpr hb.right⟩hfI1:(⇑f '' Set.Icc a b).OrdConnected ∧ (⇑f '' Set.Icc a b).NonemptyhfI2:(⇑f '' Set.Icc b c).OrdConnected ∧ (⇑f '' Set.Icc b c).Nonemptyh_uIcc1:Set.uIcc (f a) (f b) ⊆ ⇑f '' Set.Icc a b := Set.OrdConnected.uIcc_subset hfI1.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.left)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.left))h_uIcc2:Set.uIcc (f b) (f c) ⊆ ⇑f '' Set.Icc b c := Set.OrdConnected.uIcc_subset hfI2.left (Set.mem_image_of_mem (⇑f) (Set.left_mem_Icc.mpr hb.right)) (Set.mem_image_of_mem (⇑f) (Set.right_mem_Icc.mpr hb.right))h_gt:max (f a) (f c) < f by:ℝ := max (f a) (f c)hy1:y ∈ Set.uIcc (f a) (f b) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f a) (f b)) (Set.Icc (f b) (f a)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f b) (f a)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f a ≤ y ∧ y ≤ f b ∨ _a) (propext Set.mem_Icc))) (Or.inl ⟨le_max_left (f a) (f c), LT.lt.le h_gt⟩))))hy2:y ∈ Set.uIcc (f b) (f c) := Eq.mpr (id (congrArg (fun _a => y ∈ _a) Set.uIcc_eq_union)) (Eq.mpr (id (congrArg (fun _a => _a) (propext (Set.mem_union y (Set.Icc (f b) (f c)) (Set.Icc (f c) (f b)))))) (Eq.mpr (id (congrArg (fun _a => _a ∨ y ∈ Set.Icc (f c) (f b)) (propext Set.mem_Icc))) (Eq.mpr (id (congrArg (fun _a => f b ≤ y ∧ y ≤ f c ∨ _a) (propext Set.mem_Icc))) (Or.inr ⟨le_max_right (f a) (f c), LT.lt.le h_gt⟩))))x1:ℝhx1:x1 ∈ Set.Icc a bhfx1:f x1 = yx2:ℝhx2:x2 ∈ Set.Icc b chfx2:f x2 = yh_eq:x1 = x2 := Equiv.injective f (Eq.trans hfx1 (Eq.symm hfx2))⊢ False have h_eq_b : x1 = b := f:ℝ ≃ ℝhf:IsConnectedMap ⇑f⊢ IsConnectedMap ⇑f.symm All goals completed! 🐙 have : f b = max (f a) (f c) := f:ℝ ≃ ℝhf:IsConnectedMap ⇑f⊢ IsConnectedMap ⇑f.symm All goals completed! 🐙 All goals completed! 🐙

The composition of two connected maps is a connected map.

@[category test, AMS 54] lemma isConnectedMap_comp {X Y Z : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] {f : X → Y} {g : Y → Z} (hf : IsConnectedMap f) (hg : IsConnectedMap g) : IsConnectedMap (g ∘ f) := X:Type u_1Y:Type u_2Z:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace Yinst✝:TopologicalSpace Zf:X → Yg:Y → Zhf:IsConnectedMap fhg:IsConnectedMap g⊢ IsConnectedMap (g ∘ f) /- We prove this by simply applying the definition of a connected map twice. -/ intro s X:Type u_1Y:Type u_2Z:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace Yinst✝:TopologicalSpace Zf:X → Yg:Y → Zhf:IsConnectedMap fhg:IsConnectedMap gs:Set Xhs:IsConnected s⊢ IsConnected (g ∘ f '' s) X:Type u_1Y:Type u_2Z:Type u_3inst✝²:TopologicalSpace Xinst✝¹:TopologicalSpace Yinst✝:TopologicalSpace Zf:X → Yg:Y → Zhf:IsConnectedMap fhg:IsConnectedMap gs:Set Xhs:IsConnected s⊢ IsConnected (g '' (f '' s)) All goals completed! 🐙

A homeomorphism is a connected map.

@[category test, AMS 54] lemma isConnectedMap_homeomorph {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] (h : X ≃ₜ Y) : IsConnectedMap h := X:Type u_1Y:Type u_2inst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yh:X ≃ₜ Y⊢ IsConnectedMap ⇑h /- We prove this by noting that a homeomorphism is continuous, and continuous maps preserve connectedness. -/ intro s X:Type u_1Y:Type u_2inst✝¹:TopologicalSpace Xinst✝:TopologicalSpace Yh:X ≃ₜ Ys:Set Xhs:IsConnected s⊢ IsConnected (⇑h '' s) All goals completed! 🐙

If $f : \mathbb{R}^1 \to \mathbb{R}^1$ is a connected bijection, then its inverse is also a connected bijection.

@[category test, AMS 54] lemma isConnectedMap_symm_of_E1 (f : ℝ^1 ≃ ℝ^1) (hf : IsConnectedMap f) : IsConnectedMap f.symm := f:ℝ^1 ≃ ℝ^1hf:IsConnectedMap ⇑f⊢ IsConnectedMap ⇑f.symm /- We prove this by conjugating $f$ with the standard homeomorphism between $\mathbb{R}^1$ and $\mathbb{R}$, and then applying the corresponding result for $\mathbb{R}$. -/ f:ℝ^1 ≃ ℝ^1hf:IsConnectedMap ⇑fh:ℝ^1 ≃ₜ ℝ := (EuclideanSpace.equiv (Fin 1) ℝ).toHomeomorph.trans (Homeomorph.funUnique (Fin 1) ℝ)⊢ IsConnectedMap ⇑f.symm f:ℝ^1 ≃ ℝ^1hf:IsConnectedMap ⇑fh:ℝ^1 ≃ₜ ℝ := (EuclideanSpace.equiv (Fin 1) ℝ).toHomeomorph.trans (Homeomorph.funUnique (Fin 1) ℝ)g:ℝ ≃ ℝ := h.symm.trans (f.trans h.toEquiv)⊢ IsConnectedMap ⇑f.symm have hg_conn : IsConnectedMap g := f:ℝ^1 ≃ ℝ^1hf:IsConnectedMap ⇑f⊢ IsConnectedMap ⇑f.symm f:ℝ^1 ≃ ℝ^1hf:IsConnectedMap ⇑fh:ℝ^1 ≃ₜ ℝ := (EuclideanSpace.equiv (Fin 1) ℝ).toHomeomorph.trans (Homeomorph.funUnique (Fin 1) ℝ)g:ℝ ≃ ℝ := h.symm.trans (f.trans h.toEquiv)h1:IsConnectedMap ⇑h.symm := isConnectedMap_homeomorph h.symm⊢ IsConnectedMap ⇑g f:ℝ^1 ≃ ℝ^1hf:IsConnectedMap ⇑fh:ℝ^1 ≃ₜ ℝ := (EuclideanSpace.equiv (Fin 1) ℝ).toHomeomorph.trans (Homeomorph.funUnique (Fin 1) ℝ)g:ℝ ≃ ℝ := h.symm.trans (f.trans h.toEquiv)h1:IsConnectedMap ⇑h.symm := isConnectedMap_homeomorph h.symmh2:IsConnectedMap ⇑h := isConnectedMap_homeomorph h⊢ IsConnectedMap ⇑g f:ℝ^1 ≃ ℝ^1hf:IsConnectedMap ⇑fh:ℝ^1 ≃ₜ ℝ := (EuclideanSpace.equiv (Fin 1) ℝ).toHomeomorph.trans (Homeomorph.funUnique (Fin 1) ℝ)g:ℝ ≃ ℝ := h.symm.trans (f.trans h.toEquiv)h1:IsConnectedMap ⇑h.symm := isConnectedMap_homeomorph h.symmh2:IsConnectedMap ⇑h := isConnectedMap_homeomorph h⊢ IsConnectedMap (⇑h ∘ ⇑f ∘ ⇑h.symm) All goals completed! 🐙 f:ℝ^1 ≃ ℝ^1hf:IsConnectedMap ⇑fh:ℝ^1 ≃ₜ ℝ := (EuclideanSpace.equiv (Fin 1) ℝ).toHomeomorph.trans (Homeomorph.funUnique (Fin 1) ℝ)g:ℝ ≃ ℝ := h.symm.trans (f.trans h.toEquiv)hg_conn:IsConnectedMap ⇑g := have h1 := isConnectedMap_homeomorph h.symm; have h2 := isConnectedMap_homeomorph h; id (isConnectedMap_comp (isConnectedMap_comp h1 hf) h2)hg_symm_conn:IsConnectedMap ⇑g.symm := isConnectedMap_symm_of_R g hg_conn⊢ IsConnectedMap ⇑f.symm have hf_eq : (f.symm : ℝ^1 → ℝ^1) = h.symm ∘ g.symm ∘ h := f:ℝ^1 ≃ ℝ^1hf:IsConnectedMap ⇑f⊢ IsConnectedMap ⇑f.symm f:ℝ^1 ≃ ℝ^1hf:IsConnectedMap ⇑fh:ℝ^1 ≃ₜ ℝ := (EuclideanSpace.equiv (Fin 1) ℝ).toHomeomorph.trans (Homeomorph.funUnique (Fin 1) ℝ)g:ℝ ≃ ℝ := h.symm.trans (f.trans h.toEquiv)hg_conn:IsConnectedMap ⇑g := have h1 := isConnectedMap_homeomorph h.symm; have h2 := isConnectedMap_homeomorph h; id (isConnectedMap_comp (isConnectedMap_comp h1 hf) h2)hg_symm_conn:IsConnectedMap ⇑g.symm := isConnectedMap_symm_of_R g hg_connx:ℝ^1i✝:Fin 1⊢ (f.symm x).ofLp i✝ = ((⇑h.symm ∘ ⇑g.symm ∘ ⇑h) x).ofLp i✝ All goals completed! 🐙 f:ℝ^1 ≃ ℝ^1hf:IsConnectedMap ⇑fh:ℝ^1 ≃ₜ ℝ := (EuclideanSpace.equiv (Fin 1) ℝ).toHomeomorph.trans (Homeomorph.funUnique (Fin 1) ℝ)g:ℝ ≃ ℝ := h.symm.trans (f.trans h.toEquiv)hg_conn:IsConnectedMap ⇑g := have h1 := isConnectedMap_homeomorph h.symm; have h2 := isConnectedMap_homeomorph h; id (isConnectedMap_comp (isConnectedMap_comp h1 hf) h2)hg_symm_conn:IsConnectedMap ⇑g.symm := isConnectedMap_symm_of_R g hg_connhf_eq:⇑f.symm = ⇑h.symm ∘ ⇑g.symm ∘ ⇑h := funext fun x => PiLp.ext fun i => of_eq_true (Eq.trans (congrArg (fun x_1 => (f.symm x).ofLp i = x_1.ofLp i) (Eq.trans (congrArg (fun x => h.symm (h.symm.symm (f.symm x))) (Homeomorph.symm_apply_apply h x)) (Homeomorph.symm_apply_apply h (f.symm x)))) (eq_self ((f.symm x).ofLp i)))⊢ IsConnectedMap (⇑h.symm ∘ ⇑g.symm ∘ ⇑h) f:ℝ^1 ≃ ℝ^1hf:IsConnectedMap ⇑fh:ℝ^1 ≃ₜ ℝ := (EuclideanSpace.equiv (Fin 1) ℝ).toHomeomorph.trans (Homeomorph.funUnique (Fin 1) ℝ)g:ℝ ≃ ℝ := h.symm.trans (f.trans h.toEquiv)hg_conn:IsConnectedMap ⇑g := have h1 := isConnectedMap_homeomorph h.symm; have h2 := isConnectedMap_homeomorph h; id (isConnectedMap_comp (isConnectedMap_comp h1 hf) h2)hg_symm_conn:IsConnectedMap ⇑g.symm := isConnectedMap_symm_of_R g hg_connhf_eq:⇑f.symm = ⇑h.symm ∘ ⇑g.symm ∘ ⇑h := funext fun x => PiLp.ext fun i => of_eq_true (Eq.trans (congrArg (fun x_1 => (f.symm x).ofLp i = x_1.ofLp i) (Eq.trans (congrArg (fun x => h.symm (h.symm.symm (f.symm x))) (Homeomorph.symm_apply_apply h x)) (Homeomorph.symm_apply_apply h (f.symm x)))) (eq_self ((f.symm x).ofLp i)))h1:IsConnectedMap ⇑h := isConnectedMap_homeomorph h⊢ IsConnectedMap (⇑h.symm ∘ ⇑g.symm ∘ ⇑h) f:ℝ^1 ≃ ℝ^1hf:IsConnectedMap ⇑fh:ℝ^1 ≃ₜ ℝ := (EuclideanSpace.equiv (Fin 1) ℝ).toHomeomorph.trans (Homeomorph.funUnique (Fin 1) ℝ)g:ℝ ≃ ℝ := h.symm.trans (f.trans h.toEquiv)hg_conn:IsConnectedMap ⇑g := have h1 := isConnectedMap_homeomorph h.symm; have h2 := isConnectedMap_homeomorph h; id (isConnectedMap_comp (isConnectedMap_comp h1 hf) h2)hg_symm_conn:IsConnectedMap ⇑g.symm := isConnectedMap_symm_of_R g hg_connhf_eq:⇑f.symm = ⇑h.symm ∘ ⇑g.symm ∘ ⇑h := funext fun x => PiLp.ext fun i => of_eq_true (Eq.trans (congrArg (fun x_1 => (f.symm x).ofLp i = x_1.ofLp i) (Eq.trans (congrArg (fun x => h.symm (h.symm.symm (f.symm x))) (Homeomorph.symm_apply_apply h x)) (Homeomorph.symm_apply_apply h (f.symm x)))) (eq_self ((f.symm x).ofLp i)))h1:IsConnectedMap ⇑h := isConnectedMap_homeomorph hh2:IsConnectedMap ⇑h.symm := isConnectedMap_homeomorph h.symm⊢ IsConnectedMap (⇑h.symm ∘ ⇑g.symm ∘ ⇑h) f:ℝ^1 ≃ ℝ^1hf:IsConnectedMap ⇑fh:ℝ^1 ≃ₜ ℝ := (EuclideanSpace.equiv (Fin 1) ℝ).toHomeomorph.trans (Homeomorph.funUnique (Fin 1) ℝ)g:ℝ ≃ ℝ := h.symm.trans (f.trans h.toEquiv)hg_conn:IsConnectedMap ⇑g := have h1 := isConnectedMap_homeomorph h.symm; have h2 := isConnectedMap_homeomorph h; id (isConnectedMap_comp (isConnectedMap_comp h1 hf) h2)hg_symm_conn:IsConnectedMap ⇑g.symm := isConnectedMap_symm_of_R g hg_connhf_eq:⇑f.symm = ⇑h.symm ∘ ⇑g.symm ∘ ⇑h := funext fun x => PiLp.ext fun i => of_eq_true (Eq.trans (congrArg (fun x_1 => (f.symm x).ofLp i = x_1.ofLp i) (Eq.trans (congrArg (fun x => h.symm (h.symm.symm (f.symm x))) (Homeomorph.symm_apply_apply h x)) (Homeomorph.symm_apply_apply h (f.symm x)))) (eq_self ((f.symm x).ofLp i)))h1:IsConnectedMap ⇑h := isConnectedMap_homeomorph hh2:IsConnectedMap ⇑h.symm := isConnectedMap_homeomorph h.symm⊢ IsConnectedMap (⇑h.symm ∘ ⇑g.symm ∘ ⇑h) All goals completed! 🐙

Assume for $n>1$, $f:\mathbb{R}^n\to\mathbb{R}^n$ is a bijection, where $\mathbb{R}^n$ is equipped with the standard topology. Does the connectedness of (the induced power set map) $f$ imply that of $f^{-1}$?

@[category research open, AMS 26 54] theorem declaration uses 'sorry'mathoverflow_235893 : answer(sorry) ↔ ∀ n > 1, ∀ (f : ℝ^n ≃ ℝ^n), IsConnectedMap f → IsConnectedMap f.symm := ⊢ True ↔ ∀ n > 1, ∀ (f : ℝ^n ≃ ℝ^n), IsConnectedMap ⇑f → IsConnectedMap ⇑f.symm All goals completed! 🐙

There exists a connected bijection ℝ → ℝ^2 where the inverse is not connected, proven in mathoverflow/260589 by user Gro-Tsen.

@[category research solved, AMS 26 54] theorem declaration uses 'sorry'mathoverflow_260589 : ∃ f : ℝ ≃ ℝ^2, IsConnectedMap f ∧ ¬ IsConnectedMap f.symm := ⊢ ∃ f, IsConnectedMap ⇑f ∧ ¬IsConnectedMap ⇑f.symm All goals completed! 🐙 -- TODO: Add remarks from the mathoverflow post end Mathoverflow235893