constructor
case h
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
ab : Set ℝ
a b : ℝ
hab : Set.Ioo a b = ab
c : ℝ
hc : c ∈ f ⁻¹' ab
h2 : IsOpen (Set.Ioc a (f c))
h3 : IsOpen (f ⁻¹' Set.Ioc a (f c))
h4 : c ∈ f ⁻¹' Set.Ioc a (f c)
t : Set ℝ
a' c' : ℝ
hac' : Set.Ioc a' c' = t
htc : c ∈ Set.Ioc a' c'
ht : t ⊆ f ⁻¹' Set.Ioc a (f c)
⊢ Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c) ∧ a' < c ∧ a < f c
case h.left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
ab : Set ℝ
a b : ℝ
hab : Set.Ioo a b = ab
c : ℝ
hc : c ∈ f ⁻¹' ab
h2 : IsOpen (Set.Ioc a (f c))
h3 : IsOpen (f ⁻¹' Set.Ioc a (f c))
h4 : c ∈ f ⁻¹' Set.Ioc a (f c)
t : Set ℝ
a' c' : ℝ
hac' : Set.Ioc a' c' = t
htc : c ∈ Set.Ioc a' c'
ht : t ⊆ f ⁻¹' Set.Ioc a (f c)
⊢ Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)

case h.right
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
ab : Set ℝ
a b : ℝ
hab : Set.Ioo a b = ab
c : ℝ
hc : c ∈ f ⁻¹' ab
h2 : IsOpen (Set.Ioc a (f c))
h3 : IsOpen (f ⁻¹' Set.Ioc a (f c))
h4 : c ∈ f ⁻¹' Set.Ioc a (f c)
t : Set ℝ
a' c' : ℝ
hac' : Set.Ioc a' c' = t
htc : c ∈ Set.Ioc a' c'
ht : t ⊆ f ⁻¹' Set.Ioc a (f c)
⊢ a' < c ∧ a < f c