-- Mathlib/Dynamics/Ergodic/AddCircle.lean
theorem ergodic_zsmul {n : ℤ} (hn : 1 < |n|) : Ergodic fun y : AddCircle T => n • y :=
  { measurePreserving_zsmul volume (abs_pos.mp <| lt_trans zero_lt_one hn) with
    aeconst_set := fun s hs hs' => by
      let u : ℕ → AddCircle T := fun j => ↑((↑1 : ℝ) / ↑(n.natAbs ^ j) * T)
      replace hn : 1 < n.natAbs

Proof state:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * T)
⊢ EventuallyConst s (ae volume)

Tactic:
replace hn : 1 < n.natAbs := by rwa [Int.abs_eq_natAbs, Nat.one_lt_cast] at hn

Result:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
⊢ EventuallyConst s (ae volume)

Proof state:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * 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 volume] s
hu₂ : Tendsto (fun j => addOrderOf (u j)) atTop atTop
⊢ s =ᶠ[ae volume] ∅ ∨ s =ᶠ[ae volume] univ

Tactic:
exact ae_empty_or_univ_of_forall_vadd_ae_eq_self hs.nullMeasurableSet hu₁ hu₂

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * 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 volume] s
⊢ EventuallyConst s (ae volume)

Tactic:
have hu₂ : Tendsto (fun j => addOrderOf <| u j) atTop atTop := by
  simp_rw [hu₀]; exact Nat.tendsto_pow_atTop_atTop_of_one_lt hn

Result:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * 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 volume] s
hu₂ : Tendsto (fun j => addOrderOf (u j)) atTop atTop
⊢ EventuallyConst s (ae volume)

Proof state:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
j : ℕ
⊢ addOrderOf (u j) = n.natAbs ^ j

Tactic:
convert addOrderOf_div_of_gcd_eq_one (p := T) (m := 1)
  (pow_pos (pos_of_gt hn) j) (gcd_one_left _)

Result:
case h.e'_2.h.e'_3.h.e'_4.h.e'_5.h.e'_5
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
j : ℕ
⊢ 1 = ↑1

Proof state:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
⊢ EventuallyConst s (ae volume)

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

Result:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
⊢ EventuallyConst s (ae volume)

Proof state:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
⊢ EventuallyConst s (ae volume)

Tactic:
let u : ℕ → AddCircle T := fun j => ↑((↑1 : ℝ) / ↑(n.natAbs ^ j) * T)

Result:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * T)
⊢ EventuallyConst s (ae volume)

Proof state:
case h.e'_2.h.e'_3.h.e'_4.h.e'_5.h.e'_5
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
j : ℕ
⊢ 1 = ↑1

Tactic:
norm_cast

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * 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 volume] s
hu₂ : Tendsto (fun j => addOrderOf (u j)) atTop atTop
⊢ EventuallyConst s (ae volume)

Tactic:
rw [eventuallyConst_set']

Result:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * 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 volume] s
hu₂ : Tendsto (fun j => addOrderOf (u j)) atTop atTop
⊢ s =ᶠ[ae volume] ∅ ∨ s =ᶠ[ae volume] univ

Proof state:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
⊢ EventuallyConst s (ae volume)

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)]

Result:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * 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 volume] s
⊢ EventuallyConst s (ae volume)

Proof state:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * T)
⊢ 1 < n.natAbs

Tactic:
rwa [Int.abs_eq_natAbs, Nat.one_lt_cast] at hn

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
⊢ EventuallyConst s (ae volume)

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]

Result:
T : ℝ
hT : Fact (0 < T)
n : ℤ
hn✝ : 1 < |n|
s : Set (AddCircle T)
hs : MeasurableSet s
hs' : (fun y => n • y) ⁻¹' s = s
u : ℕ → AddCircle T := fun j => ↑(1 / ↑(n.natAbs ^ j) * T)
hn : 1 < n.natAbs
hu₀ : ∀ (j : ℕ), addOrderOf (u j) = n.natAbs ^ j
hnu : ∀ (j : ℕ), n ^ j • u j = 0
⊢ EventuallyConst s (ae volume)