f g : CircleDeg1Lift
x : ℝ
⊢ ↑f x < x + (↑⌊τ f⌋ + 1)
f g : CircleDeg1Lift
x : ℝ
⊢ ↑f x < x + ↑⌊τ f⌋ + 1
rw [add_assoc]
f g : CircleDeg1Lift
x : ℝ
⊢ ↑f x < x + ↑(⌊τ f⌋ + 1)
f g : CircleDeg1Lift
x : ℝ
⊢ ↑f x < x + (↑⌊τ f⌋ + 1)
norm_cast
f g : CircleDeg1Lift
x : ℝ
⊢ τ f < ↑(⌊τ f⌋ + 1)
f g : CircleDeg1Lift
x : ℝ
⊢ ↑f x < x + ↑(⌊τ f⌋ + 1)
refine' map_lt_of_translationNumber_lt_int _ _ _
f g : CircleDeg1Lift
x : ℝ
⊢ τ f < ↑⌊τ f⌋ + 1
f g : CircleDeg1Lift
x : ℝ
⊢ τ f < ↑(⌊τ f⌋ + 1)
push_cast
no goals
f g : CircleDeg1Lift
x : ℝ
⊢ τ f < ↑⌊τ f⌋ + 1
exact lt_floor_add_one _