use b'
case intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
ab : Set ℝ
a b : ℝ
hab : Set.Ioo a b = ab
h6oc : ∀ c ∈ f ⁻¹' ab, ∃ a', Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c) ∧ a' < c ∧ a < f c
c : ℝ
hc : c ∈ f ⁻¹' ab
h2 : IsOpen (Set.Ico (f c) b)
h3 : IsOpen (f ⁻¹' Set.Ico (f c) b)
h4 : c ∈ f ⁻¹' Set.Ico (f c) b
t : Set ℝ
c' b' : ℝ
hcb' : Set.Ico c' b' = t
htc : c ∈ t
ht : t ⊆ f ⁻¹' Set.Ico (f c) b
⊢ ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
case h
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
ab : Set ℝ
a b : ℝ
hab : Set.Ioo a b = ab
h6oc : ∀ c ∈ f ⁻¹' ab, ∃ a', Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c) ∧ a' < c ∧ a < f c
c : ℝ
hc : c ∈ f ⁻¹' ab
h2 : IsOpen (Set.Ico (f c) b)
h3 : IsOpen (f ⁻¹' Set.Ico (f c) b)
h4 : c ∈ f ⁻¹' Set.Ico (f c) b
t : Set ℝ
c' b' : ℝ
hcb' : Set.Ico c' b' = t
htc : c ∈ t
ht : t ⊆ f ⁻¹' Set.Ico (f c) b
⊢ Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b