Theorem: Romania1998P12.extend_function_mono (Compfiles/Romania1998P12.lean)

State before:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
⊢ ∀ (x : ℝ), u x = f x
Tactic:
by_contra! hn
State after:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
hn : ∃ x, u x ≠ f x
⊢ False

State before:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
hn : ∃ x, u x ≠ f x
⊢ False
Tactic:
obtain ⟨y, hy⟩ := hn
State after:
case intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
⊢ False

State before:
case intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
⊢ False
Tactic:
let ε : ℝ := |u y - f y|
State after:
case intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
⊢ False

State before:
case intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
⊢ False
Tactic:
have hε : 0 < ε := abs_sub_pos.mpr hy
State after:
case intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
⊢ False

State before:
case intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
⊢ False
Tactic:
obtain ⟨δ, hδ0, hδ⟩ := Metric.continuous_iff.mp f_cont y ε hε
State after:
case intro.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
⊢ False

State before:
case intro.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
⊢ False
Tactic:
obtain h1 | h2 | h3 := lt_trichotomy (u y) (f y)
State after:
case intro.intro.intro.inl
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
⊢ False

case intro.intro.intro.inr.inl
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h2 : u y = f y
⊢ False

case intro.intro.intro.inr.inr
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
⊢ False

State before:
case intro.intro.intro.inl
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
⊢ False
Tactic:
have : ∃ z : ℚ, (z:ℝ) < y ∧ dist (z:ℝ) y < δ := by
  have hyδ : y - δ < y := sub_lt_self y hδ0
  obtain ⟨z, hz1, hz2⟩ := exists_rat_btwn hyδ
  refine ⟨z, hz2, ?_⟩
  . rw [Real.dist_eq, abs_sub_comm, abs_of_pos (sub_pos.mpr hz2)]
    exact sub_lt_comm.mp hz1
State after:
case intro.intro.intro.inl
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
this : ∃ z, ↑z < y ∧ dist (↑z) y < δ
⊢ False

State before:
case intro.intro.intro.inl
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
this : ∃ z, ↑z < y ∧ dist (↑z) y < δ
⊢ False
Tactic:
obtain ⟨z, h_z_lt_y, hyz⟩ := this
State after:
case intro.intro.intro.inl.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
⊢ False

State before:
case intro.intro.intro.inl.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
⊢ False
Tactic:
have hbzb := hδ z hyz
State after:
case intro.intro.intro.inl.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (f ↑z) (f y) < ε
⊢ False

State before:
case intro.intro.intro.inl.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (f ↑z) (f y) < ε
⊢ False
Tactic:
rw [←h z] at hbzb
State after:
case intro.intro.intro.inl.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
⊢ False

State before:
case intro.intro.intro.inl.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
huzuy : u y < u ↑z
⊢ False
Tactic:
have h_y_le_z := le_of_lt  h_z_lt_y
State after:
case intro.intro.intro.inl.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
huzuy : u y < u ↑z
h_y_le_z : ↑z ≤ y
⊢ False

State before:
case intro.intro.intro.inl.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
huzuy : u y < u ↑z
h_y_le_z : ↑z ≤ y
⊢ False
Tactic:
have := u_mono h_y_le_z
State after:
case intro.intro.intro.inl.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
huzuy : u y < u ↑z
h_y_le_z : ↑z ≤ y
this : u ↑z ≤ u y
⊢ False

State before:
case intro.intro.intro.inl.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
huzuy : u y < u ↑z
h_y_le_z : ↑z ≤ y
this : u ↑z ≤ u y
⊢ False
Tactic:
linarith
State after:
no goals

State before:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
⊢ ∃ z, ↑z < y ∧ dist (↑z) y < δ
Tactic:
have hyδ : y - δ < y := sub_lt_self y hδ0
State after:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
hyδ : y - δ < y
⊢ ∃ z, ↑z < y ∧ dist (↑z) y < δ

State before:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
hyδ : y - δ < y
⊢ ∃ z, ↑z < y ∧ dist (↑z) y < δ
Tactic:
obtain ⟨z, hz1, hz2⟩ := exists_rat_btwn hyδ
State after:
case intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
hyδ : y - δ < y
z : ℚ
hz1 : y - δ < ↑z
hz2 : ↑z < y
⊢ ∃ z, ↑z < y ∧ dist (↑z) y < δ

