awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n : (a : ℝ) → ℝ) 0) (x n) ≤ C
n : ℕ
this : 0 < HPow.hPow (α := ℝ) 2 n
⊢ dist ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0) (x (HPow.hPow (α := ℕ) 2 n)) / HPow.hPow (α := ℝ) 2 n ≤
    C / HPow.hPow (α := ℝ) 2 n

Tactic:
(div_le_div_iff_of_pos_right this).2 (H (2 ^ n))

Premises used: Iff.mpr, div_le_div_iff_of_pos_right, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n : (a : ℝ) → ℝ) 0) (x n) ≤ C
n : ℕ
this : 0 < HPow.hPow (α := ℝ) 2 n
h :
  dist (f.transnumAuxSeq n) (x (HPow.hPow (α := ℕ) 2 n) / HPow.hPow (α := ℝ) 2 n) =
    dist ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0) (x (HPow.hPow (α := ℕ) 2 n)) / HPow.hPow (α := ℝ) 2 n
⊢ dist (f.transnumAuxSeq n) (x (HPow.hPow (α := ℕ) 2 n) / HPow.hPow (α := ℝ) 2 n) ≤ C / HPow.hPow (α := ℝ) 2 n

Tactic:
convert! (div_le_div_iff_of_pos_right this).2 (H (2 ^ n)) using 1

Premises used: Iff.mpr, div_le_div_iff_of_pos_right, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n : (a : ℝ) → ℝ) 0) (x n) ≤ C
n : ℕ
this : 0 < HPow.hPow (α := ℝ) 2 n
h :
  dist (HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n))
      (x (HPow.hPow (α := ℕ) 2 n) / HPow.hPow (α := ℝ) 2 n) =
    dist ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0) (x (HPow.hPow (α := ℕ) 2 n)) / HPow.hPow (α := ℝ) 2 n
h₁ :
  |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
        x (HPow.hPow (α := ℕ) 2 n) / HPow.hPow (α := ℝ) 2 n| =
    dist ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0) (x (HPow.hPow (α := ℕ) 2 n)) / HPow.hPow (α := ℝ) 2 n
h₂ :
  |HSub.hSub (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (x (HPow.hPow (α := ℕ) 2 n)) /
        HPow.hPow (α := ℝ) 2 n| =
    dist ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0) (x (HPow.hPow (α := ℕ) 2 n)) / HPow.hPow (α := ℝ) 2 n
h₃ :
  |HSub.hSub (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (x (HPow.hPow (α := ℕ) 2 n))| /
      |HPow.hPow (α := ℝ) 2 n| =
    dist ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0) (x (HPow.hPow (α := ℕ) 2 n)) / HPow.hPow (α := ℝ) 2 n
h₄ :
  |HSub.hSub (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (x (HPow.hPow (α := ℕ) 2 n))| /
      HPow.hPow (α := ℝ) 2 n =
    dist ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0) (x (HPow.hPow (α := ℕ) 2 n)) / HPow.hPow (α := ℝ) 2 n
h₅ h₆ :
  |HSub.hSub (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (x (HPow.hPow (α := ℕ) 2 n))| /
      HPow.hPow (α := ℝ) 2 n =
    |HSub.hSub (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (x (HPow.hPow (α := ℕ) 2 n))| /
      HPow.hPow (α := ℝ) 2 n
⊢ dist (f.transnumAuxSeq n) (x (HPow.hPow (α := ℕ) 2 n) / HPow.hPow (α := ℝ) 2 n) =
    dist ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0) (x (HPow.hPow (α := ℕ) 2 n)) / HPow.hPow (α := ℝ) 2 n

Tactic:
rw [transnumAuxSeq, Real.dist_eq, ← sub_div, abs_div, abs_of_pos this, Real.dist_eq]

Premises used: abs_div, sub_div, Real.dist_eq, abs_of_pos, CircleDeg1Lift.transnumAuxSeq
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n : (a : ℝ) → ℝ) 0) (x n) ≤ C
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (α := ℝ) 2 n) atTop (𝓝 0)

