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

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
⊢ Monotone f
Tactic:
intro z b hz
State after:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
⊢ f z ≤ f b

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
L2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z) → y ∈ f ⁻¹' Set.Ici (f z)
⊢ f z ≤ f b
Tactic:
have h0 : Set.Ici z ⊆ f ⁻¹' (Set.Ici (f z)) :=
  real_induction L1 L2 (@Set.left_mem_Ici _ _ (f z))
State after:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
L2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z) → y ∈ f ⁻¹' Set.Ici (f z)
h0 : Set.Ici z ⊆ f ⁻¹' Set.Ici (f z)
⊢ f z ≤ f b

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
L2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z) → y ∈ f ⁻¹' Set.Ici (f z)
h0 : Set.Ici z ⊆ f ⁻¹' Set.Ici (f z)
⊢ f z ≤ f b
Tactic:
exact h0 hz
State after:
no goals

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
⊢ ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
Tactic:
intro x hx
State after:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
⊢ ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
⊢ ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
Tactic:
have inverse_image_open := continuous_def.mp hlc _ (infinite_interval_lower_open (f z))
State after:
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))
⊢ ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)

State before:
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))
⊢ ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
Tactic:
have h2 := (@TopologicalSpace.IsTopologicalBasis.isOpen_iff ℝ tₗ (f ⁻¹' (Set.Ici (f z)))
   lower_intervals lower_basis).mp inverse_image_open x hx
State after:
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)

State before:
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)
Tactic:
obtain ⟨t , ⟨ta, tb, htb⟩, xint, tsub⟩ := h2
State after:
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)

State before:
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)
Tactic:
use tb
State after:
case h
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)
⊢ x < tb ∧ Set.Ico x tb ⊆ f ⁻¹' Set.Ici (f z)

State before:
case h
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)
⊢ x < tb ∧ Set.Ico x tb ⊆ f ⁻¹' Set.Ici (f z)
Tactic:
constructor
State after:
case h.left
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)
⊢ x < tb

case h.right
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)
⊢ Set.Ico x tb ⊆ f ⁻¹' Set.Ici (f z)

State before:
case h.left
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)
⊢ x < tb
Tactic:
rw [←htb] at xint
State after:
case h.left
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 ∈ Set.Ico ta tb
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
⊢ x < tb

State before:
case h.left
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 ∈ Set.Ico ta tb
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
⊢ x < tb
Tactic:
exact xint.2
State after:
no goals

State before:
case h.right
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)
auxsub : Set.Ico x tb ⊆ t
⊢ Set.Ico x tb ⊆ f ⁻¹' Set.Ici (f z)
Tactic:
exact auxsub.trans tsub
State after:
no goals

State before:
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)
⊢ Set.Ico x tb ⊆ t
Tactic:
intro xx hxx
State after:
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)
xx : ℝ
hxx : xx ∈ Set.Ico x tb
⊢ xx ∈ t

State before:
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)
xx : ℝ
hxx : xx ∈ Set.Ico x tb
⊢ xx ∈ t
Tactic:
rw[←htb]
State after:
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)
xx : ℝ
hxx : xx ∈ Set.Ico x tb
⊢ xx ∈ Set.Ico ta tb

State before:
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)
xx : ℝ
hxx : xx ∈ Set.Ico x tb
⊢ xx ∈ Set.Ico ta tb
Tactic:
rw[←htb] at xint
State after:
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 ∈ Set.Ico ta tb
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
xx : ℝ
hxx : xx ∈ Set.Ico x tb
⊢ xx ∈ Set.Ico ta tb

State before:
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 ∈ Set.Ico ta tb
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
xx : ℝ
hxx : xx ∈ Set.Ico x tb
⊢ xx ∈ Set.Ico ta tb
Tactic:
constructor
State after:
case left
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 ∈ Set.Ico ta tb
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
xx : ℝ
hxx : xx ∈ Set.Ico x tb
⊢ ta ≤ xx

case right
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 ∈ Set.Ico ta tb
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
xx : ℝ
hxx : xx ∈ Set.Ico x tb
⊢ xx < tb

