awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.NormedSpace (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → α
g : α → E
x : α
h : Bornology.IsBounded.{u_2} (α := E) (range fun (x_1 : ℕ) ↦ g (f^[x_1] x))
C : ℝ
hC : ∀ (x_1 y : ℕ), dist (g (f^[x_1] x)) (g (f^[y] x)) ≤ C
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / (↑n : ℝ)) atTop (𝓝 0)
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x) atTop (𝓝 0)
have refine : ∀ (n : ℕ), ‖birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x‖ ≤ C / (↑n : ℝ)
Tactic: refine squeeze_zero_norm (fun n ↦ ?_) this
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.NormedSpace (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → α
g : α → E
x : α
h : Bornology.IsBounded.{u_2} (α := E) (range fun (x_1 : ℕ) ↦ g (f^[x_1] x))
C : ℝ
hC : ∀ (x_1 y : ℕ), dist (g (f^[x_1] x)) (g (f^[y] x)) ≤ C
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
⊢ ‖birkhoffAverage 𝕜 f g n (f x) - birkhoffAverage 𝕜 f g n x‖ ≤ C / (↑n : ℝ)
have rw : dist (g (f^[n] x)) (g x) / (↑n : ℝ) ≤ C / (↑n : ℝ)
Tactic: rw [← dist_eq_norm, dist_birkhoffAverage_apply_birkhoffAverage]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.NormedSpace (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
𝕜 : Type u_3
inst_1 : RCLike 𝕜
inst_2 : NormedSpace 𝕜 E
f : α → α
g : α → E
x : α
h : Bornology.IsBounded.{u_2} (α := E) (range fun (x_1 : ℕ) ↦ g (f^[x_1] x))
C : ℝ
hC : ∀ (x_1 y : ℕ), dist (g (f^[x_1] x)) (g (f^[y] x)) ≤ C
this : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C / (↑n : ℝ)) atTop (𝓝 0)
n : ℕ
⊢ dist (g (f^[n] x)) (g x) / (↑n : ℝ) ≤ C / (↑n : ℝ)
have hab : dist (g (f^[n] x)) (g x) ≤ C
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.NormedSpace (goal)
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
⊢ UniformEquicontinuous (birkhoffAverage 𝕜 f g)
have refine : ∀ (ε : ℝ) (hε : 0 < ε),
  ∀ᶠ (xy : X × X) in 𝓤 X,
    ∀ (i : ℕ),
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε}
        (birkhoffAverage 𝕜 f g i xy.1, birkhoffAverage 𝕜 f g i xy.2)
Tactic: refine Metric.uniformity_basis_dist_le.uniformEquicontinuous_iff_right.2 fun ε hε ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.NormedSpace (goal)
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
⊢ ∀ᶠ (xy : X × X) in 𝓤 X,
    ∀ (i : ℕ),
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε}
        (birkhoffAverage 𝕜 f g i xy.1, birkhoffAverage 𝕜 f g i xy.2)
have rcases : ∀ (δ : ℝ≥0∞) (hδ₀ : 0 < δ)
  (hδε :
    ∀ (x y : X),
      Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
        Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε} (g x, g y)),
  ∀ᶠ (xy : X × X) in 𝓤 X,
    ∀ (i : ℕ),
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε}
        (birkhoffAverage 𝕜 f g i xy.1, birkhoffAverage 𝕜 f g i xy.2)
Tactic: rcases (uniformity_basis_edist_le.uniformContinuous_iff Metric.uniformity_basis_dist_le).1 hg ε hε
    with ⟨δ, hδ₀, hδε⟩
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.NormedSpace (goal)
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε :
  ∀ (x y : X),
    Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε} (g x, g y)
⊢ ∀ᶠ (xy : X × X) in 𝓤 X,
    ∀ (i : ℕ),
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε}
        (birkhoffAverage 𝕜 f g i xy.1, birkhoffAverage 𝕜 f g i xy.2)
have refine : ∀ {x y : X} (h : edist x y < δ) (n : ℕ),
  Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε}
    (birkhoffAverage 𝕜 f g n (x, y).1, birkhoffAverage 𝕜 f g n (x, y).2)
