f✝ g✝ f g : CircleDeg1Lift
h : Commute f g
⊢ Tendsto (fun x => transnumAuxSeq f x + transnumAuxSeq g x) atTop (𝓝 (τ (f * g)))
f✝ g✝ f g : CircleDeg1Lift
h : Commute f g
⊢ τ (f * g) = τ f + τ g
refine tendsto_nhds_unique ?_
  (f.tendsto_translationNumber_aux.add g.tendsto_translationNumber_aux)
f✝ g✝ f g : CircleDeg1Lift
h : Commute f g
⊢ Tendsto (fun x => (↑(f ^ 2 ^ x) 0 + ↑(g ^ 2 ^ x) 0) / 2 ^ x) atTop (𝓝 (τ (f * g)))
f✝ g✝ f g : CircleDeg1Lift
h : Commute f g
⊢ Tendsto (fun x => transnumAuxSeq f x + transnumAuxSeq g x) atTop (𝓝 (τ (f * g)))
simp only [transnumAuxSeq, ← add_div]
f✝ g✝ f g : CircleDeg1Lift
h : Commute f g
n : ℕ
⊢ dist (↑((f * g) ^ n) 0) ((fun n => ↑(f ^ n) 0 + ↑(g ^ n) 0) n) ≤ 1
f✝ g✝ f g : CircleDeg1Lift
h : Commute f g
⊢ Tendsto (fun x => (↑(f ^ 2 ^ x) 0 + ↑(g ^ 2 ^ x) 0) / 2 ^ x) atTop (𝓝 (τ (f * g)))
refine (f * g).tendsto_translationNumber_of_dist_bounded_aux
  (fun n ↦ (f ^ n) 0 + (g ^ n) 0) 1 fun n ↦ ?_
f✝ g✝ f g : CircleDeg1Lift
h : Commute f g
n : ℕ
⊢ dist ((fun n => ↑(f ^ n) 0 + ↑(g ^ n) 0) n) (↑(f ^ n * g ^ n) 0) ≤ 1
f✝ g✝ f g : CircleDeg1Lift
h : Commute f g
n : ℕ
⊢ dist (↑((f * g) ^ n) 0) ((fun n => ↑(f ^ n) 0 + ↑(g ^ n) 0) n) ≤ 1
rw [h.mul_pow, dist_comm]
no goals
f✝ g✝ f g : CircleDeg1Lift
h : Commute f g
n : ℕ
⊢ dist ((fun n => ↑(f ^ n) 0 + ↑(g ^ n) 0) n) (↑(f ^ n * g ^ n) 0) ≤ 1
exact le_of_lt ((f ^ n).dist_map_map_zero_lt (g ^ n))