Tactic:
exact mul_zero C ▸ tendsto_const_nhds.mul <| tendsto_inv_atTop_zero.comp <|
      tendsto_pow_atTop_atTop_of_one_lt one_lt_two

Premises used: tendsto_inv_atTop_zero, tendsto_pow_atTop_atTop_of_one_lt, one_lt_two, Filter.Tendsto.comp
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
C : ℝ
H : ∀ (n : ℕ), dist (α := ℝ) ((f ^ n : (a : ℝ) → ℝ) 0 : ℝ) ((g ^ n : (a : ℝ) → ℝ) 0 : ℝ) ≤ C
⊢ τ f = τ g

Tactic:
Eq.symm <| g.translationNumber_eq_of_tendsto_aux <|
    f.tendsto_translationNumber_of_dist_bounded_aux (fun n ↦ (g ^ n) 0) C H

Premises used: HPow.hPow, CircleDeg1Lift.translationNumber_eq_of_tendsto_aux, OfNat.ofNat, Eq.symm, DFunLike.coe, CircleDeg1Lift.tendsto_translationNumber_of_dist_bounded_aux
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) ((⇑1 : (a : ℝ) → ℝ)^[n] 0) (↑n : ℝ)) atTop (𝓝 0)

Tactic:
simp
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g₁ g₂ : CircleDeg1Lift
H : SemiconjBy f g₁ g₂
⊢ τ g₁ = τ g₂

Tactic:
translationNumber_eq_of_dist_bounded 2 fun n =>
    le_of_lt <| dist_map_zero_lt_of_semiconjBy <| H.pow_right n

Premises used: le_of_lt, SemiconjBy.pow_right, CircleDeg1Lift.translationNumber_eq_of_dist_bounded, OfNat.ofNat, CircleDeg1Lift.dist_map_zero_lt_of_semiconjBy
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g₁ g₂ : CircleDeg1Lift
H : Semiconj (α := ℝ) (β := ℝ) (⇑f : (a : ℝ) → ℝ) (⇑g₁ : (a : ℝ) → ℝ) (⇑g₂ : (a : ℝ) → ℝ)
⊢ τ g₁ = τ g₂

Tactic:
translationNumber_eq_of_semiconjBy <| semiconjBy_iff_semiconj.2 H

Premises used: Iff.mpr, CircleDeg1Lift.translationNumber_eq_of_semiconjBy, CircleDeg1Lift.semiconjBy_iff_semiconj
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
h : Commute f g
⊢ τ (f * g) = τ f + τ g

Tactic:
tendsto_nhds_unique ?_
    (f.tendsto_translationNumber_aux.add g.tendsto_translationNumber_aux)

Premises used: CircleDeg1Lift.tendsto_translationNumber_aux, Filter.Tendsto.add, tendsto_nhds_unique
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
h : Commute f g
refine : Tendsto (fun (x : ℕ) ↦ f.transnumAuxSeq x + g.transnumAuxSeq x) atTop (𝓝 (τ (f * g)))
⊢ τ (f * g) = τ f + τ g

Tactic:
refine tendsto_nhds_unique ?_
    (f.tendsto_translationNumber_aux.add g.tendsto_translationNumber_aux)

Premises used: CircleDeg1Lift.tendsto_translationNumber_aux, Filter.Tendsto.add, tendsto_nhds_unique
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
h : Commute f g
simp :
  Tendsto
    (fun (x : ℕ) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 x : (a : ℝ) → ℝ) 0 : ℝ)
          ((g ^ HPow.hPow (α := ℕ) 2 x : (a : ℝ) → ℝ) 0 : ℝ) /
        HPow.hPow (α := ℝ) 2 x)
    atTop (𝓝 (τ (f * g)))
⊢ Tendsto (fun (x : ℕ) ↦ f.transnumAuxSeq x + g.transnumAuxSeq x) atTop (𝓝 (τ (f * g)))

Tactic:
simp only [transnumAuxSeq, ← add_div]