Tactic: refine mem_uniformity_edist.2 ⟨δ, hδ₀, fun {x y} h n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.NormedSpace (goal)
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε :
  ∀ (x y : X),
    Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε} (g x, g y)
x y : X
h : edist x y < δ
n : ℕ
⊢ HDiv.hDiv (α := ℝ) (∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))) (↑n : ℝ) ≤
    HDiv.hDiv (α := ℝ) (∑ _k ∈ Finset.range n, ε) (↑n : ℝ)
have hab : ∀ i ∈ Finset.range n, dist (g (f^[i] x)) (g (f^[i] y)) ≤ ε
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.NormedSpace (goal)
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε :
  ∀ (x y : X),
    Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε} (g x, g y)
x y : X
h : edist x y < δ
n i : ℕ
h_1 : i ∈ Finset.range n
⊢ dist (g (f^[i] x)) (g (f^[i] y)) ≤ ε
have hab : Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (f^[i] x, f^[i] y)
Tactic: refine hδε _ _ ?_
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.NormedSpace (goal)
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε :
  ∀ (x y : X),
    Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε} (g x, g y)
x y : X
h : edist x y < δ
n : ℕ
⊢ (↑n : ℝ) * ε / (↑n : ℝ) ≤ ε
have inl : ∀ (hn : n = 0), (↑n : ℝ) * ε / (↑n : ℝ) ≤ ε
Tactic: rcases eq_or_ne n 0 with hn | hn
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.NormedSpace (goal)
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε :
  ∀ (x y : X),
    Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε} (g x, g y)
x y : X
h : edist x y < δ
n : ℕ
inl : ∀ (hn : n = 0), (↑n : ℝ) * ε / (↑n : ℝ) ≤ ε
⊢ (↑n : ℝ) * ε / (↑n : ℝ) ≤ ε
have inr : ∀ (hn : n ≠ 0), (↑n : ℝ) * ε / (↑n : ℝ) ≤ ε
Tactic: rcases eq_or_ne n 0 with hn | hn
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.NormedSpace (goal)
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε :
  ∀ (x y : X),
    Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
      Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε} (g x, g y)
x y : X
h : edist x y < δ
n : ℕ
⊢ Membership.mem (γ := Set (E × E)) {p : E × E | dist p.1 p.2 ≤ ε}
    (birkhoffAverage 𝕜 f g n (x, y).1, birkhoffAverage 𝕜 f g n (x, y).2)
have dist : HDiv.hDiv (α := ℝ) (∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))) (↑n : ℝ) ≤
  HDiv.hDiv (α := ℝ) (∑ _k ∈ Finset.range n, ε) (↑n : ℝ)
Tactic: calc
    dist (birkhoffAverage 𝕜 f g n x) (birkhoffAverage 𝕜 f g n y)
      ≤ (∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))) / n :=
      dist_birkhoffAverage_birkhoffAverage_le ..
    _ ≤ (∑ _k ∈ Finset.range n, ε) / n := by
      gcongr
      refine hδε _ _ ?_
      simpa using (hf.iterate _).edist_le_mul_of_le h.le
    _ = n * ε / n := by simp
    _ ≤ ε := by
      rcases eq_or_ne n 0 with hn | hn <;> simp [hn, hε.le, mul_div_cancel_left₀]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.NormedSpace (goal)
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε :
  ∀ (x y : X),
    Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
      Membership.mem (γ := Set (E × E)) {p : E × E | Dist.dist p.1 p.2 ≤ ε} (g x, g y)
x y : X
h : edist x y < δ
n : ℕ
dist :
  HDiv.hDiv (α := ℝ) (∑ k ∈ Finset.range n, Dist.dist (g (f^[k] x)) (g (f^[k] y))) (↑n : ℝ) ≤
    HDiv.hDiv (α := ℝ) (∑ _k ∈ Finset.range n, ε) (↑n : ℝ)
