Theorem: UpperLowerContinuous.continuous_of_upper_lower_continuous (Compfiles/UpperLowerContinuous.lean)

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
⊢ Continuous f
Tactic:
apply continuous_generateFrom_iff.mpr
State after:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
⊢ ∀ s ∈ open_intervals, IsOpen (f ⁻¹' s)

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
⊢ ∀ s ∈ open_intervals, IsOpen (f ⁻¹' s)
Tactic:
intro ab hab
State after:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
ab : Set ℝ
hab : ab ∈ open_intervals
⊢ IsOpen (f ⁻¹' ab)

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
ab : Set ℝ
hab : ab ∈ open_intervals
⊢ IsOpen (f ⁻¹' ab)
Tactic:
obtain ⟨a,b, hab⟩ := hab
State after:
case intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
ab : Set ℝ
a b : ℝ
hab : Set.Ioo a b = ab
⊢ IsOpen (f ⁻¹' ab)

State before:
case 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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
h1 : ∀ c ∈ f ⁻¹' ab, ∃ t ∈ open_intervals, c ∈ t ∧ t ⊆ f ⁻¹' ab
⊢ IsOpen (f ⁻¹' ab)
Tactic:
exact
   (@TopologicalSpace.IsTopologicalBasis.isOpen_iff ℝ tₛ (f ⁻¹' ab)
     open_intervals open_basis).mpr h1
State after:
no goals

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
ab : Set ℝ
a b : ℝ
hab : Set.Ioo a b = ab
⊢ ∀ c ∈ f ⁻¹' ab, ∃ a', Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c) ∧ a' < c ∧ a < f c
Tactic:
intro c hc
State after:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
ab : Set ℝ
a b : ℝ
hab : Set.Ioo a b = ab
c : ℝ
hc : c ∈ f ⁻¹' ab
⊢ ∃ a', Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c) ∧ a' < c ∧ a < f c

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
ab : Set ℝ
a b : ℝ
hab : Set.Ioo a b = ab
c : ℝ
hc : c ∈ f ⁻¹' ab
⊢ ∃ a', Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c) ∧ a' < c ∧ a < f c
Tactic:
have h2 : IsOpen[tᵤ] (Set.Ioc a (f c)) := by
  apply TopologicalSpace.isOpen_generateFrom_of_mem
  exact ⟨a, f c, rfl⟩
State after:
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))
⊢ ∃ a', Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c) ∧ a' < c ∧ a < f c

State before:
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))
⊢ ∃ a', Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c) ∧ a' < c ∧ a < f c
Tactic:
have h3 : IsOpen[tᵤ] (f ⁻¹' (Set.Ioc a (f c))) := continuous_def.mp huc _ h2
State after:
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))
⊢ ∃ a', Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c) ∧ a' < c ∧ a < f c

State before:
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))
⊢ ∃ a', Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c) ∧ a' < c ∧ a < f c
Tactic:
have h4 : c ∈ f ⁻¹' Set.Ioc a (f c) := by aesop
State after:
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)
⊢ ∃ a', Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c) ∧ a' < c ∧ a < f c

State before:
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)
⊢ ∃ a', Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c) ∧ a' < c ∧ a < f c
Tactic:
have h5 :=
 (@TopologicalSpace.IsTopologicalBasis.isOpen_iff _ tᵤ _
   upper_intervals upper_basis).mp h3 c h4
State after:
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)
h5 : ∃ t ∈ upper_intervals, c ∈ t ∧ t ⊆ f ⁻¹' Set.Ioc a (f c)
⊢ ∃ a', Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c) ∧ a' < c ∧ a < f c

State before:
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)
h5 : ∃ t ∈ upper_intervals, c ∈ t ∧ t ⊆ f ⁻¹' Set.Ioc a (f c)
⊢ ∃ a', Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c) ∧ a' < c ∧ a < f c
Tactic:
obtain ⟨t, ⟨a', c', hac'⟩, htc, ht⟩ := h5
State after:
case intro.intro.intro.intro.intro
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 ∈ t
ht : t ⊆ f ⁻¹' Set.Ioc a (f c)
⊢ ∃ a', Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c) ∧ a' < c ∧ a < f c

State before:
case intro.intro.intro.intro.intro
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 ∈ t
ht : t ⊆ f ⁻¹' Set.Ioc a (f c)
⊢ ∃ a', Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c) ∧ a' < c ∧ a < f c
Tactic:
use a'
State after:
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 ∈ t
ht : t ⊆ f ⁻¹' Set.Ioc a (f c)
⊢ Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c) ∧ a' < c ∧ a < f c