Premises used: CircleDeg1Lift.transnumAuxSeq, add_div
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
h : Commute f g
⊢ Tendsto
    (fun (x : ℕ) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 x : (a : ℝ) → ℝ) 0 : ℝ)
          ((g ^ HPow.hPow (α := ℕ) 2 x : (a : ℝ) → ℝ) 0 : ℝ) /
        HPow.hPow (α := ℝ) 2 x)
    atTop (𝓝 (τ (f * g)))

Tactic:
(f * g).tendsto_translationNumber_of_dist_bounded_aux
    (fun n ↦ (f ^ n) 0 + (g ^ n) 0) 1 fun n ↦ ?_

Premises used: HMul.hMul, HPow.hPow, HAdd.hAdd, OfNat.ofNat, DFunLike.coe, CircleDeg1Lift.tendsto_translationNumber_of_dist_bounded_aux
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
h : Commute f g
refine :
  ∀ (n : ℕ),
    dist (α := ℝ) (((f * g) ^ n : (a : ℝ) → ℝ) 0 : ℝ)
        ((fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ n : (a : ℝ) → ℝ) 0 : ℝ) ((g ^ n : (a : ℝ) → ℝ) 0 : ℝ)) n :
          ℝ) ≤
      1
⊢ Tendsto
    (fun (x : ℕ) ↦
      HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 x : (a : ℝ) → ℝ) 0 : ℝ)
          ((g ^ HPow.hPow (α := ℕ) 2 x : (a : ℝ) → ℝ) 0 : ℝ) /
        HPow.hPow (α := ℝ) 2 x)
    atTop (𝓝 (τ (f * g)))

Tactic:
refine (f * g).tendsto_translationNumber_of_dist_bounded_aux
    (fun n ↦ (f ^ n) 0 + (g ^ n) 0) 1 fun n ↦ ?_

Premises used: HMul.hMul, HPow.hPow, HAdd.hAdd, OfNat.ofNat, DFunLike.coe, CircleDeg1Lift.tendsto_translationNumber_of_dist_bounded_aux
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
h : Commute f g
n : ℕ
rw :
  dist (α := ℝ)
      ((fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ n : (a : ℝ) → ℝ) 0 : ℝ) ((g ^ n : (a : ℝ) → ℝ) 0 : ℝ)) n : ℝ)
      ((f ^ n * g ^ n : (a : ℝ) → ℝ) 0 : ℝ) ≤
    1
⊢ dist (α := ℝ) (((f * g) ^ n : (a : ℝ) → ℝ) 0 : ℝ)
      ((fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ n : (a : ℝ) → ℝ) 0 : ℝ) ((g ^ n : (a : ℝ) → ℝ) 0 : ℝ)) n : ℝ) ≤
    1

Tactic:
rw [h.mul_pow, dist_comm]

Premises used: dist_comm, Commute.mul_pow
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
h : Commute f g
n : ℕ
⊢ dist (α := ℝ)
      ((fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ n : (a : ℝ) → ℝ) 0 : ℝ) ((g ^ n : (a : ℝ) → ℝ) 0 : ℝ)) n : ℝ)
      ((f ^ n * g ^ n : (a : ℝ) → ℝ) 0 : ℝ) ≤
    1

Tactic:
le_of_lt ((f ^ n).dist_map_map_zero_lt (g ^ n))

Premises used: CircleDeg1Lift.dist_map_map_zero_lt, le_of_lt, HPow.hPow
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
h : Commute f g
n : ℕ
⊢ dist (α := ℝ)
      ((fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ n : (a : ℝ) → ℝ) 0 : ℝ) ((g ^ n : (a : ℝ) → ℝ) 0 : ℝ)) n : ℝ)
      ((f ^ n * g ^ n : (a : ℝ) → ℝ) 0 : ℝ) ≤
    1

Tactic:
exact le_of_lt ((f ^ n).dist_map_map_zero_lt (g ^ n))

Premises used: CircleDeg1Lift.dist_map_map_zero_lt, le_of_lt, HPow.hPow
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Liftˣ
⊢ τ (↑f⁻¹ : CircleDeg1Lift) + τ (↑f : CircleDeg1Lift) = 0

Tactic:
simp [← translationNumber_mul_of_commute (Commute.refl _).units_inv_left]