State before:
case intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
hyδ : y - δ < y
z : ℚ
hz1 : y - δ < ↑z
hz2 : ↑z < y
⊢ ∃ z, ↑z < y ∧ dist (↑z) y < δ
Tactic:
refine ⟨z, hz2, ?_⟩
State after:
case intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
hyδ : y - δ < y
z : ℚ
hz1 : y - δ < ↑z
hz2 : ↑z < y
⊢ dist (↑z) y < δ

State before:
case intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
hyδ : y - δ < y
z : ℚ
hz1 : y - δ < ↑z
hz2 : ↑z < y
⊢ dist (↑z) y < δ
Tactic:
. rw [Real.dist_eq, abs_sub_comm, abs_of_pos (sub_pos.mpr hz2)]
  exact sub_lt_comm.mp hz1
State after:
no goals

State before:
case intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
hyδ : y - δ < y
z : ℚ
hz1 : y - δ < ↑z
hz2 : ↑z < y
⊢ dist (↑z) y < δ
Tactic:
rw [Real.dist_eq, abs_sub_comm, abs_of_pos (sub_pos.mpr hz2)]
State after:
case intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
hyδ : y - δ < y
z : ℚ
hz1 : y - δ < ↑z
hz2 : ↑z < y
⊢ y - ↑z < δ

State before:
case intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
hyδ : y - δ < y
z : ℚ
hz1 : y - δ < ↑z
hz2 : ↑z < y
⊢ y - ↑z < δ
Tactic:
exact sub_lt_comm.mp hz1
State after:
no goals

State before:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
⊢ u y < u ↑z
Tactic:
have hufp : u y - f y < 0 := by linarith
State after:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
hufp : u y - f y < 0
⊢ u y < u ↑z

State before:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
hufp : u y - f y < 0
⊢ u y < u ↑z
Tactic:
have hua : ε = -(u y - f y) := abs_of_neg hufp
State after:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
hufp : u y - f y < 0
hua : ε = -(u y - f y)
⊢ u y < u ↑z

State before:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
hufp : u y - f y < 0
hua : ε = -(u y - f y)
⊢ u y < u ↑z
Tactic:
rw [hua, Real.dist_eq] at hbzb
State after:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < -(u y - f y)
hufp : u y - f y < 0
hua : ε = -(u y - f y)
⊢ u y < u ↑z

State before:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < -(u y - f y)
hufp : u y - f y < 0
hua : ε = -(u y - f y)
⊢ u y < u ↑z
Tactic:
obtain h5 | h6 := em (f y < u z)
State after:
case inl
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < -(u y - f y)
hufp : u y - f y < 0
hua : ε = -(u y - f y)
h5 : f y < u ↑z
⊢ u y < u ↑z

case inr
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < -(u y - f y)
hufp : u y - f y < 0
hua : ε = -(u y - f y)
h6 : ¬f y < u ↑z
⊢ u y < u ↑z

State before:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
⊢ u y - f y < 0
Tactic:
linarith
State after:
no goals

State before:
case inl
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < -(u y - f y)
hufp : u y - f y < 0
hua : ε = -(u y - f y)
h5 : f y < u ↑z
⊢ u y < u ↑z
Tactic:
linarith
State after:
no goals

State before:
case inr
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < -(u y - f y)
hufp : u y - f y < 0
hua : ε = -(u y - f y)
h6 : ¬f y < u ↑z
⊢ u y < u ↑z
Tactic:
have : u z - f y ≤ 0 := by linarith
State after:
case inr
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < -(u y - f y)
hufp : u y - f y < 0
hua : ε = -(u y - f y)
h6 : ¬f y < u ↑z
this : u ↑z - f y ≤ 0
⊢ u y < u ↑z

State before:
case inr
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < -(u y - f y)
hufp : u y - f y < 0
hua : ε = -(u y - f y)
h6 : ¬f y < u ↑z
this : u ↑z - f y ≤ 0
⊢ u y < u ↑z
Tactic:
rw[abs_eq_neg_self.mpr this] at hbzb
State after:
case inr
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : -(u ↑z - f y) < -(u y - f y)
hufp : u y - f y < 0
hua : ε = -(u y - f y)
h6 : ¬f y < u ↑z
this : u ↑z - f y ≤ 0
⊢ u y < u ↑z