State before:
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 ∈ t
ht : t ⊆ f ⁻¹' Set.Ioc a (f c)
⊢ Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c) ∧ a' < c ∧ a < f c
Tactic:
rw [←hac'] at htc
State after:
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

State before:
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
Tactic:
constructor
State after:
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

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
ab : Set ℝ
a b : ℝ
hab : Set.Ioo a b = ab
c : ℝ
hc : c ∈ f ⁻¹' ab
⊢ IsOpen (Set.Ioc a (f c))
Tactic:
apply TopologicalSpace.isOpen_generateFrom_of_mem
State after:
case hs
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
ab : Set ℝ
a b : ℝ
hab : Set.Ioo a b = ab
c : ℝ
hc : c ∈ f ⁻¹' ab
⊢ Set.Ioc a (f c) ∈ upper_intervals

State before:
case hs
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
ab : Set ℝ
a b : ℝ
hab : Set.Ioo a b = ab
c : ℝ
hc : c ∈ f ⁻¹' ab
⊢ Set.Ioc a (f c) ∈ upper_intervals
Tactic:
exact ⟨a, f c, rfl⟩
State after:
no goals

State before:
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))
⊢ c ∈ f ⁻¹' Set.Ioc a (f c)
Tactic:
aesop
State after:
no goals

State before:
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)
Tactic:
intro x hx
State after:
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)
x : ℝ
hx : x ∈ Set.Ioc a' c
⊢ x ∈ f ⁻¹' Set.Ioc a (f c)

State before:
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)
x : ℝ
hx : x ∈ Set.Ioc a' c
⊢ x ∈ f ⁻¹' Set.Ioc a (f c)
Tactic:
have h7 : x ∈ Set.Ioc a' c' := ⟨hx.1, hx.2.trans htc.2⟩
State after:
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)
x : ℝ
hx : x ∈ Set.Ioc a' c
h7 : x ∈ Set.Ioc a' c'
⊢ x ∈ f ⁻¹' Set.Ioc a (f c)

State before:
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)
x : ℝ
hx : x ∈ Set.Ioc a' c
h7 : x ∈ Set.Ioc a' c'
⊢ x ∈ f ⁻¹' Set.Ioc a (f c)
Tactic:
rw [hac'] at h7
State after:
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)
x : ℝ
hx : x ∈ Set.Ioc a' c
h7 : x ∈ t
⊢ x ∈ f ⁻¹' Set.Ioc a (f c)

State before:
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)
x : ℝ
hx : x ∈ Set.Ioc a' c
h7 : x ∈ t
⊢ x ∈ f ⁻¹' Set.Ioc a (f c)
Tactic:
exact ht h7
State after:
no goals

State before:
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
Tactic:
exact ⟨ htc.1, h4.1 ⟩
State after:
no goals

State before:
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 ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
Tactic:
intro c hc
State after:
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
⊢ ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b

State before:
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
⊢ ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
Tactic:
have h2 : IsOpen[tₗ] (Set.Ico (f c) b) := by
  apply TopologicalSpace.isOpen_generateFrom_of_mem
  exact ⟨f c, b, rfl⟩
State after:
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)
⊢ ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b

State before:
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)
⊢ ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
Tactic:
have h3 : IsOpen[tₗ] (f ⁻¹' (Set.Ico (f c) b)) := continuous_def.mp hlc _ h2
State after:
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)
⊢ ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b

State before:
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)
⊢ ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
Tactic:
have h4 : c ∈ f ⁻¹' Set.Ico (f c) b := by aesop
State after:
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
⊢ ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b

State before:
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
⊢ ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
Tactic:
have h5 :=
 (@TopologicalSpace.IsTopologicalBasis.isOpen_iff _ tₗ _
   lower_intervals lower_basis).mp h3 c h4
State after:
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
h5 : ∃ t ∈ lower_intervals, c ∈ t ∧ t ⊆ f ⁻¹' Set.Ico (f c) b
⊢ ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b

State before:
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
h5 : ∃ t ∈ lower_intervals, c ∈ t ∧ t ⊆ f ⁻¹' Set.Ico (f c) b
⊢ ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
Tactic:
obtain ⟨t, ⟨c', b', hcb'⟩, htc, ht⟩ := h5
State after:
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

State before:
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
Tactic:
use b'
State after:
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