Premises used: CircleDeg1Lift.translationNumber_mul_of_commute, Commute.units_inv_left, Commute.refl
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
⊢ τ (HPow.hPow (β := ℕ) f 0) = (↑0 : ℝ) * τ f

Tactic:
simp
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℕ
rw : τ (f ^ n * f) = (↑(n + 1) : ℝ) * τ f
rw₁ : τ (f ^ n) + τ f = (↑(n + 1) : ℝ) * τ f
rw₂ : (↑n : ℝ) * τ f + τ f = (↑(n + 1) : ℝ) * τ f
rw₃ : (↑n : ℝ) * τ f + τ f = HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * τ f
rw₄ : (↑n : ℝ) * τ f + τ f = (↑n : ℝ) * τ f + 1 * τ f
rw₅ rw₆ : (↑n : ℝ) * τ f + τ f = (↑n : ℝ) * τ f + τ f
⊢ τ (f ^ (n + 1)) = (↑(n + 1) : ℝ) * τ f

Tactic:
rw [pow_succ, translationNumber_mul_of_commute (Commute.pow_self f n),
      translationNumber_pow n, Nat.cast_add_one, add_mul, one_mul]

Premises used: CircleDeg1Lift.translationNumber_mul_of_commute, add_mul, pow_succ, Commute.pow_self, Nat.cast_add_one, one_mul
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Liftˣ
n : ℕ
⊢ τ (↑(HPow.hPow (β := ℤ) f (↑n : ℤ)) : CircleDeg1Lift) = (↑(↑n : ℤ) : ℝ) * τ (↑f : CircleDeg1Lift)

Tactic:
simp [translationNumber_pow f n]

Premises used: Units.val, CircleDeg1Lift.translationNumber_pow
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Liftˣ
n : ℕ
simp :
  -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * τ (↑f : CircleDeg1Lift)) =
    HAdd.hAdd (α := ℝ) (-1) (-(↑n : ℝ)) * τ (↑f : CircleDeg1Lift)
⊢ τ (↑(f ^ -[n+1]) : CircleDeg1Lift) = (↑-[n+1] : ℝ) * τ (↑f : CircleDeg1Lift)

Tactic:
simp
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Liftˣ
n : ℕ
⊢ -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * τ (↑f : CircleDeg1Lift)) =
    HAdd.hAdd (α := ℝ) (-1) (-(↑n : ℝ)) * τ (↑f : CircleDeg1Lift)

Tactic:
ring
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Liftˣ
g : CircleDeg1Lift
⊢ τ ((↑f : CircleDeg1Lift) * g * (↑f⁻¹ : CircleDeg1Lift)) = τ g

Tactic:
(translationNumber_eq_of_semiconjBy (f.mk_semiconjBy g)).symm

Premises used: CircleDeg1Lift.translationNumber_eq_of_semiconjBy, Eq.symm, Units.mk_semiconjBy
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Liftˣ
g : CircleDeg1Lift
⊢ τ ((↑f⁻¹ : CircleDeg1Lift) * g * (↑f : CircleDeg1Lift)) = τ g

Tactic:
translationNumber_conj_eq f⁻¹ g

Premises used: Inv.inv, CircleDeg1Lift.translationNumber_conj_eq
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℕ
⊢ dist ((f ^ n : (a : ℝ) → ℝ) 0) ((↑n : ℝ) * τ f) ≤ 1

Tactic:
f.translationNumber_pow n ▸ (f ^ n).dist_map_zero_translationNumber_le

Premises used: CircleDeg1Lift.dist_map_zero_translationNumber_le, Eq.rec, HPow.hPow, CircleDeg1Lift.translationNumber_pow
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) ((f ^ (n + 1) : (a : ℝ) → ℝ) 0 : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) atTop
    (𝓝 (τ f))

Tactic:
tendsto_iff_dist_tendsto_zero.2 <|
      squeeze_zero (fun _ => dist_nonneg) (fun n => ?_)
        ((tendsto_const_div_atTop_nhds_zero_nat 1).comp (tendsto_add_atTop_nat 1))

