-- 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:
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
⊢ 1 ∈ g ^ 0 • V

Tactic:
simpa

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) μ
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
⊢ ∀ (i : ℤ) ⦃a_1 : G⦄, a_1 ∈ g ^ i • V → a_1 ∉ a • V

Tactic:
rintro m _ ⟨x, hx, rfl⟩ ⟨y, hy, hxy⟩

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
⊢ 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
⊢ Disjoint s (a • V)

Tactic:
simp_rw [s, disjoint_iUnion_left, disjoint_left]

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
⊢ ∀ (i : ℤ) ⦃a_1 : G⦄, a_1 ∈ g ^ i • V → a_1 ∉ a • 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
s : Set G := ⋃ m, g ^ m • V
hso : IsOpen s
⊢ False

Tactic:
have hsne : s.Nonempty := ⟨1, mem_iUnion.2 ⟨0, by simpa⟩⟩

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
hso : IsOpen s
hsne : s.Nonempty
⊢ False

Proof state:
case intro.intro.intro.inl
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
⊢ False

Tactic:
exact hso.measure_ne_zero _ hsne h

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) μ
a : G
h : a ∉ closure (range fun x => g ^ x)
⊢ ∃ V, 1 ∈ V ∧ IsOpen V ∧ ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y

Tactic:
rw [← mem_compl_iff, ← interior_compl, mem_interior_iff_mem_nhds] at 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 : (range fun x => g ^ x)ᶜ ∈ 𝓝 a
⊢ ∃ V, 1 ∈ V ∧ IsOpen V ∧ ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y

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
⊢ False

Tactic:
have hd : Disjoint s (a • V) := by
  simp_rw [s, disjoint_iUnion_left, disjoint_left]
  rintro m _ ⟨x, hx, rfl⟩ ⟨y, hy, hxy⟩
  apply hV y hy x hx m
  simp_all

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
hso : IsOpen s
hsne : s.Nonempty
hd : Disjoint s (a • V)
⊢ False

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
⊢ False

Tactic:
have hso : IsOpen s := isOpen_iUnion fun m ↦ hVo.smul _

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
hso : IsOpen s
⊢ 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)
m : ℤ
⊢ g ^ (-1 + m) • V = g⁻¹ • g ^ m • V

Tactic:
simp [zpow_add, mul_smul]

Result:
no goals