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

State before:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
⊢ u x = f x
Tactic:
by_contra! hx
State after:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
⊢ False

State before:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
⊢ False
Tactic:
let ε : ℝ := |u x - f x|
State after:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
⊢ False

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

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

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

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

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

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

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

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

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

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

State before:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
⊢ ∃ z, ↑z < x ∧ dist (↑z) x < δ ∧ 0 < ↑z
Tactic:
obtain h3 | h4 := le_or_lt x δ
State after:
case inl
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
h3 : x ≤ δ
⊢ ∃ z, ↑z < x ∧ dist (↑z) x < δ ∧ 0 < ↑z

case inr
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
h4 : δ < x
⊢ ∃ z, ↑z < x ∧ dist (↑z) x < δ ∧ 0 < ↑z

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

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

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

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

State before:
case inr.intro.intro
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
h4 : δ < x
hxδ : x - δ < x
z : ℚ
hz1 : x - δ < ↑z
hz2 : ↑z < x
⊢ x - ↑z < δ ∧ 0 < ↑z
Tactic:
constructor
State after:
case inr.intro.intro.left
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
h4 : δ < x
hxδ : x - δ < x
z : ℚ
hz1 : x - δ < ↑z
hz2 : ↑z < x
⊢ x - ↑z < δ

case inr.intro.intro.right
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
h4 : δ < x
hxδ : x - δ < x
z : ℚ
hz1 : x - δ < ↑z
hz2 : ↑z < x
⊢ 0 < ↑z

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

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

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

State before:
case inl.intro.intro
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
h3 : x ≤ δ
z : ℚ
hz1 : 0 < ↑z
hz2 : ↑z < x
⊢ x - ↑z < δ ∧ 0 < ↑z
Tactic:
constructor
State after:
case inl.intro.intro.left
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
h3 : x ≤ δ
z : ℚ
hz1 : 0 < ↑z
hz2 : ↑z < x
⊢ x - ↑z < δ

case inl.intro.intro.right
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
h3 : x ≤ δ
z : ℚ
hz1 : 0 < ↑z
hz2 : ↑z < x
⊢ 0 < ↑z

State before:
case inl.intro.intro.left
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
h3 : x ≤ δ
z : ℚ
hz1 : 0 < ↑z
hz2 : ↑z < x
⊢ x - ↑z < δ
Tactic:
linarith
State after:
no goals

State before:
case inl.intro.intro.right
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
h3 : x ≤ δ
z : ℚ
hz1 : 0 < ↑z
hz2 : ↑z < x
⊢ 0 < ↑z
Tactic:
linarith
State after:
no goals

State before:
case inr.intro.intro.left
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
h4 : δ < x
hxδ : x - δ < x
z : ℚ
hz1 : x - δ < ↑z
hz2 : ↑z < x
⊢ x - ↑z < δ
Tactic:
linarith
State after:
no goals

State before:
case inr.intro.intro.right
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
h4 : δ < x
hxδ : x - δ < x
z : ℚ
hz1 : x - δ < ↑z
hz2 : ↑z < x
⊢ 0 < ↑z
Tactic:
linarith
State after:
no goals

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

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

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

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

case inr
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
z : ℚ
h_z_lt_x : ↑z < x
hxz : dist (↑z) x < δ
zpos : 0 < ↑z
hbzb : |u ↑z - f x| < -(u x - f x)
hufp : u x - f x < 0
hua : ε = -(u x - f x)
h6 : ¬f x < u ↑z
⊢ u x < u ↑z

State before:
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h1 : u x < f x
z : ℚ
h_z_lt_x : ↑z < x
hxz : dist (↑z) x < δ
zpos : 0 < ↑z
hbzb : dist (u ↑z) (f x) < ε
⊢ u x - f x < 0
Tactic:
linarith
State after:
no goals

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

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

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

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

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

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

State before:
case intro.intro.inr.inr
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
⊢ False
Tactic:
have : ∃ z : ℚ, x < z ∧ dist (z:ℝ) x < δ := by
  have hxδ : x < x + δ := lt_add_of_pos_right x hδ0
  obtain ⟨z, hz1, hz2⟩ := exists_rat_btwn hxδ
  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.inr.inr
u f : ℝ → ℝ
u_mono : ∀ (x y : ℝ), 0 ≤ x → x ≤ y → u x ≤ u y
f_cont : Continuous f
h : ∀ (x : ℚ), u ↑x = f ↑x
x : ℝ
xpos : 0 < x
hx : u x ≠ f x
ε : ℝ := |u x - f x|
hε : 0 < ε
δ : ℝ
hδ0 : δ > 0
hδ : ∀ (a : ℝ), dist a x < δ → dist (f a) (f x) < ε
h3 : f x < u x
this : ∃ z, x < ↑z ∧ dist (↑z) x < δ
⊢ False

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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