awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : ContinuousInv G
X : Type u_2
inst_3 : TopologicalSpace X
inst_4 : R1Space X
inst_5 : MeasurableSpace X
inst_6 : BorelSpace X
inst_7 : MulAction G X
inst_8 : ContinuousSMul G X
g : G
hg : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ g ^ x
μ : Measure X
inst_9 : IsFiniteMeasure μ
inst_10 : μ.InnerRegular
inst_11 : ErgodicSMul G X μ
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
s : Set X
hsm : MeasurableSet s
hs : (fun (x : X) ↦ g • x) ⁻¹' s = s
rw : (↑(Subgroup.zpowers g) : Set G) ⊆ (↑(MulAction.aestabilizer G μ s) : Set G)
rw₁ : LE.le (α := Subgroup G) (Subgroup.zpowers g) (MulAction.aestabilizer G μ s)
rw₂ : LE.le (α := Subgroup G) (Subgroup.zpowers g⁻¹) (MulAction.aestabilizer G μ s)
⊢ (range fun (x : ℤ) ↦ g ^ x) ⊆ (↑(MulAction.aestabilizer G μ s) : Set G)
have rw₃ : Membership.mem (γ := Subgroup G) (MulAction.aestabilizer G μ s) g⁻¹
Tactic: rw [← Subgroup.coe_zpowers, SetLike.coe_subset_coe, ← Subgroup.zpowers_inv, Subgroup.zpowers_le,
    MulAction.mem_aestabilizer, ← preimage_smul, hs]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : ContinuousInv G
X : Type u_2
inst_3 : TopologicalSpace X
inst_4 : R1Space X
inst_5 : MeasurableSpace X
inst_6 : BorelSpace X
inst_7 : MulAction G X
inst_8 : ContinuousSMul G X
g : G
hg : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ g ^ x
μ : Measure X
inst_9 : IsFiniteMeasure μ
inst_10 : μ.InnerRegular
inst_11 : ErgodicSMul G X μ
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
s : Set X
hsm : MeasurableSet s
hs : (fun (x : X) ↦ g • x) ⁻¹' s = s
rw : (↑(Subgroup.zpowers g) : Set G) ⊆ (↑(MulAction.aestabilizer G μ s) : Set G)
rw₁ : LE.le (α := Subgroup G) (Subgroup.zpowers g) (MulAction.aestabilizer G μ s)
rw₂ : LE.le (α := Subgroup G) (Subgroup.zpowers g⁻¹) (MulAction.aestabilizer G μ s)
rw₃ : Membership.mem (γ := Subgroup G) (MulAction.aestabilizer G μ s) g⁻¹
⊢ (range fun (x : ℤ) ↦ g ^ x) ⊆ (↑(MulAction.aestabilizer G μ s) : Set G)
have rw₄ : g⁻¹ • s =ᶠ[ae μ] s
Tactic: rw [← Subgroup.coe_zpowers, SetLike.coe_subset_coe, ← Subgroup.zpowers_inv, Subgroup.zpowers_le,
    MulAction.mem_aestabilizer, ← preimage_smul, hs]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : ContinuousInv G