⊢ Membership.mem (γ := Set (E × E)) {p : E × E | Dist.dist p.1 p.2 ≤ ε}
    (birkhoffAverage 𝕜 f g n (x, y).1, birkhoffAverage 𝕜 f g n (x, y).2)
have dist₁ : HDiv.hDiv (α := ℝ) (∑ _k ∈ Finset.range n, ε) (↑n : ℝ) = (↑n : ℝ) * ε / (↑n : ℝ)
Tactic: calc
    dist (birkhoffAverage 𝕜 f g n x) (birkhoffAverage 𝕜 f g n y)
      ≤ (∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))) / n :=
      dist_birkhoffAverage_birkhoffAverage_le ..
    _ ≤ (∑ _k ∈ Finset.range n, ε) / n := by
      gcongr
      refine hδε _ _ ?_
      simpa using (hf.iterate _).edist_le_mul_of_le h.le
    _ = n * ε / n := by simp
    _ ≤ ε := by
      rcases eq_or_ne n 0 with hn | hn <;> simp [hn, hε.le, mul_div_cancel_left₀]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.NormedSpace (goal)
Goal:
𝕜 : Type u_1
X : Type u_2
E : Type u_3
inst : PseudoEMetricSpace X
inst_1 : RCLike 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
f : X → X
g : X → E
hf : LipschitzWith 1 f
hg : UniformContinuous g
ε : ℝ
hε : 0 < ε
δ : ℝ≥0∞
hδ₀ : 0 < δ
hδε :
  ∀ (x y : X),
    Membership.mem (γ := SetRel X X) {p : X × X | edist p.1 p.2 ≤ δ} (x, y) →
      Membership.mem (γ := Set (E × E)) {p : E × E | Dist.dist p.1 p.2 ≤ ε} (g x, g y)
x y : X
h : edist x y < δ
n : ℕ
dist :
  HDiv.hDiv (α := ℝ) (∑ k ∈ Finset.range n, Dist.dist (g (f^[k] x)) (g (f^[k] y))) (↑n : ℝ) ≤
    HDiv.hDiv (α := ℝ) (∑ _k ∈ Finset.range n, ε) (↑n : ℝ)
dist₁ : HDiv.hDiv (α := ℝ) (∑ _k ∈ Finset.range n, ε) (↑n : ℝ) = (↑n : ℝ) * ε / (↑n : ℝ)
⊢ Membership.mem (γ := Set (E × E)) {p : E × E | Dist.dist p.1 p.2 ≤ ε}
    (birkhoffAverage 𝕜 f g n (x, y).1, birkhoffAverage 𝕜 f g n (x, y).2)
