awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : OpensMeasurableSpace G
μ : Measure G
inst_5 : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun (x : G) ↦ g * x) μ
a : G
h : (range fun (x : ℤ) ↦ g ^ x)ᶜ ∈ 𝓝 a
this :
  Tendsto
    (fun (x : G × G) ↦
      match (motive := G × G → G) x with
      | (x, y) => a * x / y)
    (𝓝 1) (𝓝 a)
⊢ Tendsto
    (fun (x : G × G) ↦
      match (motive := G × G → G) x with
      | (x, y) => a * x / y)
    (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1.1) (𝓝 1.2)) (𝓝 a)

Tactic:
rw [nhds_prod_eq] at this

Premises used: nhds_prod_eq
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : OpensMeasurableSpace G
μ : Measure G
inst_5 : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun (x : G) ↦ g * x) μ
a : G
h : (range fun (x : ℤ) ↦ g ^ x)ᶜ ∈ 𝓝 a
this :
  Tendsto
    (fun (x : G × G) ↦
      match (motive := G × G → G) x with
      | (x, y) => a * x / y)
    (SProd.sprod (α := Filter G) (β := Filter G) (𝓝 1.1) (𝓝 1.2)) (𝓝 a)
⊢ ∃ (V : Set G), 1 ∈ V ∧ IsOpen[inst_1] 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

Premises used: Filter.HasBasis.mem_iff, Filter.HasBasis.prod_self, Set.prod_subset_iff, and_assoc, nhds_basis_opens, OfNat.ofNat
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : OpensMeasurableSpace G
μ : Measure G
inst_5 : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun (x : G) ↦ g * x) μ
a : G
h : a ∉ closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)
obtain :
  ∀ (V : Set G) (hV₁ : 1 ∈ V) (hVo : IsOpen[inst_1] V) (hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y), False
⊢ 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

Premises used: Set
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : OpensMeasurableSpace G
μ : Measure G
inst_5 : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun (x : G) ↦ g * x) μ
a : G
h : a ∉ closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst_1] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ (m : ℤ), g ^ m • V
⊢ IsOpen[inst_1] s

Tactic:
have hso : IsOpen s := isOpen_iUnion fun m ↦ hVo.smul _
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : OpensMeasurableSpace G
μ : Measure G
inst_5 : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun (x : G) ↦ g * x) μ
a : G
h : a ∉ closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst_1] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ (m : ℤ), g ^ m • V
hso : IsOpen[inst_1] s
⊢ 1 ∈ HPow.hPow (β := ℤ) g 0 • V

Tactic:
simpa
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : OpensMeasurableSpace G
μ : Measure G
inst_5 : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun (x : G) ↦ g * x) μ
a : G
h : a ∉ closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst_1] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ (m : ℤ), g ^ m • V
hso : IsOpen[inst_1] s
⊢ s.Nonempty

Tactic:
have hsne : s.Nonempty := ⟨1, mem_iUnion.2 ⟨0, by simpa⟩⟩
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : OpensMeasurableSpace G
μ : Measure G
inst_5 : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun (x : G) ↦ g * x) μ
a : G
h : a ∉ closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst_1] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ (m : ℤ), g ^ m • V
hso : IsOpen[inst_1] s
hsne : s.Nonempty
simp_rw : ∀ (i : ℤ) ⦃a_1 : G⦄, a_1 ∈ g ^ i • V → a_1 ∉ a • V
⊢ Disjoint s (a • V)

Tactic:
simp_rw [s, disjoint_iUnion_left, disjoint_left]

Premises used: Set.disjoint_left, Set.disjoint_iUnion_left
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : OpensMeasurableSpace G
μ : Measure G
inst_5 : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun (x : G) ↦ g * x) μ
a : G
h : a ∉ closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst_1] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ (m : ℤ), g ^ m • V
hso : IsOpen[inst_1] s
hsne : s.Nonempty
m : ℤ
x : G
hx : x ∈ V
y : G
hy : y ∈ V
hxy : Eq.{u_1 + 1} (α := G) ((fun (x : G) ↦ a • x) y) ((fun (x : G) ↦ g ^ m • x) x)
apply : g ^ m = a * y / x
⊢ False