State before:
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
Tactic:
rw [←hcb'] at htc
State after:
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 ∈ Set.Ico c' b'
ht : t ⊆ f ⁻¹' Set.Ico (f c) b
⊢ Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b

State before:
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 ∈ Set.Ico c' b'
ht : t ⊆ f ⁻¹' Set.Ico (f c) b
⊢ Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
Tactic:
constructor
State after:
case h.left
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 ∈ Set.Ico c' b'
ht : t ⊆ f ⁻¹' Set.Ico (f c) b
⊢ Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b

case h.right
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 ∈ Set.Ico c' b'
ht : t ⊆ f ⁻¹' Set.Ico (f c) b
⊢ c < b' ∧ f c < b

State before:
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
⊢ IsOpen (Set.Ico (f c) b)
Tactic:
apply TopologicalSpace.isOpen_generateFrom_of_mem
State after:
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

State before:
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
Tactic:
exact ⟨f c, b, rfl⟩
State after:
no goals

State before:
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)
⊢ c ∈ f ⁻¹' Set.Ico (f c) b
Tactic:
aesop
State after:
no goals

State before:
case h.left
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 ∈ Set.Ico c' b'
ht : t ⊆ f ⁻¹' Set.Ico (f c) b
⊢ Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b
Tactic:
intro x hx
State after:
case h.left
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 ∈ Set.Ico c' b'
ht : t ⊆ f ⁻¹' Set.Ico (f c) b
x : ℝ
hx : x ∈ Set.Ico c b'
⊢ x ∈ f ⁻¹' Set.Ico (f c) b