Premises used: Iff.mpr, squeeze_zero, tendsto_const_div_atTop_nhds_zero_nat, dist_nonneg, Filter.tendsto_add_atTop_nat, Filter.Tendsto.comp, OfNat.ofNat, tendsto_iff_dist_tendsto_zero
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
squeeze_zero :
  ∀ (n : ℕ),
    dist (HDiv.hDiv (α := ℝ) ((f ^ (n + 1) : (a : ℝ) → ℝ) 0 : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) (τ f) ≤
      ((fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)) ∘ fun (a : ℕ) ↦ a + 1) n
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) ((f ^ (n + 1) : (a : ℝ) → ℝ) 0 : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) atTop
    (𝓝 (τ f))

Tactic:
refine
    tendsto_iff_dist_tendsto_zero.2 <|
      squeeze_zero (fun _ => dist_nonneg) (fun n => ?_)
        ((tendsto_const_div_atTop_nhds_zero_nat 1).comp (tendsto_add_atTop_nat 1))

Premises used: Iff.mpr, squeeze_zero, tendsto_const_div_atTop_nhds_zero_nat, dist_nonneg, Filter.tendsto_add_atTop_nat, Filter.Tendsto.comp, OfNat.ofNat, tendsto_iff_dist_tendsto_zero
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℕ
⊢ 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
have : (0 : ℝ) < n + 1 := n.cast_add_one_pos
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℕ
this : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
rw : dist ((f ^ (n + 1) : (a : ℝ) → ℝ) 0) ((↑(n + 1) : ℝ) * τ f) ≤ 1
⊢ dist (HDiv.hDiv (α := ℝ) ((f ^ (n + 1) : (a : ℝ) → ℝ) 0 : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) (τ f) ≤
    HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)

Tactic:
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_iff_of_pos_right this, ← Nat.cast_add_one]

Premises used: abs_div, ne_of_gt, div_le_div_iff_of_pos_right, Real.dist_eq, div_sub', abs_of_pos, Nat.cast_add_one
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℕ
this : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ dist ((f ^ (n + 1) : (a : ℝ) → ℝ) 0) ((↑(n + 1) : ℝ) * τ f) ≤ 1

Tactic:
apply dist_pow_map_zero_mul_translationNumber_le

Premises used: CircleDeg1Lift.dist_pow_map_zero_mul_translationNumber_le
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) (β := ℝ) ((f ^ n : (a : ℝ) → ℝ) 0 : ℝ) ((↑n : ℝ) : ℝ)) atTop (𝓝 (τ f))

Tactic:
(tendsto_add_atTop_iff_nat 1).1 (mod_cast f.tendsto_translation_number₀')

Premises used: congrArg, Nat.cast_add._simp_1, cast, nhds, CircleDeg1Lift.translationNumber, HDiv.hDiv, Nat.cast, Filter.atTop, funext, HPow.hPow, HAdd.hAdd, Filter.Tendsto, congr, Iff.mp, Filter.tendsto_add_atTop_iff_nat, congrFun', Nat.cast_zero, OfNat.ofNat, Eq.symm, Nat.cast_one, DFunLike.coe, CircleDeg1Lift.tendsto_translation_number₀', Eq.trans
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
rw :
  Tendsto (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) ((f ^ n : (a : ℝ) → ℝ) x : ℝ) x / (↑n : ℝ)) atTop
    (𝓝
      (τ
        ((↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                    ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x))⁻¹ :
              CircleDeg1Lift) *
            f *
          (↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x)) :
            CircleDeg1Lift))))
⊢ Tendsto (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) ((f ^ n : (a : ℝ) → ℝ) x : ℝ) x / (↑n : ℝ)) atTop (𝓝 (τ f))

Tactic:
rw [← translationNumber_conj_eq' (translate <| Multiplicative.ofAdd x)]

Premises used: CircleDeg1Lift.translate, Multiplicative.ofAdd, CircleDeg1Lift.translationNumber_conj_eq', DFunLike.coe
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) ((f ^ n : (a : ℝ) → ℝ) x : ℝ) x / (↑n : ℝ)) atTop
    (𝓝
      (τ
        ((↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                    ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x))⁻¹ :
              CircleDeg1Lift) *
            f *
          (↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x)) :
            CircleDeg1Lift))))

