f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
⊢ ∃ x, x ∈ Icc 0 1 ∧ ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y

case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
⊢ z < τ f
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
⊢ z < τ f
obtain ⟨x, -, hx⟩ : ∃ x ∈ Icc (0 : ℝ) 1, ∀ y ∈ Icc (0 : ℝ) 1, f x - x ≤ f y - y
case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
⊢ z < τ f
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
⊢ ∃ x, x ∈ Icc 0 1 ∧ ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y

case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
⊢ z < τ f
exact isCompact_Icc.exists_forall_le (nonempty_Icc.2 zero_le_one)
  (hf.sub continuous_id).continuousOn
case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
⊢ ↑f x - x ≤ τ f
case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
⊢ z < τ f
refine' lt_of_lt_of_le (lt_sub_iff_add_lt'.2 <| hz x) _
case intro.intro.hz
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
⊢ ∀ (x_1 : ℝ), x_1 + (↑f x - x) ≤ ↑f x_1
case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
⊢ ↑f x - x ≤ τ f
apply le_translationNumber_of_add_le
case intro.intro.hz
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
⊢ ∀ (x_1 : ℝ), ↑f x - x ≤ ↑f x_1 - x_1
case intro.intro.hz
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
⊢ ∀ (x_1 : ℝ), x_1 + (↑f x - x) ≤ ↑f x_1
simp only [← le_sub_iff_add_le']
no goals
case intro.intro.hz
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), x + z < ↑f x
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f x - x ≤ ↑f y - y
⊢ ∀ (x_1 : ℝ), ↑f x - x ≤ ↑f x_1 - x_1
exact f.forall_map_sub_of_Icc _ hx