State before:
case inr
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : -(u ↑z - f y) < -(u y - f y)
hufp : u y - f y < 0
hua : ε = -(u y - f y)
h6 : ¬f y < u ↑z
this : u ↑z - f y ≤ 0
⊢ u y < u ↑z
Tactic:
linarith
State after:
no goals

State before:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h1 : u y < f y
z : ℚ
h_z_lt_y : ↑z < y
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < -(u y - f y)
hufp : u y - f y < 0
hua : ε = -(u y - f y)
h6 : ¬f y < u ↑z
⊢ u ↑z - f y ≤ 0
Tactic:
linarith
State after:
no goals

State before:
case intro.intro.intro.inr.inl
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h2 : u y = f y
⊢ False
Tactic:
exact hy h2
State after:
no goals

State before:
case intro.intro.intro.inr.inr
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
⊢ False
Tactic:
have : ∃ z : ℚ, y < z ∧ dist (z:ℝ) y < δ := by
  have hyδ : y < y + δ := lt_add_of_pos_right y hδ0
  obtain ⟨z, hz1, hz2⟩ := exists_rat_btwn hyδ
  refine ⟨z, hz1, ?_⟩
  . rw [Real.dist_eq, abs_of_pos (sub_pos.mpr hz1)]
    exact sub_left_lt_of_lt_add hz2
State after:
case intro.intro.intro.inr.inr
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
this : ∃ z, y < ↑z ∧ dist (↑z) y < δ
⊢ False

State before:
case intro.intro.intro.inr.inr
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
this : ∃ z, y < ↑z ∧ dist (↑z) y < δ
⊢ False
Tactic:
obtain ⟨z, h_y_lt_z, hyz⟩ := this
State after:
case intro.intro.intro.inr.inr.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
⊢ False

State before:
case intro.intro.intro.inr.inr.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
⊢ False
Tactic:
have hbzb := hδ z hyz
State after:
case intro.intro.intro.inr.inr.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : dist (f ↑z) (f y) < ε
⊢ False

State before:
case intro.intro.intro.inr.inr.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : dist (f ↑z) (f y) < ε
⊢ False
Tactic:
rw [←h z] at hbzb
State after:
case intro.intro.intro.inr.inr.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
⊢ False

State before:
case intro.intro.intro.inr.inr.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
huzuy : u ↑z < u y
⊢ False
Tactic:
have h_y_le_z := le_of_lt h_y_lt_z
State after:
case intro.intro.intro.inr.inr.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
huzuy : u ↑z < u y
h_y_le_z : y ≤ ↑z
⊢ False

State before:
case intro.intro.intro.inr.inr.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
huzuy : u ↑z < u y
h_y_le_z : y ≤ ↑z
⊢ False
Tactic:
have := u_mono h_y_le_z
State after:
case intro.intro.intro.inr.inr.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
huzuy : u ↑z < u y
h_y_le_z : y ≤ ↑z
this : u y ≤ u ↑z
⊢ False

State before:
case intro.intro.intro.inr.inr.intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
huzuy : u ↑z < u y
h_y_le_z : y ≤ ↑z
this : u y ≤ u ↑z
⊢ False
Tactic:
linarith
State after:
no goals

State before:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
⊢ ∃ z, y < ↑z ∧ dist (↑z) y < δ
Tactic:
have hyδ : y < y + δ := lt_add_of_pos_right y hδ0
State after:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
hyδ : y < y + δ
⊢ ∃ z, y < ↑z ∧ dist (↑z) y < δ

State before:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
hyδ : y < y + δ
⊢ ∃ z, y < ↑z ∧ dist (↑z) y < δ
Tactic:
obtain ⟨z, hz1, hz2⟩ := exists_rat_btwn hyδ
State after:
case intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
hyδ : y < y + δ
z : ℚ
hz1 : y < ↑z
hz2 : ↑z < y + δ
⊢ ∃ z, y < ↑z ∧ dist (↑z) y < δ

