awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
n : ℕ
this : 0 < HPow.hPow (α := ℝ) 2 (n + 1)
⊢ |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
        HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 (n + 1) : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 (n + 1))| =
    |HSub.hSub (β := ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
            ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ))
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) : ℝ)| /
      |HPow.hPow (α := ℝ) 2 (n + 1)|
have rw : |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
      HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 (n + 1) : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 (n + 1))| =
  |HSub.hSub (β := ℝ)
        (HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ))
        ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) : ℝ) /
      HPow.hPow (α := ℝ) 2 (n + 1)|
Tactic: rw [← abs_div, sub_div, pow_succ, pow_succ', ← two_mul, mul_div_mul_left _ _ (two_ne_zero' ℝ),
        pow_mul, sq, mul_apply]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
n : ℕ
this : 0 < HPow.hPow (α := ℝ) 2 (n + 1)
rw :
  |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
        HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 (n + 1) : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 (n + 1))| =
    |HSub.hSub (β := ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
            ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ))
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) : ℝ) /
        HPow.hPow (α := ℝ) 2 (n + 1)|
⊢ |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
        HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 (n + 1) : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 (n + 1))| =
    |HSub.hSub (β := ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
            ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ))
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) : ℝ)| /
      |HPow.hPow (α := ℝ) 2 (n + 1)|
have rw₁ : |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
      HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 (n + 1) : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 (n + 1))| =
  |HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) /
        HPow.hPow (α := ℝ) 2 (n + 1) -
      HDiv.hDiv (α := ℝ)
        ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) : ℝ)
        (HPow.hPow (α := ℝ) 2 (n + 1))|
Tactic: rw [← abs_div, sub_div, pow_succ, pow_succ', ← two_mul, mul_div_mul_left _ _ (two_ne_zero' ℝ),
        pow_mul, sq, mul_apply]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
n : ℕ
this : 0 < HPow.hPow (α := ℝ) 2 (n + 1)
rw :
  |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
        HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 (n + 1) : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 (n + 1))| =
    |HSub.hSub (β := ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
            ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ))
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) : ℝ) /
        HPow.hPow (α := ℝ) 2 (n + 1)|
rw₁ :
  |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
        HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 (n + 1) : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 (n + 1))| =
    |HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
            ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) /
          HPow.hPow (α := ℝ) 2 (n + 1) -
        HDiv.hDiv (α := ℝ)
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) : ℝ)
          (HPow.hPow (α := ℝ) 2 (n + 1))|
⊢ |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
        HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 (n + 1) : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 (n + 1))| =
    |HSub.hSub (β := ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
            ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ))
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) : ℝ)| /
      |HPow.hPow (α := ℝ) 2 (n + 1)|
have rw₂ : |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
      HDiv.hDiv (α := ℝ) ((f ^ (HPow.hPow (α := ℕ) 2 n * 2) : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 (n + 1))| =
  |HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) /
        HPow.hPow (α := ℝ) 2 (n + 1) -
      HDiv.hDiv (α := ℝ)
        ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) : ℝ)
        (HPow.hPow (α := ℝ) 2 (n + 1))|
Tactic: rw [← abs_div, sub_div, pow_succ, pow_succ', ← two_mul, mul_div_mul_left _ _ (two_ne_zero' ℝ),
        pow_mul, sq, mul_apply]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
n : ℕ
this : 0 < HPow.hPow (α := ℝ) 2 (n + 1)
rw :
  |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
        HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 (n + 1) : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 (n + 1))| =
    |HSub.hSub (β := ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
            ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ))
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) : ℝ) /
        HPow.hPow (α := ℝ) 2 (n + 1)|
rw₁ :
  |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
        HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 (n + 1) : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 (n + 1))| =
    |HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
            ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) /
          HPow.hPow (α := ℝ) 2 (n + 1) -
        HDiv.hDiv (α := ℝ)
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) : ℝ)
          (HPow.hPow (α := ℝ) 2 (n + 1))|
