awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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)))
have refine : ∀ (n : ℕ),
  dist (α := ℝ) (((f * g) ^ n : (a : ℝ) → ℝ) 0 : ℝ)
      ((fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ n : (a : ℝ) → ℝ) 0 : ℝ) ((g ^ n : (a : ℝ) → ℝ) 0 : ℝ)) n : ℝ) ≤
    1
Tactic: refine (f * g).tendsto_translationNumber_of_dist_bounded_aux
    (fun n ↦ (f ^ n) 0 + (g ^ n) 0) 1 fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f g : CircleDeg1Lift
h : Commute f g
n : ℕ
⊢ dist (α := ℝ) (((f * g) ^ n : (a : ℝ) → ℝ) 0 : ℝ)
      ((fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ n : (a : ℝ) → ℝ) 0 : ℝ) ((g ^ n : (a : ℝ) → ℝ) 0 : ℝ)) n : ℝ) ≤
    1
have rw : dist (α := ℝ)
    ((fun (n : ℕ) ↦ HAdd.hAdd (α := ℝ) (β := ℝ) ((f ^ n : (a : ℝ) → ℝ) 0 : ℝ) ((g ^ n : (a : ℝ) → ℝ) 0 : ℝ)) n : ℝ)
    ((f ^ n * g ^ n : (a : ℝ) → ℝ) 0 : ℝ) ≤
  1
Tactic: rw [h.mul_pow, dist_comm]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
n : ℕ
⊢ τ (f ^ (n + 1)) = (↑(n + 1) : ℝ) * τ f
have rw : τ (f ^ n * f) = (↑(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]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
n : ℕ
rw : τ (f ^ n * f) = (↑(n + 1) : ℝ) * τ f
⊢ τ (f ^ (n + 1)) = (↑(n + 1) : ℝ) * τ f
have rw₁ : τ (f ^ n) + τ f = (↑(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]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
n : ℕ
rw : τ (f ^ n * f) = (↑(n + 1) : ℝ) * τ f
rw₁ : τ (f ^ n) + τ f = (↑(n + 1) : ℝ) * τ f
⊢ τ (f ^ (n + 1)) = (↑(n + 1) : ℝ) * τ f
have rw₂ : (↑n : ℝ) * τ f + τ f = (↑(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]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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
⊢ τ (f ^ (n + 1)) = (↑(n + 1) : ℝ) * τ f
have rw₃ : (↑n : ℝ) * τ f + τ f = HAdd.hAdd (α := ℝ) (↑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]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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
⊢ τ (f ^ (n + 1)) = (↑(n + 1) : ℝ) * τ f
have rw₄ : (↑n : ℝ) * τ f + τ f = (↑n : ℝ) * τ f + 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]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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
⊢ τ (f ^ (n + 1)) = (↑(n + 1) : ℝ) * τ f
have rw₅ : (↑n : ℝ) * τ f + τ f = (↑n : ℝ) * τ f + τ 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]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Liftˣ
n : ℕ
⊢ τ (↑(f ^ -[n+1]) : CircleDeg1Lift) = (↑-[n+1] : ℝ) * τ (↑f : CircleDeg1Lift)
have simp : -(HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * τ (↑f : CircleDeg1Lift)) =
  HAdd.hAdd (α := ℝ) (-1) (-(↑n : ℝ)) * τ (↑f : CircleDeg1Lift)
Tactic: simp
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
⊢ Tendsto (fun (n : ℕ) ↦ HDiv.hDiv (α := ℝ) ((f ^ (n + 1) : (a : ℝ) → ℝ) 0 : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) atTop
    (𝓝 (τ f))
have 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
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))
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (hypothesis)
Goal:
f : CircleDeg1Lift
n : ℕ
⊢ dist (HDiv.hDiv (α := ℝ) ((f ^ (n + 1) : (a : ℝ) → ℝ) 0 : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) (τ f) ≤
    HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)
have this : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: have : (0 : ℝ) < n + 1 := n.cast_add_one_pos
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
n : ℕ
this : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ dist (HDiv.hDiv (α := ℝ) ((f ^ (n + 1) : (a : ℝ) → ℝ) 0 : ℝ) (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) (τ f) ≤
    HDiv.hDiv (α := ℝ) 1 (↑(n + 1) : ℝ)
have rw : dist ((f ^ (n + 1) : (a : ℝ) → ℝ) 0) ((↑(n + 1) : ℝ) * τ f) ≤ 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]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
x : ℝ
⊢ Tendsto (fun (n : ℕ) ↦ HSub.hSub (α := ℝ) ((f ^ n : (a : ℝ) → ℝ) x : ℝ) x / (↑n : ℝ)) atTop (𝓝 (τ f))
have 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))))
Tactic: rw [← translationNumber_conj_eq' (translate <| Multiplicative.ofAdd x)]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
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))))
have 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 : ℝ)
Tactic: refine (tendsto_translation_number₀ _).congr fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f g : CircleDeg1Lift
h : f ≤ g
n : ℕ
⊢ HDiv.hDiv (α := ℝ) (β := ℝ) ((f ^ n : (a : ℝ) → ℝ) 0 : ℝ) ((↑n : ℝ) : ℝ) ≤
    HDiv.hDiv (α := ℝ) (β := ℝ) ((g ^ n : (a : ℝ) → ℝ) 0 : ℝ) ((↑n : ℝ) : ℝ)
