awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
n : ℕ
⊢ Monotone (β := ℝ → ℝ) fun (f : CircleDeg1Lift) ↦ (⇑f : (a : ℝ) → ℝ)^[n]

Tactic:
fun f _ h =>
  f.monotone.iterate_le_of_le h _

Premises used: Monotone.iterate_le_of_le, Monotone, CircleDeg1Lift.monotone
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
h : f ≤ g
n : ℕ
⊢ LE.le (α := ℝ → ℝ) (⇑f : (a : ℝ) → ℝ)^[n] (⇑g : (a : ℝ) → ℝ)^[n]

Tactic:
iterate_monotone n h

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

Tactic:
simp only [coe_pow, iterate_mono h n x]

Premises used: CircleDeg1Lift.iterate_mono, CircleDeg1Lift.coe_pow
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
n : ℕ
⊢ Monotone (β := CircleDeg1Lift) fun (f : CircleDeg1Lift) ↦ f ^ n

Tactic:
fun _ _ h => pow_mono h n

Premises used: CircleDeg1Lift.pow_mono, Monotone
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
⊢ (f : (a : ℝ) → ℝ) x ≤ HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ((↑⌈x⌉ : ℝ) : ℝ)

Tactic:
calc
    f x ≤ f ⌈x⌉ := f.monotone <| le_ceil _
    _ = f 0 + ⌈x⌉ := f.map_int_of_map_zero _

Premises used: Trans.trans, Int.le_ceil, CircleDeg1Lift.map_int_of_map_zero, CircleDeg1Lift.monotone
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
⊢ (f : (a : ℝ) → ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) ≤
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ((↑(ceil (α := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ)) : ℝ) : ℝ)

Tactic:
f.map_le_of_map_zero (g 0)

Premises used: CircleDeg1Lift.map_le_of_map_zero, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
⊢ floor (α := ℝ) ((f : (a : ℝ) → ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) : ℝ) ≤
    floor (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) + ceil (α := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ)

Tactic:
calc
    ⌊f (g 0)⌋ ≤ ⌊f 0 + ⌈g 0⌉⌋ := floor_mono <| f.map_map_zero_le g
    _ = ⌊f 0⌋ + ⌈g 0⌉ := floor_add_intCast _ _

Premises used: Trans.trans, Int.floor_mono, Int.floor_add_intCast, CircleDeg1Lift.map_map_zero_le
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
⊢ ceil (α := ℝ) ((f : (a : ℝ) → ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) : ℝ) ≤
    ceil (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) + ceil (α := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ)

Tactic:
calc
    ⌈f (g 0)⌉ ≤ ⌈f 0 + ⌈g 0⌉⌉ := ceil_mono <| f.map_map_zero_le g
    _ = ⌈f 0⌉ + ⌈g 0⌉ := ceil_add_intCast _ _