rw₂ :
  |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
        HDiv.hDiv (α := ℝ) ((f ^ (HPow.hPow (α := ℕ) 2 n * 2) : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 (n + 1))| =
    |HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
            ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) /
          HPow.hPow (α := ℝ) 2 (n + 1) -
        HDiv.hDiv (α := ℝ)
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) : ℝ)
          (HPow.hPow (α := ℝ) 2 (n + 1))|
⊢ |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
        HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 (n + 1) : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 (n + 1))| =
    |HSub.hSub (β := ℝ)
          (HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
            ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ))
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) : ℝ)| /
      |HPow.hPow (α := ℝ) 2 (n + 1)|
have rw₃ : |HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n) -
      HDiv.hDiv (α := ℝ) ((f ^ (HPow.hPow (α := ℕ) 2 n * 2) : (a : ℝ) → ℝ) 0 : ℝ) (2 * HPow.hPow (α := ℝ) 2 n)| =
  |HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) /
        (2 * HPow.hPow (α := ℝ) 2 n) -
      HDiv.hDiv (α := ℝ)
        ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) : ℝ)
        (2 * HPow.hPow (α := ℝ) 2 n)|
Tactic: rw [← abs_div, sub_div, pow_succ, pow_succ', ← two_mul, mul_div_mul_left _ _ (two_ne_zero' ℝ),
        pow_mul, sq, mul_apply]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
n : ℕ
this : 0 < HPow.hPow (α := ℝ) 2 (n + 1)
⊢ dist
        (HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ))
        ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)) /
      |HPow.hPow (α := ℝ) 2 (n + 1)| <
    1 / |HPow.hPow (α := ℝ) 2 (n + 1)|
have h : dist
    (HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
      ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ))
    ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)) <
  1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
n : ℕ
this : 0 < HPow.hPow (α := ℝ) 2 (n + 1)
⊢ dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / |HPow.hPow (α := ℝ) 2 (n + 1)|
have _ : dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) =
  dist
      (HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
        ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ))
      ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)) /
    |HPow.hPow (α := ℝ) 2 (n + 1)|
Tactic: calc
    _ = dist ((f ^ 2 ^ n) 0 + (f ^ 2 ^ n) 0) ((f ^ 2 ^ n) ((f ^ 2 ^ n) 0)) / |2 ^ (n + 1)| := by
      simp_rw [transnumAuxSeq, Real.dist_eq]
      rw [← abs_div, sub_div, pow_succ, pow_succ', ← two_mul, mul_div_mul_left _ _ (two_ne_zero' ℝ),
        pow_mul, sq, mul_apply]
    _ < _ := by gcongr; exact (f ^ 2 ^ n).dist_map_map_zero_lt (f ^ 2 ^ n)
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
n : ℕ
this : 0 < HPow.hPow (α := ℝ) 2 (n + 1)
_ :
  dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) =
    dist
        (HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
          ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ))
        ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)) /
      |HPow.hPow (α := ℝ) 2 (n + 1)|
⊢ dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / |HPow.hPow (α := ℝ) 2 (n + 1)|
have _₁ : dist
      (HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)
        ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ))
      ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ)) /
    |HPow.hPow (α := ℝ) 2 (n + 1)| <
  1 / |HPow.hPow (α := ℝ) 2 (n + 1)|
Tactic: calc
    _ = dist ((f ^ 2 ^ n) 0 + (f ^ 2 ^ n) 0) ((f ^ 2 ^ n) ((f ^ 2 ^ n) 0)) / |2 ^ (n + 1)| := by
      simp_rw [transnumAuxSeq, Real.dist_eq]
      rw [← abs_div, sub_div, pow_succ, pow_succ', ← two_mul, mul_div_mul_left _ _ (two_ne_zero' ℝ),
        pow_mul, sq, mul_apply]
    _ < _ := by gcongr; exact (f ^ 2 ^ n).dist_map_map_zero_lt (f ^ 2 ^ n)
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n : (a : ℝ) → ℝ) 0) (x n) ≤ C
apply : ℕ → ℝ
⊢ Tendsto (fun (n : ℕ) ↦ x (HPow.hPow (α := ℕ) 2 n) / HPow.hPow (α := ℝ) 2 n) atTop (𝓝 (τ f))
have apply₁ : ∀ (t : ℕ), dist (f.transnumAuxSeq t) (x (HPow.hPow (α := ℕ) 2 t) / HPow.hPow (α := ℝ) 2 t) ≤ C / HPow.hPow (α := ℝ) 2 t
Tactic: apply f.tendsto_translationNumber_aux.congr_dist (squeeze_zero (fun _ => dist_nonneg) _ _)
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n : (a : ℝ) → ℝ) 0) (x n) ≤ C
apply : ℕ → ℝ
apply₁ :
  ∀ (t : ℕ),
    dist (f.transnumAuxSeq t) (x (HPow.hPow (α := ℕ) 2 t) / HPow.hPow (α := ℝ) 2 t) ≤ C / HPow.hPow (α := ℝ) 2 t