have hab : LE.le (α := ℝ) ((f ^ n : (a : ℝ) → ℝ) 0 : ℝ) ((g ^ n : (a : ℝ) → ℝ) 0 : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
x : ℝ
⊢ (f : (a : ℝ) → ℝ) x < x + (↑⌊τ f⌋ : ℝ) + 1
have rw : (f : (a : ℝ) → ℝ) x < x + HAdd.hAdd (α := ℝ) (↑⌊τ f⌋ : ℝ) 1
Tactic: rw [add_assoc]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
x : ℝ
⊢ (f : (a : ℝ) → ℝ) x < x + HAdd.hAdd (α := ℝ) (↑⌊τ f⌋ : ℝ) 1
have norm_cast : (f : (a : ℝ) → ℝ) x < x + (↑(⌊τ f⌋ + 1) : ℝ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
x : ℝ
⊢ (f : (a : ℝ) → ℝ) x < x + (↑(⌊τ f⌋ + 1) : ℝ)
have refine : τ f < (↑(⌊τ f⌋ + 1) : ℝ)
Tactic: refine map_lt_of_translationNumber_lt_int _ ?_ _
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
x : ℝ
⊢ τ f < (↑(⌊τ f⌋ + 1) : ℝ)
have push_cast : τ f < HAdd.hAdd (α := ℝ) (↑⌊τ f⌋ : ℝ) 1
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
x : ℝ
⊢ x + (↑⌊τ f⌋ : ℝ) + 1 ≤ x + τ f + 1
have bc : (↑⌊τ f⌋ : ℝ) ≤ τ f
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (hypothesis)
Goal:
f : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : (f ^ n : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
hn : 0 < n
⊢ τ f = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
have this : τ (f ^ n) = (↑m : ℝ)
Tactic: have := (f ^ n).translationNumber_of_eq_add_int h
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
x : ℝ
n : ℕ
m : ℤ
h : (f ^ n : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
hn : 0 < n
this : τ (f ^ n) = (↑m : ℝ)
⊢ τ f = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ)
have rwa : ∀ (this : τ f * (↑n : ℝ) = (↑m : ℝ)), Ne (α := ℝ) (↑n : ℝ) 0
Tactic: rwa [translationNumber_pow, mul_comm, ← eq_div_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), (f : (a : ℝ) → ℝ) x < x + z
⊢ τ f < z
have obtain : ∀ (x : ℝ)
  (hx :
    ∀ (y : ℝ),
      Membership.mem (γ := Set ℝ) (Icc 0 1) y →
        HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x),
  τ f < z
Tactic: obtain ⟨x, -, hx⟩ : ∃ x ∈ Icc (0 : ℝ) 1, ∀ y ∈ Icc (0 : ℝ) 1, f y - y ≤ f x - x :=
    isCompact_Icc.exists_isMaxOn (nonempty_Icc.2 zero_le_one)
      (hf.sub continuous_id).continuousOn
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), (f : (a : ℝ) → ℝ) x < x + z
x : ℝ
hx :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) y →
      HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
⊢ τ f < z
have refine : τ f ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
Tactic: refine lt_of_le_of_lt ?_ (sub_lt_iff_lt_add'.2 <| hz x)
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), (f : (a : ℝ) → ℝ) x < x + z
x : ℝ
hx :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) y →
      HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
⊢ τ f ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
have hz₁ : ∀ (x_1 : ℝ), (f : (a : ℝ) → ℝ) x_1 ≤ x_1 + HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
Tactic: apply translationNumber_le_of_le_add
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), (f : (a : ℝ) → ℝ) x < x + z
x : ℝ
hx :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) y →
      HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
⊢ ∀ (x_1 : ℝ), (f : (a : ℝ) → ℝ) x_1 ≤ x_1 + HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
have hz₁ : ∀ (x_1 : ℝ), HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x_1 : ℝ) x_1 ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
Tactic: simp only [← sub_le_iff_le_add']
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), x + z < (f : (a : ℝ) → ℝ) x
⊢ z < τ f
have obtain : ∀ (x : ℝ)
  (hx :
    ∀ (y : ℝ),
      Membership.mem (γ := Set ℝ) (Icc 0 1) y →
        HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y),
  z < τ f
