f g : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun n => (↑(f ^ n) x - x) / ↑n) atTop
    (𝓝 (τ (↑(↑translate (↑Multiplicative.ofAdd x))⁻¹ * f * ↑(↑translate (↑Multiplicative.ofAdd x)))))
f g : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun n => (↑(f ^ n) x - x) / ↑n) atTop (𝓝 (τ f))
rw [← translationNumber_conj_eq' (translate <| Multiplicative.ofAdd x)]
f g : CircleDeg1Lift
x : ℝ
n : ℕ
⊢ ↑((↑(↑translate (↑Multiplicative.ofAdd x))⁻¹ * f * ↑(↑translate (↑Multiplicative.ofAdd x))) ^ n) 0 / ↑n =
    (↑(f ^ n) x - x) / ↑n
f g : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun n => (↑(f ^ n) x - x) / ↑n) atTop
    (𝓝 (τ (↑(↑translate (↑Multiplicative.ofAdd x))⁻¹ * f * ↑(↑translate (↑Multiplicative.ofAdd x)))))
refine (tendsto_translation_number₀ _).congr fun n ↦ ?_
no goals
f g : CircleDeg1Lift
x : ℝ
n : ℕ
⊢ ↑((↑(↑translate (↑Multiplicative.ofAdd x))⁻¹ * f * ↑(↑translate (↑Multiplicative.ofAdd x))) ^ n) 0 / ↑n =
    (↑(f ^ n) x - x) / ↑n
simp [sub_eq_neg_add, Units.conj_pow']