case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), ↑f x < x + z
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f y - y ≤ ↑f x - x
⊢ τ f < z
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), ↑f x < x + z
⊢ τ f < z
obtain ⟨x, -, hx⟩ : ∃ x ∈ Icc (0 : ℝ) 1, ∀ y ∈ Icc (0 : ℝ) 1, f y - y ≤ f x - x :=
  isCompact_Icc.exists_forall_ge (nonempty_Icc.2 zero_le_one)
    (hf.sub continuous_id).continuousOn
case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), ↑f x < x + z
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f y - y ≤ ↑f x - x
⊢ τ f ≤ ↑f x - x
case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), ↑f x < x + z
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f y - y ≤ ↑f x - x
⊢ τ f < z
refine' lt_of_le_of_lt _ (sub_lt_iff_lt_add'.2 <| hz x)
case intro.intro.hz
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), ↑f x < x + z
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f y - y ≤ ↑f x - x
⊢ ∀ (x_1 : ℝ), ↑f x_1 ≤ x_1 + (↑f x - x)
case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), ↑f x < x + z
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f y - y ≤ ↑f x - x
⊢ τ f ≤ ↑f x - x
apply translationNumber_le_of_le_add
case intro.intro.hz
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), ↑f x < x + z
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f y - y ≤ ↑f x - x
⊢ ∀ (x_1 : ℝ), ↑f x_1 - x_1 ≤ ↑f x - x
case intro.intro.hz
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), ↑f x < x + z
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f y - y ≤ ↑f x - x
⊢ ∀ (x_1 : ℝ), ↑f x_1 ≤ x_1 + (↑f x - x)
simp only [← sub_le_iff_le_add']
no goals
case intro.intro.hz
f g : CircleDeg1Lift
hf : Continuous ↑f
z : ℝ
hz : ∀ (x : ℝ), ↑f x < x + z
x : ℝ
hx : ∀ (y : ℝ), y ∈ Icc 0 1 → ↑f y - y ≤ ↑f x - x
⊢ ∀ (x_1 : ℝ), ↑f x_1 - x_1 ≤ ↑f x - x
exact f.forall_map_sub_of_Icc (fun a => a ≤ f x - x) hx