-- Mathlib/Dynamics/Ergodic/Action/OfMinimal.lean
theorem preErgodic_of_dense_iUnion_preimage_one
    {μ : Measure G} [IsFiniteMeasure μ] [μ.InnerRegular] [μ.IsMulLeftInvariant]
    (f : G →* G) (hf : Dense (⋃ n, f^[n] ⁻¹' 1)) : PreErgodic f μ

Proof state:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
n : ℕ
x : G
hx : x ∈ (⇑f)^[n] ⁻¹' 1
⊢ x ∈ {g | (fun x => g • x) ⁻¹' s = s}

Tactic:
have hsn : f^[n] ⁻¹' s = s := by
  rw [preimage_iterate_eq, iterate_fixed hs]

Result:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
n : ℕ
x : G
hx : x ∈ (⇑f)^[n] ⁻¹' 1
hsn : (⇑f)^[n] ⁻¹' s = s
⊢ x ∈ {g | (fun x => g • x) ⁻¹' s = s}

Proof state:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
n : ℕ
x : G
hx : (⇑f)^[n] x = 1
hsn : (⇑f)^[n] ⁻¹' s = s
⊢ (fun x_1 => x • x_1) ⁻¹' ((⇑f)^[n] ⁻¹' s) = (⇑f)^[n] ⁻¹' s

Tactic:
ext y

Result:
case h
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
n : ℕ
x : G
hx : (⇑f)^[n] x = 1
hsn : (⇑f)^[n] ⁻¹' s = s
y : G
⊢ y ∈ (fun x_1 => x • x_1) ⁻¹' ((⇑f)^[n] ⁻¹' s) ↔ y ∈ (⇑f)^[n] ⁻¹' s

Proof state:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
n : ℕ
x : G
hx : x ∈ (⇑f)^[n] ⁻¹' 1
⊢ (⇑f)^[n] ⁻¹' s = s

Tactic:
rw [preimage_iterate_eq, iterate_fixed hs]

Result:
no goals

Proof state:
case h
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
n : ℕ
x : G
hx : (⇑f)^[n] x = 1
hsn : (⇑f)^[n] ⁻¹' s = s
y : G
⊢ y ∈ (fun x_1 => x • x_1) ⁻¹' ((⇑f)^[n] ⁻¹' s) ↔ y ∈ (⇑f)^[n] ⁻¹' s

Tactic:
simp [hx]

Result:
no goals

Proof state:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
n : ℕ
x : G
hx : (⇑f)^[n] x = 1
hsn : (⇑f)^[n] ⁻¹' s = s
⊢ x ∈ {g | (fun x => g • x) ⁻¹' s = s}

Tactic:
rw [mem_setOf, ← hsn]

Result:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
n : ℕ
x : G
hx : (⇑f)^[n] x = 1
hsn : (⇑f)^[n] ⁻¹' s = s
⊢ (fun x_1 => x • x_1) ⁻¹' ((⇑f)^[n] ⁻¹' s) = (⇑f)^[n] ⁻¹' s

Proof state:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
⊢ PreErgodic (⇑f) μ

Tactic:
refine ⟨fun s hsm hs ↦ aeconst_of_dense_setOf_preimage_smul_eq (M := G) hsm.nullMeasurableSet ?_⟩

Result:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
⊢ Dense {g | (fun x => g • x) ⁻¹' s = s}

Proof state:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
⊢ Dense {g | (fun x => g • x) ⁻¹' s = s}

Tactic:
refine hf.mono <| iUnion_subset fun n x hx ↦ ?_

Result:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
n : ℕ
x : G
hx : x ∈ (⇑f)^[n] ⁻¹' 1
⊢ x ∈ {g | (fun x => g • x) ⁻¹' s = s}

Proof state:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
n : ℕ
x : G
hx : x ∈ (⇑f)^[n] ⁻¹' 1
hsn : (⇑f)^[n] ⁻¹' s = s
⊢ x ∈ {g | (fun x => g • x) ⁻¹' s = s}

Tactic:
rw [mem_preimage, Set.mem_one] at hx

Result:
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : SecondCountableTopology G
inst✝⁴ : MeasurableSpace G
inst✝³ : BorelSpace G
μ : Measure G
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : μ.IsMulLeftInvariant
f : G →* G
hf : Dense (⋃ n, (⇑f)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : ⇑f ⁻¹' s = s
n : ℕ
x : G
hx : (⇑f)^[n] x = 1
hsn : (⇑f)^[n] ⁻¹' s = s
⊢ x ∈ {g | (fun x => g • x) ⁻¹' s = s}