have h13 : (x * 2) / 2 ≤ (ii0' + y) / 2 := by linarith
case left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h10 : x ≤ ii0'
⊢ x ≤ m
case left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h10 : x ≤ ii0'
h13 : x * 2 / 2 ≤ (ii0' + y) / 2
⊢ x ≤ m