have dist₂ : (↑n : ℝ) * ε / (↑n : ℝ) ≤ ε
Tactic: calc
    dist (birkhoffAverage 𝕜 f g n x) (birkhoffAverage 𝕜 f g n y)
      ≤ (∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))) / n :=
      dist_birkhoffAverage_birkhoffAverage_le ..
    _ ≤ (∑ _k ∈ Finset.range n, ε) / n := by
      gcongr
      refine hδε _ _ ?_
      simpa using (hf.iterate _).edist_le_mul_of_le h.le
    _ = n * ε / n := by simp
    _ ≤ ε := by
      rcases eq_or_ne n 0 with hn | hn <;> simp [hn, hε.le, mul_div_cancel_left₀]
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.QuasiMeasurePreserving (goal)
Goal:
α : Type u_1
M : Type u_2
inst : MeasurableSpace α
inst_1 : AddCommMonoid M
f : α → α
μ : Measure α
φ ψ : α → M
hf : QuasiMeasurePreserving f μ μ
hφ : φ =ᵐ[μ] ψ
n : ℕ
⊢ birkhoffSum f φ n =ᵐ[μ] birkhoffSum f ψ n
have apply : ∀ᵐ (x : α) ∂μ, ∀ x_1 ∈ Finset.range n, φ (f^[x_1] x) = ψ (f^[x_1] x)
Tactic: apply Eventually.mono _ (fun _ => Finset.sum_congr rfl)
-- Lean 4 proof step from Mathlib.Dynamics.BirkhoffSum.QuasiMeasurePreserving (goal)
Goal:
α : Type u_1
M : Type u_2
inst : MeasurableSpace α
inst_1 : AddCommMonoid M
f : α → α
μ : Measure α
φ ψ : α → M
hf : QuasiMeasurePreserving f μ μ
hφ : φ =ᵐ[μ] ψ
n : ℕ
⊢ ∀ᵐ (x : α) ∂μ, ∀ x_1 ∈ Finset.range n, φ (f^[x_1] x) = ψ (f^[x_1] x)
have apply : ∀ (i : ℕ), ∀ᵐ (a : α) ∂μ, i ∈ Finset.range n → φ (f^[i] a) = ψ (f^[i] a)
Tactic: apply ae_all_iff.mpr (fun i => ?_)
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
x : ℝ
⊢ (f : (a : ℝ) → ℝ) (1 + x) = HAdd.hAdd (α := ℝ) (β := ℝ) (1 : ℝ) ((f : (a : ℝ) → ℝ) x : ℝ)
have rw : (f : (a : ℝ) → ℝ) (x + 1) = HAdd.hAdd (α := ℝ) (β := ℝ) (1 : ℝ) ((f : (a : ℝ) → ℝ) x : ℝ)
Tactic: rw [add_comm, map_add_one, add_comm 1]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
x : ℝ
rw : (f : (a : ℝ) → ℝ) (x + 1) = HAdd.hAdd (α := ℝ) (β := ℝ) (1 : ℝ) ((f : (a : ℝ) → ℝ) x : ℝ)
⊢ (f : (a : ℝ) → ℝ) (1 + x) = HAdd.hAdd (α := ℝ) (β := ℝ) (1 : ℝ) ((f : (a : ℝ) → ℝ) x : ℝ)
have rw₁ : HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) (1 : ℝ) =
  HAdd.hAdd (α := ℝ) (β := ℝ) (1 : ℝ) ((f : (a : ℝ) → ℝ) x : ℝ)
Tactic: rw [add_comm, map_add_one, add_comm 1]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
x : ℝ
rw : (f : (a : ℝ) → ℝ) (x + 1) = HAdd.hAdd (α := ℝ) (β := ℝ) (1 : ℝ) ((f : (a : ℝ) → ℝ) x : ℝ)
rw₁ :
  HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) (1 : ℝ) =
    HAdd.hAdd (α := ℝ) (β := ℝ) (1 : ℝ) ((f : (a : ℝ) → ℝ) x : ℝ)
⊢ (f : (a : ℝ) → ℝ) (1 + x) = HAdd.hAdd (α := ℝ) (β := ℝ) (1 : ℝ) ((f : (a : ℝ) → ℝ) x : ℝ)
have rw₂ : HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) (1 : ℝ) =
  HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) (1 : ℝ)
Tactic: rw [add_comm, map_add_one, add_comm 1]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
x : ℝ
n : ℕ
⊢ Eq (α := ℝ → ℝ)
    (⇑(↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x)) :
            CircleDeg1Lift) :
        (a : ℝ) → ℝ)^[n]
    (⇑(↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
              ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) ((↑n : ℝ) * x))) :
          CircleDeg1Lift) :
      (a : ℝ) → ℝ)
have rw : Eq (α := ℝ → ℝ)
  (⇑(HPow.hPow (α := CircleDeg1Lift)
        (↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
              ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x)) :
          CircleDeg1Lift)
        n) :
    (a : ℝ) → ℝ)
  (⇑(↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
            ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) ((↑n : ℝ) * x))) :
        CircleDeg1Lift) :
    (a : ℝ) → ℝ)
Tactic: rw [← coe_pow, ← Units.val_pow_eq_pow_val, translate_pow]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
x : ℝ
n : ℕ
rw :
  Eq (α := ℝ → ℝ)
    (⇑(HPow.hPow (α := CircleDeg1Lift)
          (↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x)) :
            CircleDeg1Lift)
          n) :
      (a : ℝ) → ℝ)
    (⇑(↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
              ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) ((↑n : ℝ) * x))) :
          CircleDeg1Lift) :
      (a : ℝ) → ℝ)
