case intro
f g : CircleDeg1Lift
hf : Continuous ↑f
a : ℝ
ha : ↑f a ≤ a + τ f
⊢ ∃ x, ↑f x = x + τ f
f g : CircleDeg1Lift
hf : Continuous ↑f
⊢ ∃ x, ↑f x = x + τ f
obtain ⟨a, ha⟩ : ∃ x, f x ≤ x + τ f := by
  by_contra' H
  exact lt_irrefl _ (f.lt_translationNumber_of_forall_add_lt hf H)
case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
a : ℝ
ha : ↑f a ≤ a + τ f
b : ℝ
hb : b + τ f ≤ ↑f b
⊢ ∃ x, ↑f x = x + τ f
case intro
f g : CircleDeg1Lift
hf : Continuous ↑f
a : ℝ
ha : ↑f a ≤ a + τ f
⊢ ∃ x, ↑f x = x + τ f
obtain ⟨b, hb⟩ : ∃ x, x + τ f ≤ f x := by
  by_contra' H
  exact lt_irrefl _ (f.translationNumber_lt_of_forall_lt_add hf H)
no goals
case intro.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
a : ℝ
ha : ↑f a ≤ a + τ f
b : ℝ
hb : b + τ f ≤ ↑f b
⊢ ∃ x, ↑f x = x + τ f
exact intermediate_value_univ₂ hf (continuous_id.add continuous_const) ha hb
f g : CircleDeg1Lift
hf : Continuous ↑f
H : ∀ (x : ℝ), x + τ f < ↑f x
⊢ False
f g : CircleDeg1Lift
hf : Continuous ↑f
⊢ ∃ x, ↑f x ≤ x + τ f
by_contra' H
no goals
f g : CircleDeg1Lift
hf : Continuous ↑f
H : ∀ (x : ℝ), x + τ f < ↑f x
⊢ False
exact lt_irrefl _ (f.lt_translationNumber_of_forall_add_lt hf H)
f g : CircleDeg1Lift
hf : Continuous ↑f
a : ℝ
ha : ↑f a ≤ a + τ f
H : ∀ (x : ℝ), ↑f x < x + τ f
⊢ False
f g : CircleDeg1Lift
hf : Continuous ↑f
a : ℝ
ha : ↑f a ≤ a + τ f
⊢ ∃ x, x + τ f ≤ ↑f x
by_contra' H
no goals
f g : CircleDeg1Lift
hf : Continuous ↑f
a : ℝ
ha : ↑f a ≤ a + τ f
H : ∀ (x : ℝ), ↑f x < x + τ f
⊢ False
exact lt_irrefl _ (f.translationNumber_lt_of_forall_lt_add hf H)