Premises used: Trans.trans, Int.ceil_mono, Int.ceil_add_intCast, CircleDeg1Lift.map_map_zero_le
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
bc : (↑(ceil (α := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ)) : ℝ) < HAdd.hAdd (α := ℝ) (β := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) (1 : ℝ)
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ((↑(ceil (α := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ)) : ℝ) : ℝ) <
    HAdd.hAdd (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (HAdd.hAdd (α := ℝ) (β := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) (1 : ℝ))

Tactic:
gcongr
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
⊢ (↑(ceil (α := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ)) : ℝ) < HAdd.hAdd (α := ℝ) (β := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) (1 : ℝ)

Tactic:
ceil_lt_add_one _

Premises used: Int.ceil_lt_add_one
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
⊢ (↑(ceil (α := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ)) : ℝ) < HAdd.hAdd (α := ℝ) (β := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) (1 : ℝ)

Tactic:
exact ceil_lt_add_one _

Premises used: Int.ceil_lt_add_one
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ((↑⌊x⌋ : ℝ) : ℝ) ≤ (f : (a : ℝ) → ℝ) x

Tactic:
calc
    f 0 + ⌊x⌋ = f ⌊x⌋ := (f.map_int_of_map_zero _).symm
    _ ≤ f x := f.monotone <| floor_le _

Premises used: Trans.trans, CircleDeg1Lift.map_int_of_map_zero, CircleDeg1Lift.monotone, Int.floor_le, Eq.symm
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ((↑(floor (α := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ)) : ℝ) : ℝ) ≤
    (f : (a : ℝ) → ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ)

Tactic:
f.le_map_of_map_zero (g 0)

Premises used: CircleDeg1Lift.le_map_of_map_zero, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
⊢ floor (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) + floor (α := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) ≤
    floor (α := ℝ) ((f : (a : ℝ) → ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) : ℝ)

Tactic:
calc
    ⌊f 0⌋ + ⌊g 0⌋ = ⌊f 0 + ⌊g 0⌋⌋ := (floor_add_intCast _ _).symm
    _ ≤ ⌊f (g 0)⌋ := floor_mono <| f.le_map_map_zero g

Premises used: Trans.trans, Int.floor_mono, CircleDeg1Lift.le_map_map_zero, Int.floor_add_intCast, Eq.symm
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
⊢ ceil (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) + floor (α := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) ≤
    ceil (α := ℝ) ((f * g : (a : ℝ) → ℝ) 0 : ℝ)

Tactic:
calc
    ⌈f 0⌉ + ⌊g 0⌋ = ⌈f 0 + ⌊g 0⌋⌉ := (ceil_add_intCast _ _).symm
    _ ≤ ⌈f (g 0)⌉ := ceil_mono <| f.le_map_map_zero g

Premises used: Trans.trans, CircleDeg1Lift.le_map_map_zero, Int.ceil_mono, Int.ceil_add_intCast, Eq.symm
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
bc : HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) (1 : ℝ) < (↑(floor (α := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ)) : ℝ)
⊢ HAdd.hAdd (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) (1 : ℝ)) <
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ((↑(floor (α := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ)) : ℝ) : ℝ)

Tactic:
gcongr
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
⊢ HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) (1 : ℝ) < (↑(floor (α := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ)) : ℝ)

Tactic:
sub_one_lt_floor _

Premises used: Int.sub_one_lt_floor
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
⊢ HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) (1 : ℝ) < (↑(floor (α := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ)) : ℝ)

Tactic:
exact sub_one_lt_floor _

Premises used: Int.sub_one_lt_floor
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
rw :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) - 1 <
      (f : (a : ℝ) → ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) ∧
    (f : (a : ℝ) → ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) <
      HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) + 1
⊢ dist (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ))
      ((f : (a : ℝ) → ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ)) <
    1

Tactic:
rw [dist_comm, Real.dist_eq, abs_lt, lt_sub_iff_add_lt', sub_lt_iff_lt_add', ← sub_eq_add_neg]

Premises used: lt_sub_iff_add_lt', sub_eq_add_neg, dist_comm, sub_lt_iff_lt_add', Real.dist_eq, abs_lt
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) - 1 <
      (f : (a : ℝ) → ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) ∧
    (f : (a : ℝ) → ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) <
      HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) + 1

Tactic:
⟨f.lt_map_map_zero g, f.map_map_zero_lt g⟩

Premises used: CircleDeg1Lift.map_map_zero_lt, And.intro, CircleDeg1Lift.lt_map_map_zero
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g : CircleDeg1Lift
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) - 1 <
      (f : (a : ℝ) → ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) ∧
    (f : (a : ℝ) → ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) <
      HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) + 1