State before:
case h.left
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 ∈ Set.Ico c' b'
ht : t ⊆ f ⁻¹' Set.Ico (f c) b
x : ℝ
hx : x ∈ Set.Ico c b'
h7 : x ∈ Set.Ico c' b'
⊢ x ∈ f ⁻¹' Set.Ico (f c) b
Tactic:
rw [hcb'] at h7
State after:
case h.left
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 ∈ Set.Ico c' b'
ht : t ⊆ f ⁻¹' Set.Ico (f c) b
x : ℝ
hx : x ∈ Set.Ico c b'
h7 : x ∈ t
⊢ x ∈ f ⁻¹' Set.Ico (f c) b

State before:
case h.left
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 ∈ Set.Ico c' b'
ht : t ⊆ f ⁻¹' Set.Ico (f c) b
x : ℝ
hx : x ∈ Set.Ico c b'
h7 : x ∈ t
⊢ x ∈ f ⁻¹' Set.Ico (f c) b
Tactic:
exact ht h7
State after:
no goals

State before:
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 ∈ Set.Ico c' b'
ht : t ⊆ f ⁻¹' Set.Ico (f c) b
x : ℝ
hx : x ∈ Set.Ico c b'
⊢ x ∈ Set.Ico c' b'
Tactic:
cases' hx with hxl hxr
State after:
case 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 ∈ Set.Ico c' b'
ht : t ⊆ f ⁻¹' Set.Ico (f c) b
x : ℝ
hxl : c ≤ x
hxr : x < b'
⊢ x ∈ Set.Ico c' b'

State before:
case 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 ∈ Set.Ico c' b'
ht : t ⊆ f ⁻¹' Set.Ico (f c) b
x : ℝ
hxl : c ≤ x
hxr : x < b'
⊢ x ∈ Set.Ico c' b'
Tactic:
constructor
State after:
case intro.left
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 ∈ Set.Ico c' b'
ht : t ⊆ f ⁻¹' Set.Ico (f c) b
x : ℝ
hxl : c ≤ x
hxr : x < b'
⊢ c' ≤ x

case intro.right
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 ∈ Set.Ico c' b'
ht : t ⊆ f ⁻¹' Set.Ico (f c) b
x : ℝ
hxl : c ≤ x
hxr : x < b'
⊢ x < b'

State before:
case intro.left
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 ∈ Set.Ico c' b'
ht : t ⊆ f ⁻¹' Set.Ico (f c) b
x : ℝ
hxl : c ≤ x
hxr : x < b'
⊢ c' ≤ x
Tactic:
exact htc.1.trans hxl
State after:
no goals

State before:
case intro.right
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 ∈ Set.Ico c' b'
ht : t ⊆ f ⁻¹' Set.Ico (f c) b
x : ℝ
hxl : c ≤ x
hxr : x < b'
⊢ x < b'
Tactic:
exact hxr
State after:
no goals

State before:
case h.right
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 ∈ Set.Ico c' b'
ht : t ⊆ f ⁻¹' Set.Ico (f c) b
⊢ c < b' ∧ f c < b
Tactic:
exact ⟨htc.2, h4.2⟩
State after:
no goals

State before:
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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
⊢ ∀ c ∈ f ⁻¹' ab, ∃ t ∈ open_intervals, c ∈ t ∧ t ⊆ f ⁻¹' ab
Tactic:
intro c hc
State after:
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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
⊢ ∃ t ∈ open_intervals, c ∈ t ∧ t ⊆ f ⁻¹' ab

State before:
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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
⊢ ∃ t ∈ open_intervals, c ∈ t ∧ t ⊆ f ⁻¹' ab
Tactic:
obtain ⟨ a', ha', ⟨ ineq1a, ineq1b⟩ ⟩ := h6oc c hc
State after:
case 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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
⊢ ∃ t ∈ open_intervals, c ∈ t ∧ t ⊆ f ⁻¹' ab

State before:
case 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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
⊢ ∃ t ∈ open_intervals, c ∈ t ∧ t ⊆ f ⁻¹' ab
Tactic:
obtain ⟨ b', hb', ⟨ ineq2a, ineq2b⟩ ⟩ := h6co c hc
State after:
case intro.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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
b' : ℝ
hb' : Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b
ineq2a : c < b'
ineq2b : f c < b
⊢ ∃ t ∈ open_intervals, c ∈ t ∧ t ⊆ f ⁻¹' ab

State before:
case intro.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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
b' : ℝ
hb' : Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b
ineq2a : c < b'
ineq2b : f c < b
⊢ ∃ t ∈ open_intervals, c ∈ t ∧ t ⊆ f ⁻¹' ab
Tactic:
use Set.Ioo a' b'
State after:
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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
b' : ℝ
hb' : Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b
ineq2a : c < b'
ineq2b : f c < b
⊢ Set.Ioo a' b' ∈ open_intervals ∧ c ∈ Set.Ioo a' b' ∧ Set.Ioo a' b' ⊆ f ⁻¹' ab

State before:
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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
b' : ℝ
hb' : Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b
ineq2a : c < b'
ineq2b : f c < b
⊢ Set.Ioo a' b' ∈ open_intervals ∧ c ∈ Set.Ioo a' b' ∧ Set.Ioo a' b' ⊆ f ⁻¹' ab
Tactic:
constructor
State after:
case h.left
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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
b' : ℝ
hb' : Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b
ineq2a : c < b'
ineq2b : f c < b
⊢ Set.Ioo a' b' ∈ open_intervals

case h.right
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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
b' : ℝ
hb' : Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b
ineq2a : c < b'
ineq2b : f c < b
⊢ c ∈ Set.Ioo a' b' ∧ Set.Ioo a' b' ⊆ f ⁻¹' ab

State before:
case h.left
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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
b' : ℝ
hb' : Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b
ineq2a : c < b'
ineq2b : f c < b
⊢ Set.Ioo a' b' ∈ open_intervals
Tactic:
exact ⟨a', b', rfl⟩
State after:
no goals

State before:
case h.right
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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
b' : ℝ
hb' : Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b
ineq2a : c < b'
ineq2b : f c < b
⊢ c ∈ Set.Ioo a' b' ∧ Set.Ioo a' b' ⊆ f ⁻¹' ab
Tactic:
constructor
State after:
case h.right.left
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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
b' : ℝ
hb' : Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b
ineq2a : c < b'
ineq2b : f c < b
⊢ c ∈ Set.Ioo a' b'

case h.right.right
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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
b' : ℝ
hb' : Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b
ineq2a : c < b'
ineq2b : f c < b
⊢ Set.Ioo a' b' ⊆ f ⁻¹' ab

State before:
case h.right.left
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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
b' : ℝ
hb' : Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b
ineq2a : c < b'
ineq2b : f c < b
⊢ c ∈ Set.Ioo a' b'
Tactic:
exact ⟨ineq1a, ineq2a⟩
State after:
no goals

State before:
case h.right.right
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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
b' : ℝ
hb' : Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b
ineq2a : c < b'
ineq2b : f c < b
⊢ Set.Ioo a' b' ⊆ f ⁻¹' ab
Tactic:
have ilem1 := Set.Ioc_union_Ico_eq_Ioo ineq1a ineq2a
State after:
case h.right.right
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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
b' : ℝ
hb' : Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b
ineq2a : c < b'
ineq2b : f c < b
ilem1 : Set.Ioc a' c ∪ Set.Ico c b' = Set.Ioo a' b'
⊢ Set.Ioo a' b' ⊆ f ⁻¹' ab

State before:
case h.right.right
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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
b' : ℝ
hb' : Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b
ineq2a : c < b'
ineq2b : f c < b
ilem1 : Set.Ioc a' c ∪ Set.Ico c b' = Set.Ioo a' b'
⊢ Set.Ioo a' b' ⊆ f ⁻¹' ab
Tactic:
have ilem2 := Set.Ioc_union_Ico_eq_Ioo ineq1b ineq2b
State after:
case h.right.right
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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
b' : ℝ
hb' : Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b
ineq2a : c < b'
ineq2b : f c < b
ilem1 : Set.Ioc a' c ∪ Set.Ico c b' = Set.Ioo a' b'
ilem2 : Set.Ioc a (f c) ∪ Set.Ico (f c) b = Set.Ioo a b
⊢ Set.Ioo a' b' ⊆ f ⁻¹' ab

State before:
case h.right.right
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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
b' : ℝ
hb' : Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b
ineq2a : c < b'
ineq2b : f c < b
ilem1 : Set.Ioc a' c ∪ Set.Ico c b' = Set.Ioo a' b'
ilem2 : Set.Ioc a (f c) ∪ Set.Ico (f c) b = Set.Ioo a b
⊢ Set.Ioo a' b' ⊆ f ⁻¹' ab
Tactic:
have subeq :
  Set.Ioc a' c ∪ Set.Ico c b' ⊆ f ⁻¹' Set.Ioc a (f c) ∪ f ⁻¹' Set.Ico (f c) b
  := Set.union_subset_union ha' hb'
State after:
case h.right.right
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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
b' : ℝ
hb' : Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b
ineq2a : c < b'
ineq2b : f c < b
ilem1 : Set.Ioc a' c ∪ Set.Ico c b' = Set.Ioo a' b'
ilem2 : Set.Ioc a (f c) ∪ Set.Ico (f c) b = Set.Ioo a b
subeq : Set.Ioc a' c ∪ Set.Ico c b' ⊆ f ⁻¹' Set.Ioc a (f c) ∪ f ⁻¹' Set.Ico (f c) b
⊢ Set.Ioo a' b' ⊆ f ⁻¹' ab

State before:
case h.right.right
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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
b' : ℝ
hb' : Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b
ineq2a : c < b'
ineq2b : f c < b
ilem1 : Set.Ioc a' c ∪ Set.Ico c b' = Set.Ioo a' b'
ilem2 : Set.Ioc a (f c) ∪ Set.Ico (f c) b = Set.Ioo a b
subeq : Set.Ioc a' c ∪ Set.Ico c b' ⊆ f ⁻¹' Set.Ioc a (f c) ∪ f ⁻¹' Set.Ico (f c) b
⊢ Set.Ioo a' b' ⊆ f ⁻¹' ab
Tactic:
rw [ilem1, ←Set.preimage_union, ilem2, hab] at subeq
State after:
case h.right.right
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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
b' : ℝ
hb' : Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b
ineq2a : c < b'
ineq2b : f c < b
ilem1 : Set.Ioc a' c ∪ Set.Ico c b' = Set.Ioo a' b'
ilem2 : Set.Ioc a (f c) ∪ Set.Ico (f c) b = Set.Ioo a b
subeq : Set.Ioo a' b' ⊆ f ⁻¹' ab
⊢ Set.Ioo a' b' ⊆ f ⁻¹' ab

State before:
case h.right.right
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
h6co : ∀ c ∈ f ⁻¹' ab, ∃ b', Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b ∧ c < b' ∧ f c < b
c : ℝ
hc : c ∈ f ⁻¹' ab
a' : ℝ
ha' : Set.Ioc a' c ⊆ f ⁻¹' Set.Ioc a (f c)
ineq1a : a' < c
ineq1b : a < f c
b' : ℝ
hb' : Set.Ico c b' ⊆ f ⁻¹' Set.Ico (f c) b
ineq2a : c < b'
ineq2b : f c < b
ilem1 : Set.Ioc a' c ∪ Set.Ico c b' = Set.Ioo a' b'
ilem2 : Set.Ioc a (f c) ∪ Set.Ico (f c) b = Set.Ioo a b
subeq : Set.Ioo a' b' ⊆ f ⁻¹' ab
⊢ Set.Ioo a' b' ⊆ f ⁻¹' ab
Tactic:
exact subeq
State after:
no goals