awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
d : AddCircle T
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
hd :
  Tendsto (β := ℝ≥0∞)
    (fun (j : ι) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
        ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞))
    l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : LE.le (α := ℝ) 1 (↑(n j) : ℝ)
hI₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) (0 : ℝ≥0∞)
hI₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) (∞ : ℝ≥0∞)
hI₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) ((↑(n j) : ℝ≥0∞) : ℝ≥0∞) =
    ENNReal.ofReal T
inr :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal T) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞)
      ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞)
inr₁ :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal T) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞)
      (HSMul.hSMul (β := ℝ≥0∞) (addOrderOf (u j))
        ((volume : (a : Set (AddCircle T)) → ℝ≥0∞)
            (s ∩ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(addOrderOf (u j)) : ℝ))) :
          ℝ≥0∞))
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
      ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T)
have inr₂ : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal T) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞)
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(addOrderOf (u j)) : ℝ≥0∞) : ℝ≥0∞)
      ((volume : (a : Set (AddCircle T)) → ℝ≥0∞)
          (s ∩ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(addOrderOf (u j)) : ℝ))) :
        ℝ≥0∞))
Tactic: rw [ENNReal.div_eq_div_iff hT₁ ENNReal.ofReal_ne_top hI₀ hI₁,
    volume_of_add_preimage_eq s _ (u j) d huj (hu₁ j) closedBall_ae_eq_ball, nsmul_eq_mul, ←
    mul_assoc, this, hI₂]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
s : Set (AddCircle T)
ι : Type u_1
l : Filter ι
inst : l.NeBot
u : ι → AddCircle T
μ : Measure (AddCircle T) := volume
hs : NullMeasurableSet s μ
hu₁ : ∀ (i : ι), u i +ᵥ s =ᶠ[ae μ] s
n : ι → ℕ := addOrderOf ∘ u
hu₂ : Tendsto n l atTop
hT₀ : 0 < T
hT₁ : ENNReal.ofReal T ≠ 0
h : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
d : AddCircle T
I : ι → Set (AddCircle T) := fun (j : ι) ↦ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(n j) : ℝ))
hd :
  Tendsto (β := ℝ≥0∞)
    (fun (j : ι) ↦
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
        ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞))
    l (𝓝 1)
j : ι
hj : 0 < n j
this : addOrderOf (u j) = n j
huj : IsOfFinAddOrder (u j)
huj' : LE.le (α := ℝ) 1 (↑(n j) : ℝ)
hI₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) (0 : ℝ≥0∞)
hI₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) (∞ : ℝ≥0∞)
hI₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) ((↑(n j) : ℝ≥0∞) : ℝ≥0∞) =
    ENNReal.ofReal T
inr :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal T) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞)
      ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞)
inr₁ :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal T) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞)
      (HSMul.hSMul (β := ℝ≥0∞) (addOrderOf (u j))
        ((volume : (a : Set (AddCircle T)) → ℝ≥0∞)
            (s ∩ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(addOrderOf (u j)) : ℝ))) :
          ℝ≥0∞))
inr₂ :
  HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal T) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(addOrderOf (u j)) : ℝ≥0∞) : ℝ≥0∞)
        ((volume : (a : Set (AddCircle T)) → ℝ≥0∞)
            (s ∩ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(addOrderOf (u j)) : ℝ))) :
          ℝ≥0∞))
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞)
      ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞) =
    HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) s : ℝ≥0∞) (ENNReal.ofReal T)
have inr₃ : HMul.hMul (β := ℝ≥0∞) (ENNReal.ofReal T) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ I j) : ℝ≥0∞) =
  HMul.hMul (β := ℝ≥0∞)
    (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set (AddCircle T)) → ℝ≥0∞) (I j) : ℝ≥0∞)
      ((↑(addOrderOf (u j)) : ℝ≥0∞) : ℝ≥0∞))
    ((volume : (a : Set (AddCircle T)) → ℝ≥0∞) (s ∩ closedBall d (T / HMul.hMul (α := ℝ) 2 (↑(addOrderOf (u j)) : ℝ))) :
      ℝ≥0∞)
