awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
rw₅ rw₆ : n ^ j ∣ n ^ j
⊢ n ^ j • u j = 0

Tactic:
rw [← addOrderOf_dvd_iff_zsmul_eq_zero, hu₀, Int.natCast_pow, Int.natCast_natAbs, ← abs_pow,
          abs_dvd]

Premises used: abs_dvd, Int.natCast_pow, addOrderOf_dvd_iff_zsmul_eq_zero, abs_pow, Int.natCast_natAbs
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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

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]
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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 : ℕ
rw rw₁ : s =ᶠ[ae (F := Measure (AddCircle T)) volume] s
⊢ u j +ᵥ s =ᶠ[ae (F := Measure (AddCircle T)) volume] s

Tactic:
rw [vadd_eq_self_of_preimage_zsmul_eq_self hs' (hnu j)]

Premises used: vadd_eq_self_of_preimage_zsmul_eq_self
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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

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)]
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
simp_rw : Tendsto (β := ℕ) (fun (j : ℕ) ↦ n.natAbs ^ j) atTop atTop
⊢ Tendsto (β := ℕ) (fun (j : ℕ) ↦ addOrderOf (u j)) atTop atTop

Tactic:
simp_rw [hu₀]
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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 : ℕ) ↦ n.natAbs ^ j) atTop atTop

Tactic:
tendsto_pow_atTop_atTop_of_one_lt hn

Premises used: tendsto_pow_atTop_atTop_of_one_lt
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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 : ℕ) ↦ n.natAbs ^ j) atTop atTop

Tactic:
exact tendsto_pow_atTop_atTop_of_one_lt hn

Premises used: tendsto_pow_atTop_atTop_of_one_lt
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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

Tactic:
have hu₂ : Tendsto (fun j => addOrderOf <| u j) atTop atTop := by
        simp_rw [hu₀]; exact tendsto_pow_atTop_atTop_of_one_lt hn
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
rw :
  s =ᶠ[ae (F := autoParam (Measure (AddCircle T)) PreErgodic._auto_1) volume] ∅ ∨
    s =ᶠ[ae (F := autoParam (Measure (AddCircle T)) PreErgodic._auto_1) volume] univ
⊢ EventuallyConst s (ae (F := autoParam (Measure (AddCircle T)) PreErgodic._auto_1) volume)

Tactic:
rw [eventuallyConst_set']

Premises used: Filter.eventuallyConst_set'
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
⊢ s =ᶠ[ae (F := autoParam (Measure (AddCircle T)) PreErgodic._auto_1) volume] ∅ ∨
    s =ᶠ[ae (F := autoParam (Measure (AddCircle T)) PreErgodic._auto_1) volume] univ

Tactic:
ae_empty_or_univ_of_forall_vadd_ae_eq_self hs.nullMeasurableSet hu₁ hu₂

Premises used: AddCircle.ae_empty_or_univ_of_forall_vadd_ae_eq_self, MeasurableSet.nullMeasurableSet
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
⊢ s =ᶠ[ae (F := autoParam (Measure (AddCircle T)) PreErgodic._auto_1) volume] ∅ ∨
    s =ᶠ[ae (F := autoParam (Measure (AddCircle T)) PreErgodic._auto_1) volume] univ

Tactic:
exact ae_empty_or_univ_of_forall_vadd_ae_eq_self hs.nullMeasurableSet hu₁ hu₂

Premises used: AddCircle.ae_empty_or_univ_of_forall_vadd_ae_eq_self, MeasurableSet.nullMeasurableSet
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
n : ℕ
hn : 1 < n
⊢ LT.lt (α := ℤ) 1 |(↑n : ℤ)|

Tactic:
simp [hn]
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
Goal:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
set :
  let f : AddCircle T → AddCircle T := fun (y : AddCircle T) ↦ n • y + x;
  Ergodic (m := MeasureSpace.toMeasurableSpace) f volume
⊢ Ergodic (m := MeasureSpace.toMeasurableSpace) (fun (y : AddCircle T) ↦ n • y + x) volume

Tactic:
set f : AddCircle T → AddCircle T := fun y => n • y + x

Premises used: HAdd.hAdd, HSMul.hSMul
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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))
⊢ 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)
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
rw : Ergodic (m := MeasureSpace.toMeasurableSpace) (fun (y : AddCircle T) ↦ n • y) volume
⊢ Ergodic (m := MeasureSpace.toMeasurableSpace) f volume