Tactic:
(tendsto_translation_number₀ _).congr fun n ↦ ?_

Premises used: CircleDeg1Lift.tendsto_translation_number₀, Filter.Tendsto.congr
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
refine :
  ∀ (n : ℕ),
    HDiv.hDiv (α := ℝ) (β := ℝ)
        ((((↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                            ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x))⁻¹ :
                      CircleDeg1Lift) *
                    f *
                  (↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                        ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x)) :
                    CircleDeg1Lift)) ^
                n :
              (a : ℝ) → ℝ)
            0 :
          ℝ)
        ((↑n : ℝ) : ℝ) =
      HSub.hSub (α := ℝ) ((f ^ n : (a : ℝ) → ℝ) x : ℝ) x / (↑n : ℝ)
⊢ Tendsto (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) ((f ^ n : (a : ℝ) → ℝ) x : ℝ) x / (↑n : ℝ)) atTop
    (𝓝
      (τ
        ((↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                    ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x))⁻¹ :
              CircleDeg1Lift) *
            f *
          (↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x)) :
            CircleDeg1Lift))))

Tactic:
refine (tendsto_translation_number₀ _).congr fun n ↦ ?_

Premises used: CircleDeg1Lift.tendsto_translation_number₀, Filter.Tendsto.congr
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
n : ℕ
⊢ HDiv.hDiv (α := ℝ) (β := ℝ)
      ((((↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                          ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x))⁻¹ :
                    CircleDeg1Lift) *
                  f *
                (↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                      ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x)) :
                  CircleDeg1Lift)) ^
              n :
            (a : ℝ) → ℝ)
          0 :
        ℝ)
      ((↑n : ℝ) : ℝ) =
    HSub.hSub (α := ℝ) ((f ^ n : (a : ℝ) → ℝ) x : ℝ) x / (↑n : ℝ)

Tactic:
simp [sub_eq_neg_add, Units.conj_pow']

Premises used: sub_eq_neg_add, Units.conj_pow'
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) ((f ^ (n + 1) : (a : ℝ) → ℝ) x : ℝ) x / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) atTop
    (𝓝 (τ f))

Tactic:
mod_cast (tendsto_add_atTop_iff_nat 1).2 (f.tendsto_translationNumber x)

Premises used: Iff.mpr, congrArg, Nat.cast_add._simp_1, HSub.hSub, cast, nhds, CircleDeg1Lift.translationNumber, HDiv.hDiv, Nat.cast, Filter.atTop, funext, HPow.hPow, HAdd.hAdd, Filter.Tendsto, Filter.tendsto_add_atTop_iff_nat, congrFun', CircleDeg1Lift.tendsto_translationNumber, OfNat.ofNat, Eq.symm, Nat.cast_one, DFunLike.coe, Eq.trans
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
h : f ≤ g
n : ℕ
hab : LE.le (α := ℝ) ((f ^ n : (a : ℝ) → ℝ) 0 : ℝ) ((g ^ n : (a : ℝ) → ℝ) 0 : ℝ)
⊢ HDiv.hDiv (α := ℝ) (β := ℝ) ((f ^ n : (a : ℝ) → ℝ) 0 : ℝ) ((↑n : ℝ) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g ^ n : (a : ℝ) → ℝ) 0 : ℝ) ((↑n : ℝ) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
h : f ≤ g
n : ℕ
⊢ LE.le (α := ℝ) ((f ^ n : (a : ℝ) → ℝ) 0 : ℝ) ((g ^ n : (a : ℝ) → ℝ) 0 : ℝ)

Tactic:
pow_mono h _ _

Premises used: CircleDeg1Lift.pow_mono
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
h : f ≤ g
n : ℕ
⊢ LE.le (α := ℝ) ((f ^ n : (a : ℝ) → ℝ) 0 : ℝ) ((g ^ n : (a : ℝ) → ℝ) 0 : ℝ)

Tactic:
exact pow_mono h _ _

Premises used: CircleDeg1Lift.pow_mono
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
x : ℝ
⊢ Tendsto
    (fun (n : ℕ) ↦
      (⇑(↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                      ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x)) :
                  CircleDeg1Lift) :
              (a : ℝ) → ℝ)^[n + 1]
          0 /
        HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
    atTop (𝓝 x)