Tactic:
apply hV y hy x hx m
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : OpensMeasurableSpace G
μ : Measure G
inst_5 : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun (x : G) ↦ g * x) μ
a : G
h : a ∉ closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst_1] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ (m : ℤ), g ^ m • V
hso : IsOpen[inst_1] s
hsne : s.Nonempty
m : ℤ
x : G
hx : x ∈ V
y : G
hy : y ∈ V
hxy : Eq.{u_1 + 1} (α := G) ((fun (x : G) ↦ a • x) y) ((fun (x : G) ↦ g ^ m • x) x)
⊢ g ^ m = a * y / x

Tactic:
simp_all
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : OpensMeasurableSpace G
μ : Measure G
inst_5 : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun (x : G) ↦ g * x) μ
a : G
h : a ∉ closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst_1] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ (m : ℤ), g ^ m • V
hso : IsOpen[inst_1] s
hsne : s.Nonempty
⊢ Disjoint s (a • V)

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
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : OpensMeasurableSpace G
μ : Measure G
inst_5 : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun (x : G) ↦ g * x) μ
a : G
h : a ∉ closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst_1] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ (m : ℤ), g ^ m • V
hso : IsOpen[inst_1] s
hsne : s.Nonempty
hd : Disjoint s (a • V)
simp : Eq.{u_1 + 1} (α := Set G) (⋃ (i : ℤ), g⁻¹ • g ^ i • V) (⋃ (m : ℤ), g ^ m • V)
⊢ (fun (x : G) ↦ g * x) ⁻¹' s = s

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

Premises used: Set.preimage_smul, Set.preimage_iUnion, smul_eq_mul
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : OpensMeasurableSpace G
μ : Measure G
inst_5 : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun (x : G) ↦ g * x) μ
a : G
h : a ∉ closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst_1] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ (m : ℤ), g ^ m • V
hso : IsOpen[inst_1] s
hsne : s.Nonempty
hd : Disjoint s (a • V)
⊢ Eq.{u_1 + 1} (α := Set G) (⋃ (i : ℤ), g⁻¹ • g ^ i • V) (⋃ (m : ℤ), g ^ m • V)

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

Premises used: Set.iUnion_congr_of_surjective, add_left_surjective, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : OpensMeasurableSpace G
μ : Measure G
inst_5 : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun (x : G) ↦ g * x) μ
a : G
h : a ∉ closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst_1] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ (m : ℤ), g ^ m • V
hso : IsOpen[inst_1] s
hsne : s.Nonempty
hd : Disjoint s (a • V)
refine : ∀ (m : ℤ), g ^ (-1 + m) • V = g⁻¹ • g ^ m • V
⊢ Eq.{u_1 + 1} (α := Set G) (⋃ (i : ℤ), g⁻¹ • g ^ i • V) (⋃ (m : ℤ), g ^ m • V)

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

Premises used: Set.iUnion_congr_of_surjective, add_left_surjective, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : OpensMeasurableSpace G
μ : Measure G
inst_5 : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun (x : G) ↦ g * x) μ
a : G
h : a ∉ closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst_1] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ (m : ℤ), g ^ m • V
hso : IsOpen[inst_1] s
hsne : s.Nonempty
hd : Disjoint s (a • V)
m : ℤ
⊢ g ^ (-1 + m) • V = g⁻¹ • g ^ m • V

Tactic:
simp [zpow_add, mul_smul]

Premises used: zpow_add, SemigroupAction.mul_smul
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : OpensMeasurableSpace G
μ : Measure G
inst_5 : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun (x : G) ↦ g * x) μ
a : G
h : a ∉ closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst_1] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ (m : ℤ), g ^ m • V
hso : IsOpen[inst_1] s
hsne : s.Nonempty
hd : Disjoint s (a • V)
⊢ (fun (x : G) ↦ g * x) ⁻¹' s = s