Tactic:
rw [← he.ergodic_conjugate_iff, this]

Premises used: MeasureTheory.MeasurePreserving.ergodic_conjugate_iff
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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) (fun (y : AddCircle T) ↦ n • y) volume

Tactic:
ergodic_zsmul h

Premises used: AddCircle.ergodic_zsmul
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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) (fun (y : AddCircle T) ↦ n • y) volume

Tactic:
exact ergodic_zsmul h

Premises used: AddCircle.ergodic_zsmul
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
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
⊢ Ergodic (m := MeasureSpace.toMeasurableSpace) f volume

Tactic:
suffices e ∘ f ∘ e.symm = fun y => n • y by
    rw [← he.ergodic_conjugate_iff, this]; exact ergodic_zsmul h
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
⊢ |1| < |n|

Tactic:
rw [← abs_one] at h

Premises used: abs_one
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
h₁ : |1| < |n|
⊢ let e : AddCircle T ≃ᵐ AddCircle T :=
    MeasurableEquiv.addLeft
      (@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1));
  MeasurePreserving (α := AddCircle T) (β := AddCircle T) (⇑e : (a : AddCircle T) → AddCircle T) volume volume

Tactic:
rw [← abs_one] at h

Premises used: abs_one
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
rw : n ≠ 1
⊢ n - 1 ≠ 0

Tactic:
rw [sub_ne_zero]

Premises used: sub_ne_zero
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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

Tactic:
ne_of_apply_ne _ (ne_of_gt h)

Premises used: ne_of_gt, ne_of_apply_ne
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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

Tactic:
exact ne_of_apply_ne _ (ne_of_gt h)

Premises used: ne_of_gt, ne_of_apply_ne
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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

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)
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
a₁ : @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
| x + @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)

Tactic:
congr
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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 : (n - 1) • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
| x

Tactic:
rw [← DivisibleBy.div_cancel x h]

Premises used: DivisibleBy.div_cancel
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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 : (n - 1) • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
a₁ : @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
| x + @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)

Tactic:
congr; rw [← DivisibleBy.div_cancel x h]

Premises used: DivisibleBy.div_cancel
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
conv_rhs :
  n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) =
    (n - 1) • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) +
      @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
⊢ n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) =
    x + @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)

Tactic:
conv_rhs => congr; rw [← DivisibleBy.div_cancel x h]

Premises used: DivisibleBy.div_cancel
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
rw :
  n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) =
    n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) -
        HSMul.hSMul (α := ℤ) 1
          (@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)) +
      @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
rw₁ :
  n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) =
    n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) -
        @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) +
      @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
rw₂ rw₃ :
  n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) =
    n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
⊢ n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) =
    (n - 1) • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) +
      @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)

Tactic:
rw [sub_smul, one_smul, sub_add_cancel]

Premises used: sub_smul, one_smul, sub_add_cancel
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
⊢ n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) =
    x + @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)

Tactic:
have hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1) := by
    conv_rhs => congr; rw [← DivisibleBy.div_cancel x h]
    rw [sub_smul, one_smul, sub_add_cancel]
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
hnx :
  n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) =
    x + @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
h₁ :
  ∀ (y : AddCircle T),
    ((⇑e : (a : AddCircle T) → AddCircle T) ∘ f ∘ (⇑e.symm : (a : AddCircle T) → AddCircle T)) y = n • y
⊢ 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:
ext y
-- Module: Mathlib.Dynamics.Ergodic.AddCircle
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
hnx :
  n • @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) =
    x + @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1)
y : AddCircle T
h₁ :
  @DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) +
      (-@DivisibleBy.div _ _ SubNegMonoid.toAddMonoid SubNegMonoid.toZSMul MulZeroClass.toZero _ x (n - 1) + -x +
          n • y +
        x) =
    n • y
⊢ ((⇑e : (a : AddCircle T) → AddCircle T) ∘ f ∘ (⇑e.symm : (a : AddCircle T) → AddCircle T)) y = n • y

Tactic:
simp only [f, e, hnx, MeasurableEquiv.coe_addLeft, MeasurableEquiv.symm_addLeft, comp_apply,
    smul_add, zsmul_neg', neg_smul, neg_add_rev]

Premises used: neg_add_rev, neg_smul, MeasurableEquiv.symm_addLeft, MeasurableEquiv.coe_addLeft, Function.comp_apply, zsmul_neg', smul_add