exact ⟨f c, b, rfl⟩
case hs
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
⊢ Set.Ico (f c) b ∈ lower_intervals
no goals