⊢ Eq (α := ℝ → ℝ)
    (⇑(↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x)) :
            CircleDeg1Lift) :
        (a : ℝ) → ℝ)^[n]
    (⇑(↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
              ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) ((↑n : ℝ) * x))) :
          CircleDeg1Lift) :
      (a : ℝ) → ℝ)
have rw₁ : Eq (α := ℝ → ℝ)
  (⇑(↑(HPow.hPow (α := CircleDeg1Liftˣ)
            ((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x) :
              CircleDeg1Liftˣ)
            n) :
        CircleDeg1Lift) :
    (a : ℝ) → ℝ)
  (⇑(↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
            ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) ((↑n : ℝ) * x))) :
        CircleDeg1Lift) :
    (a : ℝ) → ℝ)
Tactic: rw [← coe_pow, ← Units.val_pow_eq_pow_val, translate_pow]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
x : ℝ
n : ℕ
rw :
  Eq (α := ℝ → ℝ)
    (⇑(HPow.hPow (α := CircleDeg1Lift)
          (↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x)) :
            CircleDeg1Lift)
          n) :
      (a : ℝ) → ℝ)
    (⇑(↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
              ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) ((↑n : ℝ) * x))) :
          CircleDeg1Lift) :
      (a : ℝ) → ℝ)
rw₁ :
  Eq (α := ℝ → ℝ)
    (⇑(↑(HPow.hPow (α := CircleDeg1Liftˣ)
              ((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                  ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x) :
                CircleDeg1Liftˣ)
              n) :
          CircleDeg1Lift) :
      (a : ℝ) → ℝ)
    (⇑(↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
              ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) ((↑n : ℝ) * x))) :
          CircleDeg1Lift) :
      (a : ℝ) → ℝ)
⊢ Eq (α := ℝ → ℝ)
    (⇑(↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
                ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) x)) :
            CircleDeg1Lift) :
        (a : ℝ) → ℝ)^[n]
    (⇑(↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
              ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) ((↑n : ℝ) * x))) :
          CircleDeg1Lift) :
      (a : ℝ) → ℝ)
have rw₂ : Eq (α := ℝ → ℝ)
  (⇑(↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
            ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) ((↑n : ℝ) * x))) :
        CircleDeg1Lift) :
    (a : ℝ) → ℝ)
  (⇑(↑((translate : (a : Multiplicative ℝ) → CircleDeg1Liftˣ)
            ((Multiplicative.ofAdd : (a : ℝ) → Multiplicative ℝ) ((↑n : ℝ) * x))) :
        CircleDeg1Lift) :
    (a : ℝ) → ℝ)
Tactic: rw [← coe_pow, ← Units.val_pow_eq_pow_val, translate_pow]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
n : ℤ
⊢ (f : (a : ℝ) → ℝ) (↑n : ℝ) = HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ((↑n : ℝ) : ℝ)
have rw : Eq (α := ℝ) ((f : (a : ℝ) → ℝ) (↑n : ℝ) : ℝ) ((f : (a : ℝ) → ℝ) (HAdd.hAdd (α := ℝ) 0 (↑n : ℝ)) : ℝ)
Tactic: rw [← f.map_add_int, zero_add]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
n : ℤ
rw : Eq (α := ℝ) ((f : (a : ℝ) → ℝ) (↑n : ℝ) : ℝ) ((f : (a : ℝ) → ℝ) (HAdd.hAdd (α := ℝ) 0 (↑n : ℝ)) : ℝ)
⊢ (f : (a : ℝ) → ℝ) (↑n : ℝ) = HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ((↑n : ℝ) : ℝ)
have rw₁ : Eq (α := ℝ) ((f : (a : ℝ) → ℝ) (↑n : ℝ) : ℝ) ((f : (a : ℝ) → ℝ) (↑n : ℝ) : ℝ)
Tactic: rw [← f.map_add_int, zero_add]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
x : ℝ
⊢ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) (fract x) : ℝ) (fract x) = HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
have rw : HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) (x - (↑⌊x⌋ : ℝ)) : ℝ) (x - (↑⌊x⌋ : ℝ)) =
  HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
