case refine'_1
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
⊢ ℕ → ℝ

case refine'_2
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
⊢ ∀ (t : ℕ), dist (transnumAuxSeq f t) (x (2 ^ t) / 2 ^ t) ≤ ?refine'_1 t

case refine'_3
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
⊢ Tendsto ?refine'_1 atTop (𝓝 0)
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
⊢ Tendsto (fun n => x (2 ^ n) / 2 ^ n) atTop (𝓝 (τ f))
refine' f.tendsto_translationNumber_aux.congr_dist (squeeze_zero (fun _ => dist_nonneg) _ _)
no goals
case refine'_1
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
⊢ ℕ → ℝ
exact fun n => C / 2 ^ n
case refine'_2
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
n : ℕ
⊢ dist (transnumAuxSeq f n) (x (2 ^ n) / 2 ^ n) ≤ C / 2 ^ n
case refine'_2
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
⊢ ∀ (t : ℕ), dist (transnumAuxSeq f t) (x (2 ^ t) / 2 ^ t) ≤ C / 2 ^ t
intro n
case refine'_2
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
n : ℕ
this : 0 < 2 ^ n
⊢ dist (transnumAuxSeq f n) (x (2 ^ n) / 2 ^ n) ≤ C / 2 ^ n
case refine'_2
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
n : ℕ
⊢ dist (transnumAuxSeq f n) (x (2 ^ n) / 2 ^ n) ≤ C / 2 ^ n
have : 0 < (2 ^ n : ℝ) := pow_pos zero_lt_two _
case h.e'_3
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
n : ℕ
this : 0 < 2 ^ n
⊢ dist (transnumAuxSeq f n) (x (2 ^ n) / 2 ^ n) = dist (↑(f ^ 2 ^ n) 0) (x (2 ^ n)) / 2 ^ n
case refine'_2
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
n : ℕ
this : 0 < 2 ^ n
⊢ dist (transnumAuxSeq f n) (x (2 ^ n) / 2 ^ n) ≤ C / 2 ^ n
convert (div_le_div_right this).2 (H (2 ^ n)) using 1
no goals
case h.e'_3
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
n : ℕ
this : 0 < 2 ^ n
⊢ dist (transnumAuxSeq f n) (x (2 ^ n) / 2 ^ n) = dist (↑(f ^ 2 ^ n) 0) (x (2 ^ n)) / 2 ^ n
rw [transnumAuxSeq, Real.dist_eq, ← sub_div, abs_div, abs_of_pos this, Real.dist_eq]
no goals
case refine'_3
f g : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist (↑(f ^ n) 0) (x n) ≤ C
⊢ Tendsto (fun n => C / 2 ^ n) atTop (𝓝 0)
exact mul_zero C ▸ tendsto_const_nhds.mul <| tendsto_inv_atTop_zero.comp <|
  tendsto_pow_atTop_atTop_of_one_lt one_lt_two