State before:
case left
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 ∈ Set.Ico ta tb
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
xx : ℝ
hxx : xx ∈ Set.Ico x tb
⊢ ta ≤ xx
Tactic:
exact xint.1.trans hxx.1
State after:
no goals

State before:
case right
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 ∈ Set.Ico ta tb
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
xx : ℝ
hxx : xx ∈ Set.Ico x tb
⊢ xx < tb
Tactic:
exact hxx.2
State after:
no goals

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
⊢ ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z) → y ∈ f ⁻¹' Set.Ici (f z)
Tactic:
intro x
State after:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x : ℝ
⊢ ∀ (y : ℝ), x < y → Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z) → y ∈ f ⁻¹' Set.Ici (f z)

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x : ℝ
⊢ ∀ (y : ℝ), x < y → Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z) → y ∈ f ⁻¹' Set.Ici (f z)
Tactic:
by_contra! H
State after:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x : ℝ
H : ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z) ∧ y ∉ f ⁻¹' Set.Ici (f z)
⊢ False

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x : ℝ
H : ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z) ∧ y ∉ f ⁻¹' Set.Ici (f z)
⊢ False
Tactic:
obtain ⟨y, hxy, hxyz, hy⟩ := H
State after:
case intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
⊢ False

State before:
case intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
⊢ False
Tactic:
have h1 := infinite_interval_upper_open (f z)
State after:
case intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
⊢ False

State before:
case intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
⊢ False
Tactic:
have h2 := continuous_def.mp huc (Set.Iio (f z)) h1
State after:
case intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
⊢ False

State before:
case intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
⊢ False
Tactic:
have h3 : y ∈ f ⁻¹' Set.Iio (f z) := by aesop
State after:
case intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
⊢ False

State before:
case intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
⊢ False
Tactic:
have h4 := (@TopologicalSpace.IsTopologicalBasis.isOpen_iff
             ℝ tᵤ _ upper_intervals upper_basis).mp h2 y h3
State after:
case intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
h4 : ∃ t ∈ upper_intervals, y ∈ t ∧ t ⊆ f ⁻¹' Set.Iio (f z)
⊢ False