Tactic: rw [Int.fract, f.map_sub_int, sub_sub_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
x : ℝ
rw :
  HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) (x - (↑⌊x⌋ : ℝ)) : ℝ) (x - (↑⌊x⌋ : ℝ)) =
    HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
⊢ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) (fract x) : ℝ) (fract x) = HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
have rw₁ : HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) ((↑⌊x⌋ : ℝ) : ℝ) - (x - (↑⌊x⌋ : ℝ)) =
  HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
Tactic: rw [Int.fract, f.map_sub_int, sub_sub_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
x : ℝ
rw :
  HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) (x - (↑⌊x⌋ : ℝ)) : ℝ) (x - (↑⌊x⌋ : ℝ)) =
    HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
rw₁ :
  HSub.hSub (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) ((↑⌊x⌋ : ℝ) : ℝ) - (x - (↑⌊x⌋ : ℝ)) =
    HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
⊢ HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) (fract x) : ℝ) (fract x) = HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
have rw₂ : HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x = HSub.hSub (α := ℝ) ((f : (a : ℝ) → ℝ) x : ℝ) x
Tactic: rw [Int.fract, f.map_sub_int, sub_sub_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f g : CircleDeg1Lift
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ((↑(ceil (α := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ)) : ℝ) : ℝ) <
    HAdd.hAdd (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (HAdd.hAdd (α := ℝ) (β := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) (1 : ℝ))
have bc : (↑(ceil (α := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ)) : ℝ) < HAdd.hAdd (α := ℝ) (β := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) (1 : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f g : CircleDeg1Lift
⊢ HAdd.hAdd (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) (HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) (1 : ℝ)) <
    HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ((↑(floor (α := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ)) : ℝ) : ℝ)
have bc : HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ) (1 : ℝ) < (↑(floor (α := ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ)) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f g : CircleDeg1Lift
⊢ dist (HAdd.hAdd (α := ℝ) (β := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ))
      ((f : (a : ℝ) → ℝ) ((g : (a : ℝ) → ℝ) 0 : ℝ)) <
    1
have 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
Tactic: rw [dist_comm, Real.dist_eq, abs_lt, lt_sub_iff_add_lt', sub_lt_iff_lt_add', ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
n : ℕ
⊢ (↑n : ℤ) * floor (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ) ≤ floor (α := ℝ) ((⇑f : (a : ℝ) → ℝ)^[n] 0)
have rw : 0 + HMul.hMul (α := ℝ) (↑n : ℝ) (↑(floor (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ)) : ℝ) ≤ (⇑f : (a : ℝ) → ℝ)^[n] 0
Tactic: rw [le_floor, Int.cast_mul, Int.cast_natCast, ← zero_add ((n : ℝ) * _)]
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (goal)
Goal:
f : CircleDeg1Lift
n : ℕ
⊢ 0 + HMul.hMul (α := ℝ) (↑n : ℝ) (↑(floor (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ)) : ℝ) ≤ (⇑f : (a : ℝ) → ℝ)^[n] 0
have h : HAdd.hAdd (α := ℝ) 0 (↑(floor (α := ℝ) ((f : (a : ℝ) → ℝ) 0 : ℝ)) : ℝ) ≤ (f : (a : ℝ) → ℝ) 0
Tactic: apply le_iterate_of_add_int_le_map
-- Lean 4 proof step from Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber (hypothesis)
Goal:
f : CircleDeg1Lift
n : ℕ
⊢ dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / 2 / HPow.hPow (α := ℝ) 2 n
have this : 0 < HPow.hPow (α := ℝ) 2 (n + 1)
Tactic: have : 0 < (2 ^ (n + 1) : ℝ) := pow_pos zero_lt_two _
-- 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 / 2 / HPow.hPow (α := ℝ) 2 n
have rw : dist (f.transnumAuxSeq n) (f.transnumAuxSeq (n + 1)) < 1 / |HPow.hPow (α := ℝ) 2 (n + 1)|
Tactic: rw [div_div, ← pow_succ', ← abs_of_pos this]