Tactic:
have hgs : (g * ·) ⁻¹' s = s := by
    simp only [s, preimage_iUnion, ← smul_eq_mul, preimage_smul]
    refine iUnion_congr_of_surjective _ (add_left_surjective (-1)) fun m ↦ ?_
    simp [zpow_add, mul_smul]
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : OpensMeasurableSpace G
μ : Measure G
inst_5 : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun (x : G) ↦ g * x) μ
a : G
h_1 : a ∉ closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst_1] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ (m : ℤ), g ^ m • V
hso : IsOpen[inst_1] s
hsne : s.Nonempty
hd : Disjoint s (a • V)
hgs : (fun (x : G) ↦ g * x) ⁻¹' s = s
h : Eq (α := ENNReal) ((μ : (a : Set G) → ENNReal) s : ENNReal) (0 : ENNReal)
⊢ False

Tactic:
hso.measure_ne_zero _ hsne h

Premises used: IsOpen.measure_ne_zero
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : OpensMeasurableSpace G
μ : Measure G
inst_5 : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun (x : G) ↦ g * x) μ
a : G
h_1 : a ∉ closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst_1] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ (m : ℤ), g ^ m • V
hso : IsOpen[inst_1] s
hsne : s.Nonempty
hd : Disjoint s (a • V)
hgs : (fun (x : G) ↦ g * x) ⁻¹' s = s
h : Eq (α := ENNReal) ((μ : (a : Set G) → ENNReal) s : ENNReal) (0 : ENNReal)
⊢ False

Tactic:
exact hso.measure_ne_zero _ hsne h

