-- 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
hsne : s.Nonempty
hd : Disjoint s (a • V)
⊢ ⋃ i, g⁻¹ • g ^ i • V = ⋃ m, g ^ m • V

Tactic:
refine iUnion_congr_of_surjective _ (add_left_surjective (-1)) fun m ↦ ?_

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

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.1 ×ˢ 𝓝 1.2) (𝓝 a)
⊢ ∃ V, 1 ∈ V ∧ IsOpen V ∧ ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y

Tactic:
simpa [(nhds_basis_opens (1 : G)).prod_self.mem_iff, prod_subset_iff, and_assoc] using this h

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

Tactic:
refine (hVo.smul a).measure_ne_zero μ (.image _ ⟨1, hV₁⟩) (measure_mono_null ?_ h)

Result:
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ᶜ

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

Tactic:
obtain ⟨V, hV₁, hVo, hV⟩ :
    ∃ V : Set G, 1 ∈ V ∧ IsOpen V ∧ ∀ x ∈ V, ∀ y ∈ V, ∀ m : ℤ, g ^ m ≠ a * x / y := by
  rw [← mem_compl_iff, ← interior_compl, mem_interior_iff_mem_nhds] at h
  have : Tendsto (fun (x, y) ↦ a * x / y) (𝓝 1) (𝓝 a) :=
    Continuous.tendsto' (by fun_prop) _ _ (by simp)
  rw [nhds_prod_eq] at this
  simpa [(nhds_basis_opens (1 : G)).prod_self.mem_iff, prod_subset_iff, and_assoc] using this h

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
⊢ 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
⊢ (match 1 with
    | (x, y) => a * x / y) =
    a

Tactic:
simp

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

Tactic:
have : Tendsto (fun (x, y) ↦ a * x / y) (𝓝 1) (𝓝 a) :=
  Continuous.tendsto' (by fun_prop) _ _ (by simp)

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) (𝓝 a)
⊢ ∃ V, 1 ∈ V ∧ IsOpen V ∧ ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y