-- Mathlib/Dynamics/Ergodic/Action/Basic.lean
theorem ergodicSMul_iterateMulAct {f : α → α} (hf : Measurable f) :
    ErgodicSMul (IterateMulAct f) α μ ↔ Ergodic f μ

Proof state:
case refine_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
x✝ :
  MeasurePreserving f μ μ ∧
    ∀ {s : Set α},
      MeasurableSet s → (∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)
h₁ : MeasurePreserving f μ μ
h₂ :
  ∀ {s : Set α},
    MeasurableSet s → (∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)
s : Set α
hm : MeasurableSet s
hs : f ⁻¹' s = s
n : IterateMulAct f
⊢ (fun x => n • x) ⁻¹' s =ᶠ[ae μ] f^[n.val] ⁻¹' s

Tactic:
rfl

Result:
no goals

Proof state:
case refine_2
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
h : Ergodic f μ
⊢ ∀ {s : Set α},
    MeasurableSet s → (∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)

Tactic:
intro s hm hs

Result:
case refine_2
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
h : Ergodic f μ
s : Set α
hm : MeasurableSet s
hs : ∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s
⊢ EventuallyConst s (ae μ)

Proof state:
case refine_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
x✝ :
  MeasurePreserving f μ μ ∧
    ∀ {s : Set α},
      MeasurableSet s → (∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)
h₁ : MeasurePreserving f μ μ
h₂ :
  ∀ {s : Set α},
    MeasurableSet s → (∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)
⊢ ∀ ⦃s : Set α⦄, MeasurableSet s → f ⁻¹' s = s → EventuallyConst s (ae μ)

Tactic:
intro s hm hs

Result:
case refine_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
x✝ :
  MeasurePreserving f μ μ ∧
    ∀ {s : Set α},
      MeasurableSet s → (∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)
h₁ : MeasurePreserving f μ μ
h₂ :
  ∀ {s : Set α},
    MeasurableSet s → (∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)
s : Set α
hm : MeasurableSet s
hs : f ⁻¹' s = s
⊢ EventuallyConst s (ae μ)

Proof state:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
⊢ ErgodicSMul (IterateMulAct f) α μ ↔ Ergodic f μ

Tactic:
simp only [ergodicSMul_iff, smulInvariantMeasure_iterateMulAct, hf]

Result:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
⊢ (MeasurePreserving f μ μ ∧
      ∀ {s : Set α},
        MeasurableSet s → (∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)) ↔
    Ergodic f μ

Proof state:
case refine_2
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
h : Ergodic f μ
s : Set α
hm : MeasurableSet s
hs : ∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s
⊢ EventuallyConst s (ae μ)

Tactic:
exact h.quasiErgodic.aeconst_set₀ hm.nullMeasurableSet <| hs (.mk 1)

Result:
no goals

Proof state:
case refine_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
x✝ :
  MeasurePreserving f μ μ ∧
    ∀ {s : Set α},
      MeasurableSet s → (∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)
h₁ : MeasurePreserving f μ μ
h₂ :
  ∀ {s : Set α},
    MeasurableSet s → (∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)
s : Set α
hm : MeasurableSet s
hs : f ⁻¹' s = s
n : IterateMulAct f
⊢ (fun x => n • x) ⁻¹' s =ᶠ[ae μ] s

Tactic:
nth_rewrite 2 [← Function.IsFixedPt.preimage_iterate hs n.val]

Result:
case refine_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
x✝ :
  MeasurePreserving f μ μ ∧
    ∀ {s : Set α},
      MeasurableSet s → (∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)
h₁ : MeasurePreserving f μ μ
h₂ :
  ∀ {s : Set α},
    MeasurableSet s → (∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)
s : Set α
hm : MeasurableSet s
hs : f ⁻¹' s = s
n : IterateMulAct f
⊢ (fun x => n • x) ⁻¹' s =ᶠ[ae μ] f^[n.val] ⁻¹' s

Proof state:
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
⊢ (MeasurePreserving f μ μ ∧
      ∀ {s : Set α},
        MeasurableSet s → (∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)) ↔
    Ergodic f μ

Tactic:
refine ⟨fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ⟨?_⟩⟩, fun h ↦ ⟨h.1, ?_⟩⟩

Result:
case refine_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
x✝ :
  MeasurePreserving f μ μ ∧
    ∀ {s : Set α},
      MeasurableSet s → (∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)
h₁ : MeasurePreserving f μ μ
h₂ :
  ∀ {s : Set α},
    MeasurableSet s → (∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)
⊢ ∀ ⦃s : Set α⦄, MeasurableSet s → f ⁻¹' s = s → EventuallyConst s (ae μ)

case refine_2
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
h : Ergodic f μ
⊢ ∀ {s : Set α},
    MeasurableSet s → (∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)

Proof state:
case refine_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
x✝ :
  MeasurePreserving f μ μ ∧
    ∀ {s : Set α},
      MeasurableSet s → (∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)
h₁ : MeasurePreserving f μ μ
h₂ :
  ∀ {s : Set α},
    MeasurableSet s → (∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)
s : Set α
hm : MeasurableSet s
hs : f ⁻¹' s = s
⊢ EventuallyConst s (ae μ)

Tactic:
refine h₂ hm fun n ↦ ?_

Result:
case refine_1
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → α
hf : Measurable f
x✝ :
  MeasurePreserving f μ μ ∧
    ∀ {s : Set α},
      MeasurableSet s → (∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)
h₁ : MeasurePreserving f μ μ
h₂ :
  ∀ {s : Set α},
    MeasurableSet s → (∀ (g : IterateMulAct f), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s) → EventuallyConst s (ae μ)
s : Set α
hm : MeasurableSet s
hs : f ⁻¹' s = s
n : IterateMulAct f
⊢ (fun x => n • x) ⁻¹' s =ᶠ[ae μ] s