f g : CircleDeg1Lift
n : ℕ
⊢ dist (↑(f ^ (n + 1)) 0 / (↑n + 1)) (τ f) ≤ ((fun n => 1 / ↑n) ∘ fun a => a + 1) n
f g : CircleDeg1Lift
⊢ Tendsto (fun n => ↑(f ^ (n + 1)) 0 / (↑n + 1)) atTop (𝓝 (τ f))
refine'
  tendsto_iff_dist_tendsto_zero.2 <|
    squeeze_zero (fun _ => dist_nonneg) (fun n => _)
      ((tendsto_const_div_atTop_nhds_0_nat 1).comp (tendsto_add_atTop_nat 1))
f g : CircleDeg1Lift
n : ℕ
⊢ dist (↑(f ^ (n + 1)) 0 / (↑n + 1)) (τ f) ≤ 1 / ↑(n + 1)
f g : CircleDeg1Lift
n : ℕ
⊢ dist (↑(f ^ (n + 1)) 0 / (↑n + 1)) (τ f) ≤ ((fun n => 1 / ↑n) ∘ fun a => a + 1) n
dsimp
f g : CircleDeg1Lift
n : ℕ
this : 0 < ↑n + 1
⊢ dist (↑(f ^ (n + 1)) 0 / (↑n + 1)) (τ f) ≤ 1 / ↑(n + 1)
f g : CircleDeg1Lift
n : ℕ
⊢ dist (↑(f ^ (n + 1)) 0 / (↑n + 1)) (τ f) ≤ 1 / ↑(n + 1)
have : (0 : ℝ) < n + 1 := n.cast_add_one_pos
f g : CircleDeg1Lift
n : ℕ
this : 0 < ↑n + 1
⊢ dist (↑(f ^ (n + 1)) 0) (↑(n + 1) * τ f) ≤ 1
f g : CircleDeg1Lift
n : ℕ
this : 0 < ↑n + 1
⊢ dist (↑(f ^ (n + 1)) 0 / (↑n + 1)) (τ f) ≤ 1 / ↑(n + 1)
rw [Real.dist_eq, div_sub' _ _ _ (ne_of_gt this), abs_div, ← Real.dist_eq, abs_of_pos this,
  Nat.cast_add_one, div_le_div_right this, ← Nat.cast_add_one]
no goals
f g : CircleDeg1Lift
n : ℕ
this : 0 < ↑n + 1
⊢ dist (↑(f ^ (n + 1)) 0) (↑(n + 1) * τ f) ≤ 1
apply dist_pow_map_zero_mul_translationNumber_le