State before:
case intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
h4 : ∃ t ∈ upper_intervals, y ∈ t ∧ t ⊆ f ⁻¹' Set.Iio (f z)
⊢ False
Tactic:
obtain ⟨ii, ⟨ii0, ii1, hiiu'⟩, hyii, hiis⟩ := h4
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
⊢ False
Tactic:
let ii0' := max ii0 x
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
⊢ False
Tactic:
let m := (ii0' + y) / 2
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
⊢ False
Tactic:
have h14 : ii0' < y := by unfold_let ii0'; aesop
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6 : m ∈ Set.Ico x y
h7 : m ∈ Set.Ioc ii0' y
⊢ False
Tactic:
have h8 : f m < f z := h5 ⟨(le_max_left _ _).trans_lt h7.1, h7.2⟩
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6 : m ∈ Set.Ico x y
h7 : m ∈ Set.Ioc ii0' y
h8 : f m < f z
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6 : m ∈ Set.Ico x y
h7 : m ∈ Set.Ioc ii0' y
h8 : f m < f z
⊢ False
Tactic:
have h9 : ¬ f m  < f z := not_lt.mpr (hxyz h6)
State after:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6 : m ∈ Set.Ico x y
h7 : m ∈ Set.Ioc ii0' y
h8 : f m < f z
h9 : ¬f m < f z
⊢ False

State before:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6 : m ∈ Set.Ico x y
h7 : m ∈ Set.Ioc ii0' y
h8 : f m < f z
h9 : ¬f m < f z
⊢ False
Tactic:
exact h9 h8
State after:
no goals

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
⊢ y ∈ f ⁻¹' Set.Iio (f z)
Tactic:
aesop
State after:
no goals

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h999 : Set.Ioc ii0 y ⊆ Set.Ioc ii0 ii1
⊢ Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
Tactic:
rw [hiiu'] at h999
State after:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h999 : Set.Ioc ii0 y ⊆ ii
⊢ Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h999 : Set.Ioc ii0 y ⊆ ii
⊢ Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
Tactic:
exact h999.trans hiis
State after:
no goals

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
⊢ Set.Ioc ii0 y ⊆ Set.Ioc ii0 ii1
Tactic:
intro w hw
State after:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
w : ℝ
hw : w ∈ Set.Ioc ii0 y
⊢ w ∈ Set.Ioc ii0 ii1

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
w : ℝ
hw : w ∈ Set.Ioc ii0 y
⊢ w ∈ Set.Ioc ii0 ii1
Tactic:
constructor
State after:
case left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
w : ℝ
hw : w ∈ Set.Ioc ii0 y
⊢ ii0 < w

case right
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
w : ℝ
hw : w ∈ Set.Ioc ii0 y
⊢ w ≤ ii1

State before:
case left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
w : ℝ
hw : w ∈ Set.Ioc ii0 y
⊢ ii0 < w
Tactic:
exact hw.1
State after:
no goals

State before:
case right
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
w : ℝ
hw : w ∈ Set.Ioc ii0 y
⊢ w ≤ ii1
Tactic:
rw [←hiiu'] at hyii
State after:
case right
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ Set.Ioc ii0 ii1
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
w : ℝ
hw : w ∈ Set.Ioc ii0 y
⊢ w ≤ ii1

State before:
case right
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ Set.Ioc ii0 ii1
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
w : ℝ
hw : w ∈ Set.Ioc ii0 y
⊢ w ≤ ii1
Tactic:
exact hw.2.trans hyii.2
State after:
no goals

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
⊢ ii0' < y
Tactic:
unfold_let ii0'
State after:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
⊢ max ii0 x < y

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
⊢ max ii0 x < y
Tactic:
aesop
State after:
no goals

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
⊢ m ∈ Set.Ico x y
Tactic:
constructor
State after:
case left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
⊢ x ≤ m

case right
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
⊢ m < y

State before:
case left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
⊢ x ≤ m
Tactic:
have h10 : x ≤ ii0' := le_max_right _ _
State after:
case left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h10 : x ≤ ii0'
⊢ x ≤ m

State before:
case left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h10 : x ≤ ii0'
⊢ x ≤ m
Tactic:
have h13 : (x * 2) / 2 ≤ (ii0' + y) / 2 := by linarith
State after:
case left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h10 : x ≤ ii0'
h13 : x * 2 / 2 ≤ (ii0' + y) / 2
⊢ x ≤ m

State before:
case left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h10 : x ≤ ii0'
h13 : x * 2 / 2 ≤ (ii0' + y) / 2
⊢ x ≤ m
Tactic:
rwa [mul_div_cancel_right₀ x two_ne_zero] at h13
State after:
no goals

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h10 : x ≤ ii0'
⊢ x * 2 / 2 ≤ (ii0' + y) / 2
Tactic:
linarith
State after:
no goals

State before:
case right
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
⊢ m < y
Tactic:
exact add_div_two_lt_right.mpr h14
State after:
no goals

State before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6 : m ∈ Set.Ico x y
⊢ m ∈ Set.Ioc ii0' y
Tactic:
cases' h6 with h6l h6r
State after:
case intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6l : x ≤ m
h6r : m < y
⊢ m ∈ Set.Ioc ii0' y

State before:
case intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6l : x ≤ m
h6r : m < y
⊢ m ∈ Set.Ioc ii0' y
Tactic:
constructor
State after:
case intro.left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6l : x ≤ m
h6r : m < y
⊢ ii0' < m

case intro.right
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6l : x ≤ m
h6r : m < y
⊢ m ≤ y

State before:
case intro.left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6l : x ≤ m
h6r : m < y
⊢ ii0' < m
Tactic:
exact left_lt_add_div_two.mpr h14
State after:
no goals

State before:
case intro.right
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6l : x ≤ m
h6r : m < y
⊢ m ≤ y
Tactic:
exact le_of_lt h6r
State after:
no goals