X : Type u_2
inst_3 : TopologicalSpace X
inst_4 : R1Space X
inst_5 : MeasurableSpace X
inst_6 : BorelSpace X
inst_7 : MulAction G X
inst_8 : ContinuousSMul G X
g : G
hg : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ g ^ x
μ : Measure X
inst_9 : IsFiniteMeasure μ
inst_10 : μ.InnerRegular
inst_11 : ErgodicSMul G X μ
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
s : Set X
hsm : MeasurableSet s
hs : (fun (x : X) ↦ g • x) ⁻¹' s = s
rw : (↑(Subgroup.zpowers g) : Set G) ⊆ (↑(MulAction.aestabilizer G μ s) : Set G)
rw₁ : LE.le (α := Subgroup G) (Subgroup.zpowers g) (MulAction.aestabilizer G μ s)
rw₂ : LE.le (α := Subgroup G) (Subgroup.zpowers g⁻¹) (MulAction.aestabilizer G μ s)
rw₃ : Membership.mem (γ := Subgroup G) (MulAction.aestabilizer G μ s) g⁻¹
rw₄ : g⁻¹ • s =ᶠ[ae μ] s
⊢ (range fun (x : ℤ) ↦ g ^ x) ⊆ (↑(MulAction.aestabilizer G μ s) : Set G)
have rw₅ : (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
Tactic: rw [← Subgroup.coe_zpowers, SetLike.coe_subset_coe, ← Subgroup.zpowers_inv, Subgroup.zpowers_le,
    MulAction.mem_aestabilizer, ← preimage_smul, hs]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : ContinuousInv G
X : Type u_2
inst_3 : TopologicalSpace X
inst_4 : R1Space X
inst_5 : MeasurableSpace X
inst_6 : BorelSpace X
inst_7 : MulAction G X
inst_8 : ContinuousSMul G X
g : G
hg : DenseRange.{u_1, 0} (X := G) fun (x : ℤ) ↦ g ^ x
μ : Measure X
inst_9 : IsFiniteMeasure μ
inst_10 : μ.InnerRegular
inst_11 : ErgodicSMul G X μ
this : MeasurableSpace G := borel G
this_1 : BorelSpace G
s : Set X
hsm : MeasurableSet s
hs : (fun (x : X) ↦ g • x) ⁻¹' s = s
rw : (↑(Subgroup.zpowers g) : Set G) ⊆ (↑(MulAction.aestabilizer G μ s) : Set G)
rw₁ : LE.le (α := Subgroup G) (Subgroup.zpowers g) (MulAction.aestabilizer G μ s)
rw₂ : LE.le (α := Subgroup G) (Subgroup.zpowers g⁻¹) (MulAction.aestabilizer G μ s)
rw₃ : Membership.mem (γ := Subgroup G) (MulAction.aestabilizer G μ s) g⁻¹
rw₄ : g⁻¹ • s =ᶠ[ae μ] s
rw₅ : (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
⊢ (range fun (x : ℤ) ↦ g ^ x) ⊆ (↑(MulAction.aestabilizer G μ s) : Set G)
have rw₆ : s =ᶠ[ae μ] s
Tactic: rw [← Subgroup.coe_zpowers, SetLike.coe_subset_coe, ← Subgroup.zpowers_inv, Subgroup.zpowers_le,
    MulAction.mem_aestabilizer, ← preimage_smul, hs]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
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
⊢ Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)) a
have by_contra : ∀ (h : a ∉ closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (hypothesis)
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), 1 ∈ V ∧ IsOpen[inst_1] V ∧ ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
have h₁ : (range fun (x : ℤ) ↦ g ^ x)ᶜ ∈ 𝓝 a
Tactic: rw [← mem_compl_iff, ← interior_compl, mem_interior_iff_mem_nhds] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (hypothesis)
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
⊢ ∃ (V : Set G), 1 ∈ V ∧ IsOpen[inst_1] V ∧ ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
have this : Tendsto
  (fun (x : G × G) ↦
    match (motive := G × G → G) x with
    | (x, y) => a * x / y)
  (𝓝 1) (𝓝 a)
