obtain ⟨t , ⟨ta, tb, htb⟩, xint, tsub⟩ := h2
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
h2 : ∃ t ∈ lower_intervals, x ∈ t ∧ t ⊆ f ⁻¹' Set.Ici (f z)
⊢ ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
case intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ t
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
⊢ ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)