-- Mathlib/Dynamics/Ergodic/AddCircle.lean
theorem ergodic_zsmul_add (x : AddCircle T) {n : ℤ} (h : 1 < |n|) : Ergodic fun y => n • y + x

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : |1| < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
⊢ n ≠ 1

Tactic:
exact ne_of_apply_ne _ (ne_of_gt h)

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1)
⊢ ⇑e ∘ f ∘ ⇑e.symm = fun y => n • y

Tactic:
ext y

Result:
case h
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1)
y : AddCircle T
⊢ (⇑e ∘ f ∘ ⇑e.symm) y = n • y

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
⊢ ⇑e ∘ f ∘ ⇑e.symm = fun y => n • y

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)

Result:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
⊢ ⇑e ∘ f ∘ ⇑e.symm = fun y => n • y

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
⊢ Ergodic f volume

Tactic:
suffices e ∘ f ∘ e.symm = fun y => n • y by
  rw [← he.ergodic_conjugate_iff, this]; exact ergodic_zsmul h

Result:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
⊢ ⇑e ∘ f ∘ ⇑e.symm = fun y => n • y

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
this : ⇑e ∘ f ∘ ⇑e.symm = fun y => n • y
⊢ Ergodic f volume

Tactic:
rw [← he.ergodic_conjugate_iff, this]

Result:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
this : ⇑e ∘ f ∘ ⇑e.symm = fun y => n • y
⊢ Ergodic (fun y => n • y) volume

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
⊢ n - 1 ≠ 0

Tactic:
rw [← abs_one] at h

Result:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : |1| < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
⊢ n - 1 ≠ 0

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
this : ⇑e ∘ f ∘ ⇑e.symm = fun y => n • y
⊢ Ergodic (fun y => n • y) volume

Tactic:
exact ergodic_zsmul h

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
⊢ Ergodic f volume

Tactic:
let e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x <| n - 1)

Result:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
⊢ Ergodic f volume

Proof state:
case h
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1)
y : AddCircle T
⊢ DivisibleBy.div x (n - 1) + (-DivisibleBy.div x (n - 1) + -x + n • y + x) = n • y

Tactic:
abel

Result:
no goals

Proof state:
case h
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1)
y : AddCircle T
⊢ (⇑e ∘ f ∘ ⇑e.symm) 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]

Result:
case h
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
hnx : n • DivisibleBy.div x (n - 1) = x + DivisibleBy.div x (n - 1)
y : AddCircle T
⊢ DivisibleBy.div x (n - 1) + (-DivisibleBy.div x (n - 1) + -x + n • y + x) = n • y

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
h : n - 1 ≠ 0
⊢ n • DivisibleBy.div x (n - 1) = (n - 1) • DivisibleBy.div x (n - 1) + DivisibleBy.div x (n - 1)

Tactic:
rw [sub_smul, one_smul, sub_add_cancel]

Result:
no goals

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : |1| < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
⊢ n - 1 ≠ 0

Tactic:
rw [sub_ne_zero]

Result:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : |1| < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
⊢ n ≠ 1

Proof state:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
⊢ Ergodic f volume

Tactic:
have he : MeasurePreserving e volume volume :=
  measurePreserving_add_left volume (DivisibleBy.div x <| n - 1)

Result:
T : ℝ
hT : Fact (0 < T)
x : AddCircle T
n : ℤ
h : 1 < |n|
f : AddCircle T → AddCircle T := fun y => n • y + x
e : AddCircle T ≃ᵐ AddCircle T := MeasurableEquiv.addLeft (DivisibleBy.div x (n - 1))
he : MeasurePreserving (⇑e) volume volume
⊢ Ergodic f volume