⊢ Tendsto (fun (n : ℕ) ↦ x (HPow.hPow (α := ℕ) 2 n) / HPow.hPow (α := ℝ) 2 n) atTop (𝓝 (τ f))
have apply₂ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (α := ℝ) 2 n) atTop (𝓝 0)
Tactic: apply f.tendsto_translationNumber_aux.congr_dist (squeeze_zero (fun _ => dist_nonneg) _ _)
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (hypothesis)
Goal:
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n : (a : ℝ) → ℝ) 0) (x n) ≤ C
n : ℕ
⊢ dist (f.transnumAuxSeq n) (x (HPow.hPow (α := ℕ) 2 n) / HPow.hPow (α := ℝ) 2 n) ≤ C / HPow.hPow (α := ℝ) 2 n
have this : 0 < HPow.hPow (α := ℝ) 2 n
Tactic: have : 0 < (2 ^ n : ℝ) := pow_pos zero_lt_two _
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n : (a : ℝ) → ℝ) 0) (x n) ≤ C
n : ℕ
this : 0 < HPow.hPow (α := ℝ) 2 n
⊢ dist (f.transnumAuxSeq n) (x (HPow.hPow (α := ℕ) 2 n) / HPow.hPow (α := ℝ) 2 n) ≤ C / HPow.hPow (α := ℝ) 2 n
have 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
Tactic: convert! (div_le_div_iff_of_pos_right this).2 (H (2 ^ n)) using 1
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n : (a : ℝ) → ℝ) 0) (x n) ≤ C
n : ℕ
this : 0 < 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
have 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
Tactic: rw [transnumAuxSeq, Real.dist_eq, ← sub_div, abs_div, abs_of_pos this, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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
⊢ 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
have 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
Tactic: rw [transnumAuxSeq, Real.dist_eq, ← sub_div, abs_div, abs_of_pos this, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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
⊢ 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
have 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
Tactic: rw [transnumAuxSeq, Real.dist_eq, ← sub_div, abs_div, abs_of_pos this, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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
⊢ 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
have 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
Tactic: rw [transnumAuxSeq, Real.dist_eq, ← sub_div, abs_div, abs_of_pos this, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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
⊢ 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
have 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
Tactic: rw [transnumAuxSeq, Real.dist_eq, ← sub_div, abs_div, abs_of_pos this, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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
⊢ 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
have 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
Tactic: rw [transnumAuxSeq, Real.dist_eq, ← sub_div, abs_div, abs_of_pos this, Real.dist_eq]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f g : CircleDeg1Lift
h : Commute f g
⊢ τ (f * g) = τ f + τ g
have refine : Tendsto (fun (x : ℕ) ↦ f.transnumAuxSeq x + g.transnumAuxSeq x) atTop (𝓝 (τ (f * g)))
Tactic: refine tendsto_nhds_unique ?_
    (f.tendsto_translationNumber_aux.add g.tendsto_translationNumber_aux)
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f g : CircleDeg1Lift
h : Commute f g
⊢ Tendsto (fun (x : ℕ) ↦ f.transnumAuxSeq x + g.transnumAuxSeq x) atTop (𝓝 (τ (f * g)))
have 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)))
Tactic: simp only [transnumAuxSeq, ← add_div]