Tactic:
exact ⟨f.lt_map_map_zero g, f.map_map_zero_lt g⟩
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g₁ g₂ : CircleDeg1Lift
h : Semiconj (α := ℝ) (β := ℝ) (⇑f : (a : ℝ) → ℝ) (⇑g₁ : (a : ℝ) → ℝ) (⇑g₂ : (a : ℝ) → ℝ)
⊢ dist ((g₁ : (a : ℝ) → ℝ) 0)
        (HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) ((g₁ : (a : ℝ) → ℝ) 0 : ℝ) : ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ)) +
      dist (HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) ((g₁ : (a : ℝ) → ℝ) 0 : ℝ) : ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ))
        ((g₂ : (a : ℝ) → ℝ) 0) =
    dist (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ((g₁ : (a : ℝ) → ℝ) 0 : ℝ))
        ((f : (a : ℝ) → ℝ) ((g₁ : (a : ℝ) → ℝ) 0 : ℝ)) +
      dist (HAdd.hAdd (α := ℝ) (β := ℝ) ((g₂ : (a : ℝ) → ℝ) 0 : ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ))
        ((g₂ : (a : ℝ) → ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ))

Tactic:
simp only [h.eq, Real.dist_eq, sub_sub, add_comm (f 0), sub_sub_eq_add_sub,
        abs_sub_comm (g₂ (f 0))]

Premises used: Function.Semiconj.eq, sub_sub_eq_add_sub, add_comm, sub_sub, Real.dist_eq, abs_sub_comm, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f g₁ g₂ : CircleDeg1Lift
h : SemiconjBy f g₁ g₂
⊢ dist (α := ℝ) ((g₁ : (a : ℝ) → ℝ) 0 : ℝ) ((g₂ : (a : ℝ) → ℝ) 0 : ℝ) < 2

Tactic:
dist_map_zero_lt_of_semiconj <| semiconjBy_iff_semiconj.1 h

Premises used: CircleDeg1Lift.dist_map_zero_lt_of_semiconj, Iff.mp, CircleDeg1Lift.semiconjBy_iff_semiconj
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
⊢ Tendsto (α := ℝ) (β := ℝ) (⇑f : (a : ℝ) → ℝ) atBot atBot

Tactic:
tendsto_atBot_mono f.map_le_of_map_zero <| tendsto_atBot_add_const_left _ _ <|
    (tendsto_atBot_mono fun x => (ceil_lt_add_one x).le) <|
      tendsto_atBot_add_const_right _ _ tendsto_id

Premises used: Filter.tendsto_id, CircleDeg1Lift.map_le_of_map_zero, LT.lt.le, Filter.tendsto_atBot_mono, Filter.tendsto_atBot_add_const_left, Int.ceil_lt_add_one, Filter.tendsto_atBot_add_const_right
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x - 1) atTop atTop

Tactic:
simpa [sub_eq_add_neg] using tendsto_atTop_add_const_right _ _ tendsto_id

Premises used: Filter.tendsto_atTop_add_const_right, Filter.tendsto_id, sub_eq_add_neg
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
⊢ Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ) ↔ Surjective (α := ℝ) (β := ℝ) (⇑f : (a : ℝ) → ℝ)

Tactic:
⟨fun h => h.surjective f.tendsto_atTop f.tendsto_atBot, f.monotone.continuous_of_surjective⟩

Premises used: Continuous.surjective, CircleDeg1Lift.tendsto_atBot, Monotone.continuous_of_surjective, CircleDeg1Lift.tendsto_atTop, Iff.intro, CircleDeg1Lift.monotone
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
m : ℤ
h : (f : (a : ℝ) → ℝ) x ≤ x + (↑m : ℝ)
n : ℕ
⊢ (⇑f : (a : ℝ) → ℝ)^[n] x ≤ x + HMul.hMul (α := ℝ) (↑n : ℝ) (↑m : ℝ)

Tactic:
simpa only [nsmul_eq_mul, add_right_iterate] using
    (f.commute_add_int m).iterate_le_of_map_le f.monotone (monotone_id.add_const (m : ℝ)) h n