Tactic: rw [ENNReal.div_eq_div_iff hT₁ ENNReal.ofReal_ne_top hI₀ hI₁,
    volume_of_add_preimage_eq s _ (u j) d huj (hu₁ j) closedBall_ae_eq_ball, nsmul_eq_mul, ←
    mul_assoc, this, hI₂]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun (y : AddCircle T) ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun (j : ℕ) ↦ (↑(HDiv.hDiv (α := ℝ) 1 (↑(n.natAbs ^ j) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
⊢ 1 < n.natAbs
have rwa : ∀ (hn : LT.lt (α := ℤ) 1 (↑n.natAbs : ℤ)) (s : Set (AddCircle T)) (hs : MeasurableSet s)
  (hs' : (fun (y : AddCircle T) ↦ n • y) ⁻¹' s = s), 1 < n.natAbs
Tactic: rwa [Int.abs_eq_natAbs, Nat.one_lt_cast] at hn
Cleared hypotheses: s, hs, hs', u
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun (y : AddCircle T) ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun (j : ℕ) ↦ (↑(HDiv.hDiv (α := ℝ) 1 (↑(n.natAbs ^ j) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
rwa :
  ∀ (hn : LT.lt (α := ℤ) 1 (↑n.natAbs : ℤ)) (s : Set (AddCircle T)) (hs : MeasurableSet s)
    (hs' : (fun (y : AddCircle T) ↦ n • y) ⁻¹' s = s), 1 < n.natAbs
⊢ 1 < n.natAbs
have rwa₁ : ∀ (hn : 1 < n.natAbs) (s : Set (AddCircle T)) (hs : MeasurableSet s) (hs' : (fun (y : AddCircle T) ↦ n • y) ⁻¹' s = s),
  1 < n.natAbs
Tactic: rwa [Int.abs_eq_natAbs, Nat.one_lt_cast] at hn
Cleared hypotheses: s, hs, hs', u
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun (y : AddCircle T) ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun (j : ℕ) ↦ (↑(HDiv.hDiv (α := ℝ) 1 (↑(n.natAbs ^ j) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
⊢ EventuallyConst s (ae (F := autoParam (Measure (AddCircle T)) PreErgodic._auto_1) volume)
have hn₁ : 1 < n.natAbs
Tactic: replace hn : 1 < n.natAbs := by rwa [Int.abs_eq_natAbs, Nat.one_lt_cast] at hn
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn_1 : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun (y : AddCircle T) ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun (j : ℕ) ↦ (↑(HDiv.hDiv (α := ℝ) 1 (↑(n.natAbs ^ j) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hn : 1 < n.natAbs
j : ℕ
⊢ addOrderOf (u j) = n.natAbs ^ j
have h : Eq (α := ℝ) 1 (↑1 : ℝ)
Tactic: convert!
          addOrderOf_div_of_gcd_eq_one (p := T) (m := 1) (pow_pos (pos_of_gt hn) j) (gcd_one_left _)
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn_1 : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun (y : AddCircle T) ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun (j : ℕ) ↦ (↑(HDiv.hDiv (α := ℝ) 1 (↑(n.natAbs ^ j) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hn : 1 < n.natAbs
j : ℕ
⊢ Eq (α := ℝ) 1 (↑1 : ℝ)
have h : Eq (α := ℕ) 1 1
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn_1 : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun (y : AddCircle T) ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun (j : ℕ) ↦ (↑(HDiv.hDiv (α := ℝ) 1 (↑(n.natAbs ^ j) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hn : 1 < n.natAbs
⊢ EventuallyConst s (ae (F := autoParam (Measure (AddCircle T)) PreErgodic._auto_1) volume)
have hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
Tactic: have hu₀ : ∀ j, addOrderOf (u j) = n.natAbs ^ j := fun j => by
        convert!
          addOrderOf_div_of_gcd_eq_one (p := T) (m := 1) (pow_pos (pos_of_gt hn) j) (gcd_one_left _)
        norm_cast
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn_1 : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun (y : AddCircle T) ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun (j : ℕ) ↦ (↑(HDiv.hDiv (α := ℝ) 1 (↑(n.natAbs ^ j) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
j : ℕ
⊢ n ^ j • u j = 0
have rw : (↑(addOrderOf (u j)) : ℤ) ∣ n ^ j
Tactic: rw [← addOrderOf_dvd_iff_zsmul_eq_zero, hu₀, Int.natCast_pow, Int.natCast_natAbs, ← abs_pow,
          abs_dvd]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn_1 : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun (y : AddCircle T) ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun (j : ℕ) ↦ (↑(HDiv.hDiv (α := ℝ) 1 (↑(n.natAbs ^ j) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
j : ℕ
rw : (↑(addOrderOf (u j)) : ℤ) ∣ n ^ j
⊢ n ^ j • u j = 0
have rw₁ : (↑(n.natAbs ^ j) : ℤ) ∣ n ^ j
Tactic: rw [← addOrderOf_dvd_iff_zsmul_eq_zero, hu₀, Int.natCast_pow, Int.natCast_natAbs, ← abs_pow,
          abs_dvd]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn_1 : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun (y : AddCircle T) ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun (j : ℕ) ↦ (↑(HDiv.hDiv (α := ℝ) 1 (↑(n.natAbs ^ j) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
j : ℕ
rw : (↑(addOrderOf (u j)) : ℤ) ∣ n ^ j
rw₁ : (↑(n.natAbs ^ j) : ℤ) ∣ n ^ j
⊢ n ^ j • u j = 0
have rw₂ : HPow.hPow (α := ℤ) (↑n.natAbs : ℤ) j ∣ n ^ j
Tactic: rw [← addOrderOf_dvd_iff_zsmul_eq_zero, hu₀, Int.natCast_pow, Int.natCast_natAbs, ← abs_pow,
          abs_dvd]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn_1 : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun (y : AddCircle T) ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun (j : ℕ) ↦ (↑(HDiv.hDiv (α := ℝ) 1 (↑(n.natAbs ^ j) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
j : ℕ
rw : (↑(addOrderOf (u j)) : ℤ) ∣ n ^ j
rw₁ : (↑(n.natAbs ^ j) : ℤ) ∣ n ^ j
rw₂ : HPow.hPow (α := ℤ) (↑n.natAbs : ℤ) j ∣ n ^ j
⊢ n ^ j • u j = 0
have rw₃ : |n| ^ j ∣ n ^ j
Tactic: rw [← addOrderOf_dvd_iff_zsmul_eq_zero, hu₀, Int.natCast_pow, Int.natCast_natAbs, ← abs_pow,
          abs_dvd]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn_1 : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun (y : AddCircle T) ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun (j : ℕ) ↦ (↑(HDiv.hDiv (α := ℝ) 1 (↑(n.natAbs ^ j) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
j : ℕ
rw : (↑(addOrderOf (u j)) : ℤ) ∣ n ^ j
rw₁ : (↑(n.natAbs ^ j) : ℤ) ∣ n ^ j
rw₂ : HPow.hPow (α := ℤ) (↑n.natAbs : ℤ) j ∣ n ^ j
rw₃ : |n| ^ j ∣ n ^ j
⊢ n ^ j • u j = 0
have rw₄ : |n ^ j| ∣ n ^ j
Tactic: rw [← addOrderOf_dvd_iff_zsmul_eq_zero, hu₀, Int.natCast_pow, Int.natCast_natAbs, ← abs_pow,
          abs_dvd]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn_1 : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun (y : AddCircle T) ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun (j : ℕ) ↦ (↑(HDiv.hDiv (α := ℝ) 1 (↑(n.natAbs ^ j) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
j : ℕ
rw : (↑(addOrderOf (u j)) : ℤ) ∣ n ^ j
rw₁ : (↑(n.natAbs ^ j) : ℤ) ∣ n ^ j
rw₂ : HPow.hPow (α := ℤ) (↑n.natAbs : ℤ) j ∣ n ^ j
rw₃ : |n| ^ j ∣ n ^ j
rw₄ : |n ^ j| ∣ n ^ j
⊢ n ^ j • u j = 0
have rw₅ : n ^ j ∣ n ^ j
Tactic: rw [← addOrderOf_dvd_iff_zsmul_eq_zero, hu₀, Int.natCast_pow, Int.natCast_natAbs, ← abs_pow,
          abs_dvd]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn_1 : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun (y : AddCircle T) ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun (j : ℕ) ↦ (↑(HDiv.hDiv (α := ℝ) 1 (↑(n.natAbs ^ j) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
⊢ EventuallyConst s (ae (F := autoParam (Measure (AddCircle T)) PreErgodic._auto_1) volume)
have hnu : ∀ (j : ℕ), n ^ j • u j = 0
Tactic: have hnu : ∀ j, n ^ j • u j = 0 := fun j => by
        rw [← addOrderOf_dvd_iff_zsmul_eq_zero, hu₀, Int.natCast_pow, Int.natCast_natAbs, ← abs_pow,
          abs_dvd]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn_1 : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun (y : AddCircle T) ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun (j : ℕ) ↦ (↑(HDiv.hDiv (α := ℝ) 1 (↑(n.natAbs ^ j) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
j : ℕ
⊢ u j +ᵥ s =ᶠ[ae (F := Measure (AddCircle T)) volume] s
have rw : s =ᶠ[ae (F := Measure (AddCircle T)) volume] s
Tactic: rw [vadd_eq_self_of_preimage_zsmul_eq_self hs' (hnu j)]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn_1 : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun (y : AddCircle T) ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun (j : ℕ) ↦ (↑(HDiv.hDiv (α := ℝ) 1 (↑(n.natAbs ^ j) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
⊢ EventuallyConst s (ae (F := autoParam (Measure (AddCircle T)) PreErgodic._auto_1) volume)
have hu₁ : ∀ (j : ℕ), u j +ᵥ s =ᶠ[ae (F := Measure (AddCircle T)) volume] s
Tactic: have hu₁ : ∀ j, (u j +ᵥ s : Set _) =ᵐ[volume] s := fun j => by
        rw [vadd_eq_self_of_preimage_zsmul_eq_self hs' (hnu j)]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn_1 : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun (y : AddCircle T) ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun (j : ℕ) ↦ (↑(HDiv.hDiv (α := ℝ) 1 (↑(n.natAbs ^ j) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
hu₁ : ∀ (j : ℕ), u j +ᵥ s =ᶠ[ae (F := Measure (AddCircle T)) volume] s
⊢ Tendsto (β := ℕ) (fun (j : ℕ) ↦ addOrderOf (u j)) atTop atTop
have simp_rw : Tendsto (β := ℕ) (fun (j : ℕ) ↦ n.natAbs ^ j) atTop atTop
Tactic: simp_rw [hu₀]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn_1 : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun (y : AddCircle T) ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun (j : ℕ) ↦ (↑(HDiv.hDiv (α := ℝ) 1 (↑(n.natAbs ^ j) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
hu₁ : ∀ (j : ℕ), u j +ᵥ s =ᶠ[ae (F := Measure (AddCircle T)) volume] s
⊢ EventuallyConst s (ae (F := autoParam (Measure (AddCircle T)) PreErgodic._auto_1) volume)
have hu₂ : Tendsto (β := ℕ) (fun (j : ℕ) ↦ addOrderOf (u j)) atTop atTop
Tactic: have hu₂ : Tendsto (fun j => addOrderOf <| u j) atTop atTop := by
        simp_rw [hu₀]; exact tendsto_pow_atTop_atTop_of_one_lt hn
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn_1 : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun (y : AddCircle T) ↦ n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun (j : ℕ) ↦ (↑(HDiv.hDiv (α := ℝ) 1 (↑(n.natAbs ^ j) : ℝ) * T) : ℝ ⧸ AddSubgroup.zmultiples T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
hu₁ : ∀ (j : ℕ), u j +ᵥ s =ᶠ[ae (F := Measure (AddCircle T)) volume] s
hu₂ : Tendsto (β := ℕ) (fun (j : ℕ) ↦ addOrderOf (u j)) atTop atTop
⊢ EventuallyConst s (ae (F := autoParam (Measure (AddCircle T)) PreErgodic._auto_1) volume)
have rw : s =ᶠ[ae (F := autoParam (Measure (AddCircle T)) PreErgodic._auto_1) volume] ∅ ∨
  s =ᶠ[ae (F := autoParam (Measure (AddCircle T)) PreErgodic._auto_1) volume] univ
Tactic: rw [eventuallyConst_set']
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun (y : AddCircle T) ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T :=
  MeasurableEquiv.addLeft
    (@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1))
⊢ Ergodic (m := MeasureSpace.toMeasurableSpace) f volume
have he : MeasurePreserving (α := AddCircle T) (β := AddCircle T) (⇑e : (a : AddCircle T) → AddCircle T) volume volume
Tactic: have he : MeasurePreserving e volume volume :=
    measurePreserving_add_left volume (DivisibleBy.div x <| n - 1)
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun (y : AddCircle T) ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T :=
  MeasurableEquiv.addLeft
    (@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1))
he : MeasurePreserving (α := AddCircle T) (β := AddCircle T) (⇑e : (a : AddCircle T) → AddCircle T) volume volume
this :
  Eq (α := AddCircle T → AddCircle T)
    ((⇑e : (a : AddCircle T) → AddCircle T) ∘ f ∘ (⇑e.symm : (a : AddCircle T) → AddCircle T)) fun (y : AddCircle T) ↦
    n • y
⊢ Ergodic (m := MeasureSpace.toMeasurableSpace) f volume
have rw : Ergodic (m := MeasureSpace.toMeasurableSpace) (fun (y : AddCircle T) ↦ n • y) volume
Tactic: rw [← he.ergodic_conjugate_iff, this]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun (y : AddCircle T) ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T :=
  MeasurableEquiv.addLeft
    (@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1))
he : MeasurePreserving (α := AddCircle T) (β := AddCircle T) (⇑e : (a : AddCircle T) → AddCircle T) volume volume
⊢ Ergodic (m := MeasureSpace.toMeasurableSpace) f volume
have suffices : Eq (α := AddCircle T → AddCircle T)
  ((⇑e : (a : AddCircle T) → AddCircle T) ∘ f ∘ (⇑e.symm : (a : AddCircle T) → AddCircle T)) fun (y : AddCircle T) ↦
  n • y
Tactic: suffices e ∘ f ∘ e.symm = fun y => n • y by
    rw [← he.ergodic_conjugate_iff, this]; exact ergodic_zsmul h
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun (y : AddCircle T) ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T :=
  MeasurableEquiv.addLeft
    (@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1))
he : MeasurePreserving (α := AddCircle T) (β := AddCircle T) (⇑e : (a : AddCircle T) → AddCircle T) volume volume
⊢ n - 1 ≠ 0
have h₁ : |1| < |n|
Tactic: rw [← abs_one] at h
Cleared hypotheses: h, f, e, he
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : |1| < |n|
f : AddCircle T → AddCircle T := fun (y : AddCircle T) ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T :=
  MeasurableEquiv.addLeft
    (@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1))
he : MeasurePreserving (α := AddCircle T) (β := AddCircle T) (⇑e : (a : AddCircle T) → AddCircle T) volume volume
⊢ n - 1 ≠ 0
have rw : n ≠ 1
Tactic: rw [sub_ne_zero]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (hypothesis)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun (y : AddCircle T) ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T :=
  MeasurableEquiv.addLeft
    (@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1))
he : MeasurePreserving (α := AddCircle T) (β := AddCircle T) (⇑e : (a : AddCircle T) → AddCircle T) volume volume
⊢ Eq (α := AddCircle T → AddCircle T)
    ((⇑e : (a : AddCircle T) → AddCircle T) ∘ f ∘ (⇑e.symm : (a : AddCircle T) → AddCircle T)) fun (y : AddCircle T) ↦
    n • y
have h₁ : n - 1 ≠ 0
Tactic: replace h : n - 1 ≠ 0 := by
    rw [← abs_one] at h; rw [sub_ne_zero]; exact ne_of_apply_ne _ (ne_of_gt h)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun (y : AddCircle T) ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T :=
  MeasurableEquiv.addLeft
    (@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1))
he : MeasurePreserving (α := AddCircle T) (β := AddCircle T) (⇑e : (a : AddCircle T) → AddCircle T) volume volume
h : n - 1 ≠ 0
| x + @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
have a : x
Tactic: congr
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun (y : AddCircle T) ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T :=
  MeasurableEquiv.addLeft
    (@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1))
he : MeasurePreserving (α := AddCircle T) (β := AddCircle T) (⇑e : (a : AddCircle T) → AddCircle T) volume volume
h : n - 1 ≠ 0
a : x
| x + @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
have a₁ : @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
Tactic: congr
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.AddCircle (goal)
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun (y : AddCircle T) ↦ n • y + x
e : AddCircle T ≃ᵐ AddCircle T :=
  MeasurableEquiv.addLeft
    (@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1))
he : MeasurePreserving (α := AddCircle T) (β := AddCircle T) (⇑e : (a : AddCircle T) → AddCircle T) volume volume
h : n - 1 ≠ 0
| x
have a : (n - 1) • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
Tactic: rw [← DivisibleBy.div_cancel x h]