Tactic: have : Tendsto (fun (x, y) ↦ a * x / y) (𝓝 1) (𝓝 a) :=
      Continuous.tendsto' (by fun_prop) _ _ (by simp)
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (hypothesis)
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)
⊢ ∃ (V : Set G), 1 ∈ V ∧ IsOpen[inst_1] V ∧ ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y
have 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)
Tactic: rw [nhds_prod_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
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)
⊢ False
have obtain : ∀ (V : Set G) (hV₁ : 1 ∈ V) (hVo : IsOpen[inst_1] V) (hV : ∀ x ∈ V, ∀ y ∈ V, ∀ (m : ℤ), g ^ m ≠ a * x / y), 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
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (hypothesis)
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
⊢ False
have hso : IsOpen[inst_1] s
Tactic: have hso : IsOpen s := isOpen_iUnion fun m ↦ hVo.smul _
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (hypothesis)
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
⊢ False
have hsne : s.Nonempty
Tactic: have hsne : s.Nonempty := ⟨1, mem_iUnion.2 ⟨0, by simpa⟩⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
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)
have simp_rw : ∀ (i : ℤ) ⦃a_1 : G⦄, a_1 ∈ g ^ i • V → a_1 ∉ a • V
Tactic: simp_rw [s, disjoint_iUnion_left, disjoint_left]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
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)
⊢ False
have apply : g ^ m = a * y / x
Tactic: apply hV y hy x hx m
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (hypothesis)
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
⊢ False
have hd : 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
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
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
have simp : Eq.{u_1 + 1} (α := Set G) (⋃ (i : ℤ), g⁻¹ • g ^ i • V) (⋃ (m : ℤ), g ^ m • V)
Tactic: simp only [s, preimage_iUnion, ← smul_eq_mul, preimage_smul]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
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)
have refine : ∀ (m : ℤ), g ^ (-1 + m) • V = g⁻¹ • g ^ m • V
Tactic: refine iUnion_congr_of_surjective _ (add_left_surjective (-1)) fun m ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (hypothesis)
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)
⊢ False
have hgs : (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]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
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
have inr : a • V ⊆ sᶜ
Tactic: refine (hVo.smul a).measure_ne_zero μ (.image _ ⟨1, hV₁⟩) (measure_mono_null ?_ h)
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
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)
⊢ a • V ⊆ sᶜ
have 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ᶜ
Tactic: rwa [disjoint_right] at hd
Cleared hypotheses: hd, hgs, h
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (hypothesis)
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
⊢ False
have x : 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
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
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) μ
have 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}
Tactic: refine ⟨fun s hsm hs ↦ aeconst_of_dense_setOf_preimage_smul_eq (M := G) hsm.nullMeasurableSet ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
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}
have 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
Tactic: refine hf.mono <| iUnion_subset fun n x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
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
have rw : (preimage (⇑f : (a : G) → G))^[n] s = s
Tactic: rw [preimage_iterate_eq, iterate_fixed hs]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
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
⊢ (⇑f : (a : G) → G)^[n] ⁻¹' s = s
have rw₁ : s = s
Tactic: rw [preimage_iterate_eq, iterate_fixed hs]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (hypothesis)
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
⊢ Membership.mem (γ := Set G) {g : G | (fun (x : G) ↦ g • x) ⁻¹' s = s} x
have hsn : (⇑f : (a : G) → G)^[n] ⁻¹' s = s
Tactic: have hsn : f^[n] ⁻¹' s = s := by
    rw [preimage_iterate_eq, iterate_fixed hs]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (hypothesis)
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
⊢ Membership.mem (γ := Set G) {g : G | (fun (x : G) ↦ g • x) ⁻¹' s = s} x
have hx₁ : (⇑f : (a : G) → G)^[n] x = 1
Tactic: rw [mem_preimage, Set.mem_one] at hx
Cleared hypotheses: hx, hsn
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
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
⊢ Membership.mem (γ := Set G) {g : G | (fun (x : G) ↦ g • x) ⁻¹' s = s} x
have rw : (fun (x_1 : G) ↦ x • x_1) ⁻¹' (⇑f : (a : G) → G)^[n] ⁻¹' s = (⇑f : (a : G) → G)^[n] ⁻¹' s
Tactic: rw [mem_setOf, ← hsn]
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.OfMinimal (goal)
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
⊢ (fun (x_1 : G) ↦ x • x_1) ⁻¹' (⇑f : (a : G) → G)^[n] ⁻¹' s = (⇑f : (a : G) → G)^[n] ⁻¹' s
have h : ∀ (y : G),
  Membership.mem (γ := Set G) ((fun (x_1 : G) ↦ x • x_1) ⁻¹' (⇑f : (a : G) → G)^[n] ⁻¹' s) y ↔
    y ∈ (⇑f : (a : G) → G)^[n] ⁻¹' s
Tactic: ext y
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Regular (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
⊢ ErgodicSMul G G μ
have refine : ∀ {s : Set G} (hsm : MeasurableSet s) (hs : ∀ (g : G), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s), EventuallyConst s (ae μ)
Tactic: refine ⟨fun {s} hsm hs ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Ergodic.Action.Regular (goal)
Goal:
G : Type u_1
inst : Group G
inst_1 : MeasurableSpace G
inst_2 : MeasurableMul₂ G
inst_3 : MeasurableInv G
μ : Measure G
inst_4 : SFinite μ
inst_5 : μ.IsMulLeftInvariant
s : Set G
hsm : MeasurableSet s
hs : ∀ (g : G), (fun (x : G) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
this : (∃ᵐ (x : G) ∂μ, x ∈ s) → ∀ᵐ (x : G) ∂μ, x ∈ s
⊢ EventuallyConst s (ae μ)
have simp : (∀ᵐ (x : G) ∂μ, x ∈ s) ∨ ¬∃ᵐ (x : G) ∂μ, x ∈ s
Tactic: simp only [eventuallyConst_set, ← not_frequently]