Tactic:
simp only [translate_iterate, translate_apply, add_zero, Nat.cast_succ,
      mul_div_cancel_left₀ (M₀ := ℝ) _ (Nat.cast_add_one_ne_zero _), tendsto_const_nhds]

Premises used: Nat.cast_succ, tendsto_const_nhds, CircleDeg1Lift.translate_iterate, mul_div_cancel_left₀, CircleDeg1Lift.translate_apply, Nat.cast_add_one_ne_zero, add_zero
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
z : ℝ
hz : ∀ (x : ℝ), (f : (a : ℝ) → ℝ) x ≤ x + z
⊢ τ f ≤ z

Tactic:
translationNumber_translate z ▸ translationNumber_mono fun x => (hz x).trans_eq (add_comm _ _)

Premises used: LE.le.trans_eq, Eq.rec, add_comm, CircleDeg1Lift.translationNumber_translate, CircleDeg1Lift.translationNumber_mono
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
z : ℝ
hz : ∀ (x : ℝ), x + z ≤ (f : (a : ℝ) → ℝ) x
⊢ z ≤ τ f

Tactic:
translationNumber_translate z ▸ translationNumber_mono fun x => (add_comm _ _).trans_le (hz x)

Premises used: Eq.rec, Eq.trans_le, add_comm, Multiplicative.toAdd, Multiplicative.ofAdd, CircleDeg1Lift.translationNumber_translate, DFunLike.coe, CircleDeg1Lift.translationNumber_mono
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
m : ℤ
h : (f : (a : ℝ) → ℝ) x ≤ x + (↑m : ℝ)
⊢ τ f ≤ (↑m : ℝ)

Tactic:
le_of_tendsto' (f.tendsto_translation_number' x) fun n =>
    (div_le_iff₀' (n.cast_add_one_pos : (0 : ℝ) < _)).mpr <| sub_le_iff_le_add'.2 <|
      (coe_pow f (n + 1)).symm ▸ @Nat.cast_add_one ℝ _ n ▸ f.iterate_le_of_map_le_add_int h (n + 1)

Premises used: Iff.mpr, Nat.cast_add_one_pos, Eq.rec, CircleDeg1Lift.tendsto_translation_number', sub_le_iff_le_add', HAdd.hAdd, CircleDeg1Lift.iterate_le_of_map_le_add_int, CircleDeg1Lift.coe_pow, le_of_tendsto', OfNat.ofNat, Eq.symm, Nat.cast_add_one, div_le_iff₀'
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
m : ℕ
h : (f : (a : ℝ) → ℝ) x ≤ x + (↑m : ℝ)
⊢ τ f ≤ (↑m : ℝ)

Tactic:
@translationNumber_le_of_le_add_int f x m h

Premises used: CircleDeg1Lift.translationNumber_le_of_le_add_int
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
m : ℤ
h : x + (↑m : ℝ) ≤ (f : (a : ℝ) → ℝ) x
n : ℕ
⊢ x + (↑m : ℝ) * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≤ (f ^ (n + 1) : (a : ℝ) → ℝ) x

Tactic:
simp only [coe_pow, mul_comm (m : ℝ), ← Nat.cast_add_one, f.le_iterate_of_add_int_le_map h]

Premises used: Int.cast, CircleDeg1Lift.le_iterate_of_add_int_le_map, mul_comm, CircleDeg1Lift.coe_pow, Nat.cast_add_one
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
m : ℕ
h : x + (↑m : ℝ) ≤ (f : (a : ℝ) → ℝ) x
⊢ (↑m : ℝ) ≤ τ f

Tactic:
@le_translationNumber_of_add_int_le f x m h

Premises used: CircleDeg1Lift.le_translationNumber_of_add_int_le