Premises used: IsOpen.measure_ne_zero
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : OpensMeasurableSpace G
μ : Measure G
inst_5 : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun (x : G) ↦ g * x) μ
a : G
h_1 : a ∉ closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst_1] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ (m : ℤ), g ^ m • V
hso : IsOpen[inst_1] s
hsne : s.Nonempty
hd : Disjoint s (a • V)
hgs : (fun (x : G) ↦ g * x) ⁻¹' s = s
h : Eq (α := ENNReal) ((μ : (a : Set G) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
⊢ False

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

Premises used: MeasureTheory.measure_mono_null, IsOpen.smul, Set.Nonempty.image, Exists.intro, OfNat.ofNat, IsOpen.measure_ne_zero
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : OpensMeasurableSpace G
μ : Measure G
inst_5 : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun (x : G) ↦ g * x) μ
a : G
h_1 : a ∉ closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst_1] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ (m : ℤ), g ^ m • V
hso : IsOpen[inst_1] s
hsne : s.Nonempty
hd : Disjoint s (a • V)
hgs : (fun (x : G) ↦ g * x) ⁻¹' s = s
h : Eq (α := ENNReal) ((μ : (a : Set G) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
inr : a • V ⊆ sᶜ
⊢ False

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

Premises used: MeasureTheory.measure_mono_null, IsOpen.smul, Set.Nonempty.image, Exists.intro, OfNat.ofNat, IsOpen.measure_ne_zero
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : OpensMeasurableSpace G
μ : Measure G
inst_5 : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun (x : G) ↦ g * x) μ
a : G
h_1 : a ∉ closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst_1] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ (m : ℤ), g ^ m • V
hso : IsOpen[inst_1] s
hsne : s.Nonempty
hd : Disjoint s (a • V)
hgs : (fun (x : G) ↦ g * x) ⁻¹' s = s
h : Eq (α := ENNReal) ((μ : (a : Set G) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)
inr inr₁ inr₂ inr₃ :
  ∀ (hd : ∀ ⦃a_1 : G⦄, a_1 ∈ a • V → a_1 ∉ s) (hgs : (fun (x : G) ↦ g * x) ⁻¹' s = s)
    (h : Eq (α := ENNReal) ((μ : (a : Set G) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)), a • V ⊆ sᶜ
⊢ a • V ⊆ sᶜ

Tactic:
rwa [disjoint_right] at hd

Premises used: Set.disjoint_right
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : OpensMeasurableSpace G
μ : Measure G
inst_5 : μ.IsOpenPosMeasure
g : G
hg : Ergodic (fun (x : G) ↦ g * x) μ
a : G
h : a ∉ closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)
V : Set G
hV₁ : 1 ∈ V
hVo : IsOpen[inst_1] V
hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
s : Set G := ⋃ (m : ℤ), g ^ m • V
hso : IsOpen[inst_1] s
hsne : s.Nonempty
hd : Disjoint s (a • V)
hgs : (fun (x : G) ↦ g * x) ⁻¹' s = s
⊢ Eq (α := ENNReal) ((μ : (a : Set G) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((μ : (a : Set G) → ENNReal) sᶜ : ENNReal) (0 : ENNReal)

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

Premises used: Set.disjoint_right, PreErgodic.measure_self_or_compl_eq_zero, IsOpen.measurableSet, Ergodic.toPreErgodic
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : SecondCountableTopology G
inst_5 : BorelSpace G
g : G
hg : DenseRange.{u_1, 0} (X := G) fun (x : ℕ) ↦ g ^ x
μ : Measure G
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
inst_8 : μ.IsMulLeftInvariant
⊢ Ergodic (fun (x : G) ↦ g * x) μ

Tactic:
ergodic_smul_of_denseRange_pow hg μ

Premises used: ergodic_smul_of_denseRange_pow
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : SecondCountableTopology G
inst_5 : BorelSpace G
g : G
hg : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ g ^ x
μ : Measure G
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
inst_8 : μ.IsMulLeftInvariant
⊢ Ergodic (fun (x : G) ↦ g * x) μ

Tactic:
ergodic_smul_of_denseRange_zpow hg μ

Premises used: ergodic_smul_of_denseRange_zpow
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : MeasurableSpace G
inst_4 : SecondCountableTopology G
inst_5 : BorelSpace G
g : G
μ : Measure G
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
inst_8 : μ.IsMulLeftInvariant
inst_9 : NeZero μ
⊢ Ergodic (fun (x : G) ↦ g * x) μ ↔ DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ g ^ x

Tactic:
⟨.zpow_of_ergodic_mul_left, (ergodic_mul_left_of_denseRange_zpow · μ)⟩

Premises used: DenseRange.zpow_of_ergodic_mul_left, ergodic_mul_left_of_denseRange_zpow, Iff.intro
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : SecondCountableTopology G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
inst_8 : μ.IsMulLeftInvariant
f : G →* G
hf : Dense.{u_1} (X := G) (⋃ (n : ℕ), (⇑f : (a : G) → G)^[n] ⁻¹' 1)
⊢ PreErgodic (⇑f : (a : G) → G) μ

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

Premises used: MeasurableSet.nullMeasurableSet, aeconst_of_dense_setOf_preimage_smul_eq, PreErgodic.mk
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : SecondCountableTopology G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
inst_8 : μ.IsMulLeftInvariant
f : G →* G
hf : Dense.{u_1} (X := G) (⋃ (n : ℕ), (⇑f : (a : G) → G)^[n] ⁻¹' 1)
refine :
  ∀ (s : Set G) (hsm : MeasurableSet s) (hs : (⇑f : (a : G) → G) ⁻¹' s = s),
    Dense.{u_1} (X := G) {g : G | (fun (x : G) ↦ g • x) ⁻¹' s = s}
⊢ PreErgodic (⇑f : (a : G) → G) μ

Tactic:
refine ⟨fun s hsm hs ↦ aeconst_of_dense_setOf_preimage_smul_eq (M := G) hsm.nullMeasurableSet ?_⟩
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : SecondCountableTopology G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
inst_8 : μ.IsMulLeftInvariant
f : G →* G
hf : Dense.{u_1} (X := G) (⋃ (n : ℕ), (⇑f : (a : G) → G)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : (⇑f : (a : G) → G) ⁻¹' s = s
⊢ Dense.{u_1} (X := G) {g : G | (fun (x : G) ↦ g • x) ⁻¹' s = s}

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

Premises used: Set.iUnion_subset, Dense.mono
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : SecondCountableTopology G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
inst_8 : μ.IsMulLeftInvariant
f : G →* G
hf : Dense.{u_1} (X := G) (⋃ (n : ℕ), (⇑f : (a : G) → G)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : (⇑f : (a : G) → G) ⁻¹' s = s
refine :
  ∀ (n : ℕ) (x : G) (hx : Membership.mem (γ := Set G) ((⇑f : (a : G) → G)^[n] ⁻¹' 1) x),
    Membership.mem (γ := Set G) {g : G | (fun (x : G) ↦ g • x) ⁻¹' s = s} x
⊢ Dense.{u_1} (X := G) {g : G | (fun (x : G) ↦ g • x) ⁻¹' s = s}

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

Premises used: Set.iUnion_subset, Dense.mono
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : SecondCountableTopology G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
inst_8 : μ.IsMulLeftInvariant
f : G →* G
hf : Dense.{u_1} (X := G) (⋃ (n : ℕ), (⇑f : (a : G) → G)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : (⇑f : (a : G) → G) ⁻¹' s = s
n : ℕ
x : G
hx : Membership.mem (γ := Set G) ((⇑f : (a : G) → G)^[n] ⁻¹' 1) x
rw : (preimage (⇑f : (a : G) → G))^[n] s = s
rw₁ rw₂ : s = s
⊢ (⇑f : (a : G) → G)^[n] ⁻¹' s = s

Tactic:
rw [preimage_iterate_eq, iterate_fixed hs]

Premises used: Set.preimage_iterate_eq, Function.iterate_fixed
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : SecondCountableTopology G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
inst_8 : μ.IsMulLeftInvariant
f : G →* G
hf : Dense.{u_1} (X := G) (⋃ (n : ℕ), (⇑f : (a : G) → G)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : (⇑f : (a : G) → G) ⁻¹' s = s
n : ℕ
x : G
hx : Membership.mem (γ := Set G) ((⇑f : (a : G) → G)^[n] ⁻¹' 1) x
⊢ (⇑f : (a : G) → G)^[n] ⁻¹' s = s

Tactic:
have hsn : f^[n] ⁻¹' s = s := by
    rw [preimage_iterate_eq, iterate_fixed hs]
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : SecondCountableTopology G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
inst_8 : μ.IsMulLeftInvariant
f : G →* G
hf : Dense.{u_1} (X := G) (⋃ (n : ℕ), (⇑f : (a : G) → G)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : (⇑f : (a : G) → G) ⁻¹' s = s
n : ℕ
x : G
hx : Membership.mem (γ := Set G) ((⇑f : (a : G) → G)^[n] ⁻¹' 1) x
hsn : (⇑f : (a : G) → G)^[n] ⁻¹' s = s
⊢ (⇑f : (a : G) → G)^[n] x = 1

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

Premises used: Set.mem_one, Set.mem_preimage
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : SecondCountableTopology G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
inst_8 : μ.IsMulLeftInvariant
f : G →* G
hf : Dense.{u_1} (X := G) (⋃ (n : ℕ), (⇑f : (a : G) → G)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : (⇑f : (a : G) → G) ⁻¹' s = s
n : ℕ
x : G
hx : Membership.mem (γ := Set G) ((⇑f : (a : G) → G)^[n] ⁻¹' 1) x
hsn : (⇑f : (a : G) → G)^[n] ⁻¹' s = s
hx₁ : (⇑f : (a : G) → G)^[n] x = 1
⊢ (⇑f : (a : G) → G)^[n] ⁻¹' s = s

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

Premises used: Set.mem_one, Set.mem_preimage
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
inst_3 : SecondCountableTopology G
inst_4 : MeasurableSpace G
inst_5 : BorelSpace G
μ : Measure G
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
inst_8 : μ.IsMulLeftInvariant
f : G →* G
hf : Dense.{u_1} (X := G) (⋃ (n : ℕ), (⇑f : (a : G) → G)^[n] ⁻¹' 1)
s : Set G
hsm : MeasurableSet s
hs : (⇑f : (a : G) → G) ⁻¹' s = s
n : ℕ
x : G
hx : (⇑f : (a : G) → G)^[n] x = 1
hsn : (⇑f : (a : G) → G)^[n] ⁻¹' s = s
rw : (fun (x_1 : G) ↦ x • x_1) ⁻¹' (⇑f : (a : G) → G)^[n] ⁻¹' s = (⇑f : (a : G) → G)^[n] ⁻¹' s
⊢ Membership.mem (γ := Set G) {g : G | (fun (x : G) ↦ g • x) ⁻¹' s = s} x

Tactic:
rw [mem_setOf, ← hsn]

Premises used: Set.mem_setOf