case mp
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
⊢ τ f = ↑m → ∃ x, ↑f x = x + ↑m

case mpr
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
⊢ (∃ x, ↑f x = x + ↑m) → τ f = ↑m
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
⊢ τ f = ↑m ↔ ∃ x, ↑f x = x + ↑m
constructor
case mp
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
h : τ f = ↑m
⊢ ∃ x, ↑f x = x + ↑m
case mp
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
⊢ τ f = ↑m → ∃ x, ↑f x = x + ↑m
intro h
case mp
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
h : τ f = ↑m
⊢ ∃ x, ↑f x = x + τ f
case mp
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
h : τ f = ↑m
⊢ ∃ x, ↑f x = x + ↑m
simp only [← h]
no goals
case mp
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
h : τ f = ↑m
⊢ ∃ x, ↑f x = x + τ f
exact f.exists_eq_add_translationNumber hf
case mpr.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
x : ℝ
hx : ↑f x = x + ↑m
⊢ τ f = ↑m
case mpr
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
⊢ (∃ x, ↑f x = x + ↑m) → τ f = ↑m
rintro ⟨x, hx⟩
no goals
case mpr.intro
f g : CircleDeg1Lift
hf : Continuous ↑f
m : ℤ
x : ℝ
hx : ↑f x = x + ↑m
⊢ τ f = ↑m
exact f.translationNumber_of_eq_add_int hx