-- Mathlib/Dynamics/Ergodic/Action/OfMinimal.lean
theorem DenseRange.zpow_of_ergodic_mul_left [OpensMeasurableSpace G]
    {μ : Measure G} [μ.IsOpenPosMeasure] {g : G} (hg : Ergodic (g * ·) μ) :
    DenseRange (g ^ · : ℤ → G)

Proof state:
case intro.intro.intro
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x => g * x) μ
a : G
h : a ∉ closure (range fun x => g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen s
hsne : s.Nonempty
hd : Disjoint s (a • V)
hgs : (fun x => g * x) ⁻¹' s = s
⊢ False

Tactic:
cases hg.measure_self_or_compl_eq_zero hso.measurableSet hgs with
| inl h => exact hso.measure_ne_zero _ hsne h
| inr h =>
  refine (hVo.smul a).measure_ne_zero μ (.image _ ⟨1, hV₁⟩) (measure_mono_null ?_ h)
  rwa [disjoint_right] at hd

Result:
no goals

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x => g * x) μ
a : G
h : a ∉ closure (range fun x => g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen s
hsne : s.Nonempty
m : ℤ
x : G
hx : x ∈ V
y : G
hy : y ∈ V
hxy : (fun x => a • x) y = (fun x => g ^ m • x) x
⊢ False

Tactic:
apply hV y hy x hx m

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x => g * x) μ
a : G
h : a ∉ closure (range fun x => g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen s
hsne : s.Nonempty
m : ℤ
x : G
hx : x ∈ V
y : G
hy : y ∈ V
hxy : (fun x => a • x) y = (fun x => g ^ m • x) x
⊢ g ^ m = a * y / x

Proof state:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x => g * x) μ
a : G
h : (range fun x => g ^ x)ᶜ ∈ 𝓝 a
this :
  Tendsto
    (fun x =>
      match x with
      | (x, y) => a * x / y)
    (𝓝 1) (𝓝 a)
⊢ ∃ V, 1 ∈ V ∧ IsOpen V ∧ ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y

Tactic:
rw [nhds_prod_eq] at this

Result:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x => g * x) μ
a : G
h : (range fun x => g ^ x)ᶜ ∈ 𝓝 a
this :
  Tendsto
    (fun x =>
      match x with
      | (x, y) => a * x / y)
    (𝓝 1.1 ×ˢ 𝓝 1.2) (𝓝 a)
⊢ ∃ V, 1 ∈ V ∧ IsOpen V ∧ ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x => g * x) μ
a : G
h : a ∉ closure (range fun x => g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen s
hsne : s.Nonempty
m : ℤ
x : G
hx : x ∈ V
y : G
hy : y ∈ V
hxy : (fun x => a • x) y = (fun x => g ^ m • x) x
⊢ g ^ m = a * y / x

Tactic:
simp_all

Result:
no goals

Proof state:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x => g * x) μ
⊢ DenseRange fun x => g ^ x

Tactic:
intro a

Result:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x => g * x) μ
a : G
⊢ a ∈ closure (range fun x => g ^ x)

Proof state:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x => g * x) μ
a : G
⊢ a ∈ closure (range fun x => g ^ x)

Tactic:
by_contra h

Result:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x => g * x) μ
a : G
h : a ∉ closure (range fun x => g ^ x)
⊢ False

Proof state:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x => g * x) μ
a : G
h : a ∉ closure (range fun x => g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen s
hsne : s.Nonempty
hd : Disjoint s (a • V)
⊢ (fun x => g * x) ⁻¹' s = s

Tactic:
simp only [s, preimage_iUnion, ← smul_eq_mul, preimage_smul]

Result:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x => g * x) μ
a : G
h : a ∉ closure (range fun x => g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen s
hsne : s.Nonempty
hd : Disjoint s (a • V)
⊢ ⋃ i, g⁻¹ • g ^ i • V = ⋃ m, g ^ m • V

Proof state:
case intro.intro.intro
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x => g * x) μ
a : G
h : a ∉ closure (range fun x => g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
⊢ False

Tactic:
set s := ⋃ m : ℤ, g ^ m • V

Result:
case intro.intro.intro
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x => g * x) μ
a : G
h : a ∉ closure (range fun x => g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
⊢ False

Proof state:
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x => g * x) μ
a : G
h : (range fun x => g ^ x)ᶜ ∈ 𝓝 a
⊢ Continuous fun x =>
    match x with
    | (x, y) => a * x / y

Tactic:
fun_prop

Result:
no goals

Proof state:
case intro.intro.intro.inr
G : Type u_1
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : IsTopologicalGroup G
inst✝² : MeasurableSpace G
inst✝¹ : OpensMeasurableSpace G
μ : Measure G
inst✝ : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun x => g * x) μ
a : G
h✝ : a ∉ closure (range fun x => g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen s
hsne : s.Nonempty
hd : Disjoint s (a • V)
hgs : (fun x => g * x) ⁻¹' s = s
h : μ sᶜ = 0
⊢ a • V ⊆ sᶜ

Tactic:
rwa [disjoint_right] at hd

Result:
no goals