Tactic: obtain ⟨x, -, hx⟩ : ∃ x ∈ Icc (0 : ℝ) 1, ∀ y ∈ Icc (0 : ℝ) 1, f x - x ≤ f y - y :=
    isCompact_Icc.exists_isMinOn (nonempty_Icc.2 zero_le_one) (hf.sub continuous_id).continuousOn
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), x + z < (f : (a : ℝ) → ℝ) x
x : ℝ
hx :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) y →
      HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y
⊢ z < τ f
have refine : HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ τ f
Tactic: refine lt_of_lt_of_le (lt_sub_iff_add_lt'.2 <| hz x) ?_
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), x + z < (f : (a : ℝ) → ℝ) x
x : ℝ
hx :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) y →
      HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y
⊢ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ τ f
have hz₁ : ∀ (x_1 : ℝ), x_1 + HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ (f : (a : ℝ) → ℝ) x_1
Tactic: apply le_translationNumber_of_add_le
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
z : ℝ
hz : ∀ (x : ℝ), x + z < (f : (a : ℝ) → ℝ) x
x : ℝ
hx :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) (Icc 0 1) y →
      HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) y : ℝ) y
⊢ ∀ (x_1 : ℝ), x_1 + HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ (f : (a : ℝ) → ℝ) x_1
have hz₁ : ∀ (x_1 : ℝ), HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x ≤ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x_1 : ℝ) x_1
Tactic: simp only [← le_sub_iff_add_le']
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
⊢ ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x ≤ x + τ f
have by_contra! : ∀ (H : ∀ (x : ℝ), x + τ f < (f : (a : ℝ) → ℝ) x), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
⊢ ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + τ f
have obtain : ∀ (a : ℝ) (ha : (f : (a : ℝ) → ℝ) a ≤ a + τ f), ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + τ f
Tactic: obtain ⟨a, ha⟩ : ∃ x, f x ≤ x + τ f := by
    by_contra! H
    exact lt_irrefl _ (f.lt_translationNumber_of_forall_add_lt hf H)
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
a : ℝ
ha : (f : (a : ℝ) → ℝ) a ≤ a + τ f
⊢ ∃ (x : ℝ), x + τ f ≤ (f : (a : ℝ) → ℝ) x
have by_contra! : ∀ (H : ∀ (x : ℝ), (f : (a : ℝ) → ℝ) x < x + τ f), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
a : ℝ
ha : (f : (a : ℝ) → ℝ) a ≤ a + τ f
⊢ ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + τ f
have obtain : ∀ (b : ℝ) (hb : b + τ f ≤ (f : (a : ℝ) → ℝ) b), ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + τ f
Tactic: obtain ⟨b, hb⟩ : ∃ x, x + τ f ≤ f x := by
    by_contra! H
    exact lt_irrefl _ (f.translationNumber_lt_of_forall_lt_add hf H)
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
m : ℤ
⊢ τ f = (↑m : ℝ) ↔ ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
have mp : τ f = (↑m : ℝ) → ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
m : ℤ
mp : τ f = (↑m : ℝ) → ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
⊢ τ f = (↑m : ℝ) ↔ ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
have mpr : (∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + (↑m : ℝ)) → τ f = (↑m : ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
m : ℤ
h : τ f = (↑m : ℝ)
⊢ ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
have mp : ∃ (x : ℝ), (f : (a : ℝ) → ℝ) x = x + τ f
Tactic: simp only [← h]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
n : ℕ
⊢ Continuous (X := ℝ) (Y := ℝ) (⇑(f ^ n) : (a : ℝ) → ℝ)
have rw : Continuous (X := ℝ) (⇑f : (a : ℝ) → ℝ)^[n]
Tactic: rw [coe_pow]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ f = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ↔ ∃ (x : ℝ), (f ^ n : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
have rw : τ (f ^ n) = (↑m : ℝ) ↔ ∃ (x : ℝ), (f ^ n : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
Tactic: rw [eq_div_iff, mul_comm, ← translationNumber_pow]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
m : ℤ
n : ℕ
hn : 0 < n
rw : τ (f ^ n) = (↑m : ℝ) ↔ ∃ (x : ℝ), (f ^ n : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
⊢ τ f = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ↔ ∃ (x : ℝ), (f ^ n : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
have rw₁ : Ne (α := ℝ) (↑n : ℝ) 0
Tactic: rw [eq_div_iff, mul_comm, ← translationNumber_pow]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
hf : Continuous (X := ℝ) (Y := ℝ) (⇑f : (a : ℝ) → ℝ)
m : ℤ
n : ℕ
hn : 0 < n
⊢ τ f = HDiv.hDiv (α := ℝ) (↑m : ℝ) (↑n : ℝ) ↔ ∃ (x : ℝ), (f ^ n : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
have rw : τ (f ^ n) = (↑m : ℝ) ↔ ∃ (x : ℝ), (f ^ n : (a : ℝ) → ℝ) x = x + (↑m : ℝ)
Tactic: rw [eq_div_iff, mul_comm, ← translationNumber_pow] <;> [skip; exact ne_of_gt (Nat.cast_pos.2 hn)]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
⊢ ∀ (x : ℝ),
    BddAbove (α := ℝ)
      (range fun (g : G) ↦
        (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ))
have refine : ∀ (x : ℝ),
  Membership.mem (γ := Set ℝ)
    (upperBounds
      (range fun (g : G) ↦
        (((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
          ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ)))
    (x + 2)
Tactic: refine fun x => ⟨x + 2, ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
x : ℝ
g : G
⊢ τ ((f₂ : (a : G) → CircleDeg1Lift) g⁻¹) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
have rw : τ (↑((f₂.toHomUnits : (a : G) → CircleDeg1Liftˣ) g⁻¹) : CircleDeg1Lift) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
Tactic: rw [← MonoidHom.coe_toHomUnits, map_inv, translationNumber_units_inv,
        MonoidHom.coe_toHomUnits]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
x : ℝ
g : G
rw : τ (↑((f₂.toHomUnits : (a : G) → CircleDeg1Liftˣ) g⁻¹) : CircleDeg1Lift) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
⊢ τ ((f₂ : (a : G) → CircleDeg1Lift) g⁻¹) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
have rw₁ : τ (↑((f₂.toHomUnits : (a : G) → CircleDeg1Liftˣ) g)⁻¹ : CircleDeg1Lift) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
Tactic: rw [← MonoidHom.coe_toHomUnits, map_inv, translationNumber_units_inv,
        MonoidHom.coe_toHomUnits]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
x : ℝ
g : G
rw : τ (↑((f₂.toHomUnits : (a : G) → CircleDeg1Liftˣ) g⁻¹) : CircleDeg1Lift) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
rw₁ : τ (↑((f₂.toHomUnits : (a : G) → CircleDeg1Liftˣ) g)⁻¹ : CircleDeg1Lift) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
⊢ τ ((f₂ : (a : G) → CircleDeg1Lift) g⁻¹) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
have rw₂ : -τ (↑((f₂.toHomUnits : (a : G) → CircleDeg1Liftˣ) g) : CircleDeg1Lift) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
Tactic: rw [← MonoidHom.coe_toHomUnits, map_inv, translationNumber_units_inv,
        MonoidHom.coe_toHomUnits]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
x : ℝ
g : G
rw : τ (↑((f₂.toHomUnits : (a : G) → CircleDeg1Liftˣ) g⁻¹) : CircleDeg1Lift) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
rw₁ : τ (↑((f₂.toHomUnits : (a : G) → CircleDeg1Liftˣ) g)⁻¹ : CircleDeg1Lift) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
rw₂ : -τ (↑((f₂.toHomUnits : (a : G) → CircleDeg1Liftˣ) g) : CircleDeg1Lift) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
⊢ τ ((f₂ : (a : G) → CircleDeg1Lift) g⁻¹) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
have rw₃ : -τ ((f₂ : (a : G) → CircleDeg1Lift) g) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
Tactic: rw [← MonoidHom.coe_toHomUnits, map_inv, translationNumber_units_inv,
        MonoidHom.coe_toHomUnits]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (hypothesis)
Goal:
G : Type u_1
inst : Group G
f₁ f₂ : G →* CircleDeg1Lift
h : ∀ (g : G), τ ((f₁ : (a : G) → CircleDeg1Lift) g) = τ ((f₂ : (a : G) → CircleDeg1Lift) g)
x : ℝ
g : G
⊢ (fun (g : G) ↦
        ((((f₂ : (a : G) → CircleDeg1Lift) g⁻¹ : CircleDeg1Lift) : (a : ℝ) → ℝ)
            ((((f₁ : (a : G) → CircleDeg1Lift) g : CircleDeg1Lift) : (a : ℝ) → ℝ) x : ℝ) :
          ℝ))
      g ≤
    x + 2
have this : τ ((f₂ : (a : G) → CircleDeg1Lift) g⁻¹) = -τ ((f₂ : (a : G) → CircleDeg1Lift) g)
Tactic: have : τ (f₂ g⁻¹) = -τ (f₂ g) := by
      rw [← MonoidHom.coe_toHomUnits, map_inv, translationNumber_units_inv,
        MonoidHom.coe_toHomUnits]