State before:
case intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
hyδ : y < y + δ
z : ℚ
hz1 : y < ↑z
hz2 : ↑z < y + δ
⊢ ∃ z, y < ↑z ∧ dist (↑z) y < δ
Tactic:
refine ⟨z, hz1, ?_⟩
State after:
case intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
hyδ : y < y + δ
z : ℚ
hz1 : y < ↑z
hz2 : ↑z < y + δ
⊢ dist (↑z) y < δ

State before:
case intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
hyδ : y < y + δ
z : ℚ
hz1 : y < ↑z
hz2 : ↑z < y + δ
⊢ dist (↑z) y < δ
Tactic:
. rw [Real.dist_eq, abs_of_pos (sub_pos.mpr hz1)]
  exact sub_left_lt_of_lt_add hz2
State after:
no goals

State before:
case intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
hyδ : y < y + δ
z : ℚ
hz1 : y < ↑z
hz2 : ↑z < y + δ
⊢ dist (↑z) y < δ
Tactic:
rw [Real.dist_eq, abs_of_pos (sub_pos.mpr hz1)]
State after:
case intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
hyδ : y < y + δ
z : ℚ
hz1 : y < ↑z
hz2 : ↑z < y + δ
⊢ ↑z - y < δ

State before:
case intro.intro
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
hyδ : y < y + δ
z : ℚ
hz1 : y < ↑z
hz2 : ↑z < y + δ
⊢ ↑z - y < δ
Tactic:
exact sub_left_lt_of_lt_add hz2
State after:
no goals

State before:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
⊢ u ↑z < u y
Tactic:
have hufp : 0 < u y - f y := by linarith
State after:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
hufp : 0 < u y - f y
⊢ u ↑z < u y

State before:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
hufp : 0 < u y - f y
⊢ u ↑z < u y
Tactic:
have hua : ε = u y - f y := abs_of_pos hufp
State after:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
hufp : 0 < u y - f y
hua : ε = u y - f y
⊢ u ↑z < u y

State before:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
hufp : 0 < u y - f y
hua : ε = u y - f y
⊢ u ↑z < u y
Tactic:
rw [hua, Real.dist_eq] at hbzb
State after:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
⊢ u ↑z < u y

State before:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
⊢ u ↑z < u y
Tactic:
cases em (f y < u z)
State after:
case inl
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h✝ : f y < u ↑z
⊢ u ↑z < u y

case inr
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h✝ : ¬f y < u ↑z
⊢ u ↑z < u y

State before:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : dist (u ↑z) (f y) < ε
⊢ 0 < u y - f y
Tactic:
linarith
State after:
no goals

State before:
case inl
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h✝ : f y < u ↑z
⊢ u ↑z < u y
Tactic:
have : 0 ≤ u z - f y := by linarith
State after:
case inl
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h✝ : f y < u ↑z
this : 0 ≤ u ↑z - f y
⊢ u ↑z < u y

State before:
case inl
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h✝ : f y < u ↑z
this : 0 ≤ u ↑z - f y
⊢ u ↑z < u y
Tactic:
rw[abs_eq_self.mpr this] at hbzb
State after:
case inl
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : u ↑z - f y < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h✝ : f y < u ↑z
this : 0 ≤ u ↑z - f y
⊢ u ↑z < u y

State before:
case inl
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : u ↑z - f y < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h✝ : f y < u ↑z
this : 0 ≤ u ↑z - f y
⊢ u ↑z < u y
Tactic:
linarith
State after:
no goals

State before:
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h✝ : f y < u ↑z
⊢ 0 ≤ u ↑z - f y
Tactic:
linarith
State after:
no goals

State before:
case inr
u f : ℝ → ℝ
u_mono : Monotone u
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
y : ℝ
hy : u y ≠ f y
ε : ℝ := |u y - f y|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a y < δ → dist (f a) (f y) < ε
h3 : f y < u y
z : ℚ
h_y_lt_z : y < ↑z
hyz : dist (↑z) y < δ
hbzb : |u ↑z - f y| < u y - f y
hufp : 0 < u y - f y
hua : ε = u y - f y
h✝ : ¬f y < u ↑z
⊢ u ↑z < u y
Tactic:
linarith
State after:
no goals