Premises used: Int.cast, monotone_id, CircleDeg1Lift.commute_add_int, Function.Commute.iterate_le_of_map_le, Monotone.add_const, add_right_iterate, CircleDeg1Lift.monotone, nsmul_eq_mul
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
m : ℤ
h : x + (↑m : ℝ) ≤ (f : (a : ℝ) → ℝ) x
n : ℕ
⊢ x + HMul.hMul (α := ℝ) (↑n : ℝ) (↑m : ℝ) ≤ (⇑f : (a : ℝ) → ℝ)^[n] x

Tactic:
simpa only [nsmul_eq_mul, add_right_iterate] using
    (f.commute_add_int m).symm.iterate_le_of_map_le (monotone_id.add_const (m : ℝ)) f.monotone h n

Premises used: Int.cast, monotone_id, CircleDeg1Lift.commute_add_int, Function.Commute.iterate_le_of_map_le, Monotone.add_const, add_right_iterate, CircleDeg1Lift.monotone, nsmul_eq_mul, Function.Commute.symm
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
m : ℤ
h : (f : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
n : ℕ
⊢ (⇑f : (a : ℝ) → ℝ)^[n] x = x + HMul.hMul (α := ℝ) (↑n : ℝ) (↑m : ℝ)

Tactic:
simpa only [nsmul_eq_mul, add_right_iterate] using (f.commute_add_int m).iterate_eq_of_map_eq n h

Premises used: CircleDeg1Lift.commute_add_int, add_right_iterate, nsmul_eq_mul, Function.Commute.iterate_eq_of_map_eq
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (⇑f : (a : ℝ) → ℝ)^[n] x ≤ x + HMul.hMul (α := ℝ) (↑n : ℝ) (↑m : ℝ) ↔ (f : (a : ℝ) → ℝ) x ≤ x + (↑m : ℝ)

Tactic:
simpa only [nsmul_eq_mul, add_right_iterate] using
    (f.commute_add_int m).iterate_pos_le_iff_map_le f.monotone (strictMono_id.add_const (m : ℝ)) hn

Premises used: Int.cast, CircleDeg1Lift.commute_add_int, strictMono_id, add_right_iterate, CircleDeg1Lift.monotone, Function.Commute.iterate_pos_le_iff_map_le, StrictMono.add_const, nsmul_eq_mul
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (⇑f : (a : ℝ) → ℝ)^[n] x < x + HMul.hMul (α := ℝ) (↑n : ℝ) (↑m : ℝ) ↔ (f : (a : ℝ) → ℝ) x < x + (↑m : ℝ)

Tactic:
simpa only [nsmul_eq_mul, add_right_iterate] using
    (f.commute_add_int m).iterate_pos_lt_iff_map_lt f.monotone (strictMono_id.add_const (m : ℝ)) hn

Premises used: Int.cast, Function.Commute.iterate_pos_lt_iff_map_lt, CircleDeg1Lift.commute_add_int, strictMono_id, add_right_iterate, CircleDeg1Lift.monotone, StrictMono.add_const, nsmul_eq_mul
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ (⇑f : (a : ℝ) → ℝ)^[n] x = x + HMul.hMul (α := ℝ) (↑n : ℝ) (↑m : ℝ) ↔ (f : (a : ℝ) → ℝ) x = x + (↑m : ℝ)

Tactic:
simpa only [nsmul_eq_mul, add_right_iterate] using
    (f.commute_add_int m).iterate_pos_eq_iff_map_eq f.monotone (strictMono_id.add_const (m : ℝ)) hn

Premises used: Int.cast, CircleDeg1Lift.commute_add_int, strictMono_id, add_right_iterate, CircleDeg1Lift.monotone, StrictMono.add_const, nsmul_eq_mul, Function.Commute.iterate_pos_eq_iff_map_eq
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ x + HMul.hMul (α := ℝ) (↑n : ℝ) (↑m : ℝ) ≤ (⇑f : (a : ℝ) → ℝ)^[n] x ↔ x + (↑m : ℝ) ≤ (f : (a : ℝ) → ℝ) x

Tactic:
simpa only [not_lt] using not_congr (f.iterate_pos_lt_iff hn)

Premises used: CircleDeg1Lift.iterate_pos_lt_iff, not_lt, not_congr
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℝ
m : ℤ
n : ℕ
hn : 0 < n
⊢ x + HMul.hMul (α := ℝ) (↑n : ℝ) (↑m : ℝ) < (⇑f : (a : ℝ) → ℝ)^[n] x ↔ x + (↑m : ℝ) < (f : (a : ℝ) → ℝ) x

Tactic:
simpa only [not_le] using not_congr (f.iterate_pos_le_iff hn)

Premises used: not_le, CircleDeg1Lift.iterate_pos_le_iff, not_congr
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℕ
rw : 0 + HMul.hMul (α := ℝ) (↑n : ℝ) (↑(floor (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ)) : ℝ) ≤ (⇑f : (a : ℝ) → ℝ)^[n] 0
⊢ (↑n : ℤ) * floor (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ≤ floor (α := ℝ) ((⇑f : (a : ℝ) → ℝ)^[n] 0)

Tactic:
rw [le_floor, Int.cast_mul, Int.cast_natCast, ← zero_add ((n : ℝ) * _)]

Premises used: Int.cast_natCast, HMul.hMul, zero_add, Nat.cast, Int.cast_mul, Int.le_floor
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℕ
h : HAdd.hAdd (α := ℝ) 0 (↑(floor (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ)) : ℝ) ≤ (f : (a : ℝ) → ℝ) 0
⊢ 0 + HMul.hMul (α := ℝ) (↑n : ℝ) (↑(floor (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ)) : ℝ) ≤ (⇑f : (a : ℝ) → ℝ)^[n] 0

Tactic:
apply le_iterate_of_add_int_le_map

Premises used: CircleDeg1Lift.le_iterate_of_add_int_le_map
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℕ
⊢ HAdd.hAdd (α := ℝ) 0 (↑(floor (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ)) : ℝ) ≤ (f : (a : ℝ) → ℝ) 0

Tactic:
simp [floor_le]

Premises used: Int.floor_le
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
⊢ f.transnumAuxSeq = fun (n : ℕ) ↦
    HDiv.hDiv (α := ℝ) ((f ^ HPow.hPow (α := ℕ) 2 n : (a : ℝ) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) 2 n)

Tactic:
rfl

Premises used: rfl, CircleDeg1Lift.transnumAuxSeq
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
τ' : ℝ
h : Tendsto f.transnumAuxSeq atTop (𝓝 τ')
⊢ τ f = τ'

Tactic:
h.limUnder_eq

Premises used: CircleDeg1Lift.translationNumber, Filter.Tendsto.limUnder_eq
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
τ' : ℝ
h : Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) ((⇑f : (a : ℝ) → ℝ)^[n] 0) (↑n : ℝ)) atTop (𝓝 τ')
⊢ Tendsto f.transnumAuxSeq atTop (𝓝 τ')

Tactic:
simpa [Function.comp_def, transnumAuxSeq_def, coe_pow] using
      h.comp (tendsto_pow_atTop_atTop_of_one_lt one_lt_two)

Premises used: CircleDeg1Lift.transnumAuxSeq_def, tendsto_pow_atTop_atTop_of_one_lt, Function.comp_def, one_lt_two, CircleDeg1Lift.coe_pow, Filter.Tendsto.comp
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
τ' : ℝ
h : Tendsto (fun (n : ℕ) ↦ (⇑f : (a : ℝ) → ℝ)^[n + 1] 0 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) atTop (𝓝 τ')
⊢ τ f = τ'

Tactic:
f.translationNumber_eq_of_tendsto₀ <| (tendsto_add_atTop_iff_nat 1).1 (mod_cast h)

Premises used: congrArg, Nat.cast_add._simp_1, cast, nhds, HDiv.hDiv, Nat.iterate, Nat.cast, Filter.atTop, funext, CircleDeg1Lift.translationNumber_eq_of_tendsto₀, 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, Eq.trans
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
⊢ f.transnumAuxSeq 0 = (f : (a : ℝ) → ℝ) 0

Tactic:
simp [transnumAuxSeq]

Premises used: CircleDeg1Lift.transnumAuxSeq
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℕ
⊢ 0 < HPow.hPow (α := ℝ) 2 (n + 1)

Tactic:
have : 0 < (2 ^ (n + 1) : ℝ) := pow_pos zero_lt_two _
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℕ
this : 0 < HPow.hPow (α := ℝ) 2 (n + 1)
rw : dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / |HPow.hPow (α := ℝ) 2 (n + 1)|
⊢ dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / 2 / HPow.hPow (α := ℝ) 2 n

Tactic:
rw [div_div, ← pow_succ', ← abs_of_pos this]

Premises used: abs_of_pos, div_div, pow_succ'
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
n : ℕ
this : 0 < HPow.hPow (α := ℝ) 2 (n + 1)
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
⊢ 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:
gcongr
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
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 : ℝ)) <
    1

Tactic:
(f ^ 2 ^ n).dist_map_map_zero_lt (f ^ 2 ^ n)

Premises used: CircleDeg1Lift.dist_map_map_zero_lt, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
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 : ℝ)) <
    1

Tactic:
exact (f ^ 2 ^ n).dist_map_map_zero_lt (f ^ 2 ^ n)

Premises used: CircleDeg1Lift.dist_map_map_zero_lt, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
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
        (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)|
⊢ dist (f.transnumAuxSeq n) (f.transnumAuxSeq (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)

Premises used: HPow.hPow, HAdd.hAdd, Dist.dist, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
⊢ Tendsto f.transnumAuxSeq atTop (𝓝 (τ f))

Tactic:
(cauchySeq_of_le_geometric_two fun n => le_of_lt <| f.transnumAuxSeq_dist_lt n).tendsto_limUnder

Premises used: le_of_lt, CircleDeg1Lift.transnumAuxSeq_dist_lt, CircleDeg1Lift.translationNumber, CauchySeq.tendsto_limUnder, cauchySeq_of_le_geometric_two
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
⊢ dist ((f : (a : ℝ) → ℝ) 0) (τ f) ≤ 1

Tactic:
f.transnumAuxSeq_zero ▸
    dist_le_of_le_geometric_two_of_tendsto₀ (fun n => le_of_lt <| f.transnumAuxSeq_dist_lt n)
      f.tendsto_translationNumber_aux

Premises used: CircleDeg1Lift.tendsto_translationNumber_aux, le_of_lt, CircleDeg1Lift.transnumAuxSeq_dist_lt, Eq.rec, CircleDeg1Lift.transnumAuxSeq_zero, dist_le_of_le_geometric_two_of_tendsto₀
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
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
apply₂ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / HPow.hPow (α := ℝ) 2 n) atTop (𝓝 0)
⊢ Tendsto (fun (n : ℕ) ↦ x (HPow.hPow (α := ℕ) 2 n) / HPow.hPow (α := ℝ) 2 n) atTop (𝓝 (τ f))

Tactic:
apply f.tendsto_translationNumber_aux.congr_dist (squeeze_zero (fun _ => dist_nonneg) _ _)

Premises used: squeeze_zero, CircleDeg1Lift.tendsto_translationNumber_aux, dist_nonneg, Filter.Tendsto.congr_dist
-- Module: Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
Goal:
f : CircleDeg1Lift
x : ℕ → ℝ
C : ℝ
H : ∀ (n : ℕ), dist ((f ^ n : (a : ℝ) → ℝ) 0) (x n) ≤ C
⊢ ℕ → ℝ

Tactic:
exact fun n => C / 2 ^ n

Premises used: HDiv.hDiv, 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 : ℕ
⊢ 0 < HPow.hPow (α := ℝ) 2 n

Tactic:
have : 0 < (2 ^ n : ℝ) := pow_pos zero_lt_two _