awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
M : Type u_1
inst : TopologicalSpace M
X : Type u_2
inst_1 : TopologicalSpace X
inst_2 : R1Space X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
inst_5 : SMul M X
inst_6 : ContinuousSMul M X
μ : Measure X
inst_7 : IsFiniteMeasure μ
inst_8 : μ.InnerRegular
inst_9 : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : Dense.{u_1} (X := M) {g : M | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}
this : MeasurableSpace M := borel M
this_1 : BorelSpace M
⊢ EventuallyConst s (ae μ)

Tactic:
aeconst_of_forall_preimage_smul_ae_eq M hsm ?_

Premises used: MeasureTheory.aeconst_of_forall_preimage_smul_ae_eq
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
M : Type u_1
inst : TopologicalSpace M
X : Type u_2
inst_1 : TopologicalSpace X
inst_2 : R1Space X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
inst_5 : SMul M X
inst_6 : ContinuousSMul M X
μ : Measure X
inst_7 : IsFiniteMeasure μ
inst_8 : μ.InnerRegular
inst_9 : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : Dense.{u_1} (X := M) {g : M | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}
this : MeasurableSpace M := borel M
this_1 : BorelSpace M
refine : ∀ (g : M), (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
⊢ EventuallyConst s (ae μ)

Tactic:
refine aeconst_of_forall_preimage_smul_ae_eq M hsm ?_

Premises used: MeasureTheory.aeconst_of_forall_preimage_smul_ae_eq
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
M : Type u_1
inst : TopologicalSpace M
X : Type u_2
inst_1 : TopologicalSpace X
inst_2 : R1Space X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
inst_5 : SMul M X
inst_6 : ContinuousSMul M X
μ : Measure X
inst_7 : IsFiniteMeasure μ
inst_8 : μ.InnerRegular
inst_9 : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : Dense.{u_1} (X := M) {g : M | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}
this : MeasurableSpace M := borel M
this_1 : BorelSpace M
rwa :
  ∀ (hd : Eq.{u_1 + 1} (α := Set M) (closure[inst] {g : M | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}) univ),
    let this := borel M;
    BorelSpace M → IsClosed[inst] {g : M | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}
⊢ ∀ (g : M), (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s

Tactic:
rwa [dense_iff_closure_eq, IsClosed.closure_eq, eq_univ_iff_forall] at hd

Premises used: Set.eq_univ_iff_forall, IsClosed.closure_eq, dense_iff_closure_eq
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
M : Type u_1
inst : TopologicalSpace M
X : Type u_2
inst_1 : TopologicalSpace X
inst_2 : R1Space X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
inst_5 : SMul M X
inst_6 : ContinuousSMul M X
μ : Measure X
inst_7 : IsFiniteMeasure μ
inst_8 : μ.InnerRegular
inst_9 : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : Eq.{u_1 + 1} (α := Set M) (closure[inst] {g : M | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}) univ
this : MeasurableSpace M := borel M
this_1 : BorelSpace M
f : C(M × X, X) := { toFun := uncurry fun (x1 : M) (x2 : X) ↦ x1 • x2, continuous_toFun := ⋯ }
⊢ IsClosed[inst] {g : M | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}

Tactic:
isClosed_setOf_preimage_ae_eq f.curry.continuous (measurePreserving_smul · μ) _ hsm
    (measure_ne_top _ _)

Premises used: ContinuousMap.continuous, ContinuousMap.curry, setOf, MeasureTheory.measure_ne_top, MeasureTheory.isClosed_setOf_preimage_ae_eq, MeasureTheory.measurePreserving_smul
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
M : Type u_1
inst : TopologicalSpace M
X : Type u_2
inst_1 : TopologicalSpace X
inst_2 : R1Space X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
inst_5 : SMul M X
inst_6 : ContinuousSMul M X
μ : Measure X
inst_7 : IsFiniteMeasure μ
inst_8 : μ.InnerRegular
inst_9 : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : Eq.{u_1 + 1} (α := Set M) (closure[inst] {g : M | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}) univ
this : MeasurableSpace M := borel M
this_1 : BorelSpace M
f : C(M × X, X) := { toFun := uncurry fun (x1 : M) (x2 : X) ↦ x1 • x2, continuous_toFun := ⋯ }
⊢ IsClosed[inst] {g : M | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}

Tactic:
exact isClosed_setOf_preimage_ae_eq f.curry.continuous (measurePreserving_smul · μ) _ hsm
    (measure_ne_top _ _)

Premises used: ContinuousMap.continuous, ContinuousMap.curry, MeasureTheory.measure_ne_top, MeasureTheory.isClosed_setOf_preimage_ae_eq, MeasureTheory.measurePreserving_smul
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
M : Type u_1
inst : TopologicalSpace M
X : Type u_2
inst_1 : TopologicalSpace X
inst_2 : R1Space X
inst_3 : MeasurableSpace X
inst_4 : BorelSpace X
inst_5 : SMul M X
inst_6 : ContinuousSMul M X
μ : Measure X
inst_7 : IsFiniteMeasure μ
inst_8 : μ.InnerRegular
inst_9 : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : Dense.{u_1} (X := M) {g : M | (fun (x : X) ↦ g • x) ⁻¹' s = s}
⊢ EventuallyConst s (ae μ)

Tactic:
aeconst_of_dense_setOf_preimage_smul_ae hsm <| hd.mono fun _ h ↦ mem_setOf.2 <| .of_eq h

Premises used: Iff.mpr, Dense.mono, Filter.EventuallyEq.of_eq, Set.mem_setOf, aeconst_of_dense_setOf_preimage_smul_ae
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
M : Type u_3
inst_4 : Monoid M
inst_5 : TopologicalSpace M
inst_6 : MulAction M X
inst_7 : ContinuousSMul M X
g : M
hg : DenseRange.{u_3, 0} (X := M) fun (x : ℕ) ↦ g ^ x
μ : Measure X
inst_8 : IsFiniteMeasure μ
inst_9 : μ.InnerRegular
inst_10 : ErgodicSMul M X μ
⊢ let this := borel M;
  BorelSpace M

Tactic:
borelize M
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
M : Type u_3
inst_4 : Monoid M
inst_5 : TopologicalSpace M
inst_6 : MulAction M X
inst_7 : ContinuousSMul M X
g : M
hg : DenseRange.{u_3, 0} (X := M) fun (x : ℕ) ↦ g ^ x
μ : Measure X
inst_8 : IsFiniteMeasure μ
inst_9 : μ.InnerRegular
inst_10 : ErgodicSMul M X μ
this : MeasurableSpace M := borel M
this_1 : BorelSpace M
⊢ Ergodic (fun (x : X) ↦ g • x) μ

Tactic:
⟨measurePreserving_smul _ _, ⟨fun s hsm hs ↦ ?_⟩⟩

Premises used: Ergodic.mk, PreErgodic.mk, MeasureTheory.measurePreserving_smul
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
M : Type u_3
inst_4 : Monoid M
inst_5 : TopologicalSpace M
inst_6 : MulAction M X
inst_7 : ContinuousSMul M X
g : M
hg : DenseRange.{u_3, 0} (X := M) fun (x : ℕ) ↦ g ^ x
μ : Measure X
inst_8 : IsFiniteMeasure μ
inst_9 : μ.InnerRegular
inst_10 : ErgodicSMul M X μ
this : MeasurableSpace M := borel M
this_1 : BorelSpace M
refine : ∀ (s : Set X) (hsm : MeasurableSet s) (hs : (fun (x : X) ↦ g • x) ⁻¹' s = s), EventuallyConst s (ae μ)
⊢ Ergodic (fun (x : X) ↦ g • x) μ

Tactic:
refine ⟨measurePreserving_smul _ _, ⟨fun s hsm hs ↦ ?_⟩⟩
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
M : Type u_3
inst_4 : Monoid M
inst_5 : TopologicalSpace M
inst_6 : MulAction M X
inst_7 : ContinuousSMul M X
g : M
hg : DenseRange.{u_3, 0} (X := M) fun (x : ℕ) ↦ g ^ x
μ : Measure X
inst_8 : IsFiniteMeasure μ
inst_9 : μ.InnerRegular
inst_10 : ErgodicSMul M X μ
this : MeasurableSpace M := borel M
this_1 : BorelSpace M
s : Set X
hsm : MeasurableSet s
hs : (fun (x : X) ↦ g • x) ⁻¹' s = s
⊢ EventuallyConst s (ae μ)

Tactic:
aeconst_of_dense_setOf_preimage_smul_eq hsm.nullMeasurableSet (hg.mono ?_)

Premises used: MeasurableSet.nullMeasurableSet, aeconst_of_dense_setOf_preimage_smul_eq, Dense.mono
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
M : Type u_3
inst_4 : Monoid M
inst_5 : TopologicalSpace M
inst_6 : MulAction M X
inst_7 : ContinuousSMul M X
g : M
hg : DenseRange.{u_3, 0} (X := M) fun (x : ℕ) ↦ g ^ x
μ : Measure X
inst_8 : IsFiniteMeasure μ
inst_9 : μ.InnerRegular
inst_10 : ErgodicSMul M X μ
this : MeasurableSpace M := borel M
this_1 : BorelSpace M
s : Set X
hsm : MeasurableSet s
hs : (fun (x : X) ↦ g • x) ⁻¹' s = s
refine : Subset.{u_3} (α := Set M) (range fun (x : ℕ) ↦ g ^ x) {g : M | (fun (x : X) ↦ g • x) ⁻¹' s = s}
⊢ EventuallyConst s (ae μ)

Tactic:
refine aeconst_of_dense_setOf_preimage_smul_eq hsm.nullMeasurableSet (hg.mono ?_)

Premises used: MeasurableSet.nullMeasurableSet, aeconst_of_dense_setOf_preimage_smul_eq, Dense.mono
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
M : Type u_3
inst_4 : Monoid M
inst_5 : TopologicalSpace M
inst_6 : MulAction M X
inst_7 : ContinuousSMul M X
g : M
hg : DenseRange.{u_3, 0} (X := M) fun (x : ℕ) ↦ g ^ x
μ : Measure X
inst_8 : IsFiniteMeasure μ
inst_9 : μ.InnerRegular
inst_10 : ErgodicSMul M X μ
this : MeasurableSpace M := borel M
this_1 : BorelSpace M
s : Set X
hsm : MeasurableSet s
hs : (fun (x : X) ↦ g • x) ⁻¹' s = s
⊢ Subset.{u_3} (α := Set M) (range fun (x : ℕ) ↦ g ^ x) {g : M | (fun (x : X) ↦ g • x) ⁻¹' s = s}

Tactic:
range_subset_iff.2 fun n ↦ ?_

Premises used: Iff.mpr, Set.range_subset_iff
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
M : Type u_3
inst_4 : Monoid M
inst_5 : TopologicalSpace M
inst_6 : MulAction M X
inst_7 : ContinuousSMul M X
g : M
hg : DenseRange.{u_3, 0} (X := M) fun (x : ℕ) ↦ g ^ x
μ : Measure X
inst_8 : IsFiniteMeasure μ
inst_9 : μ.InnerRegular
inst_10 : ErgodicSMul M X μ
this : MeasurableSpace M := borel M
this_1 : BorelSpace M
s : Set X
hsm : MeasurableSet s
hs : (fun (x : X) ↦ g • x) ⁻¹' s = s
refine : ∀ (n : ℕ), Membership.mem (γ := Set M) {g : M | (fun (x : X) ↦ g • x) ⁻¹' s = s} (g ^ n)
⊢ Subset.{u_3} (α := Set M) (range fun (x : ℕ) ↦ g ^ x) {g : M | (fun (x : X) ↦ g • x) ⁻¹' s = s}

Tactic:
refine range_subset_iff.2 fun n ↦ ?_

Premises used: Iff.mpr, Set.range_subset_iff
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : R1Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
M : Type u_3
inst_4 : Monoid M
inst_5 : TopologicalSpace M
inst_6 : MulAction M X
inst_7 : ContinuousSMul M X
g : M
hg : DenseRange.{u_3, 0} (X := M) fun (x : ℕ) ↦ g ^ x
μ : Measure X
inst_8 : IsFiniteMeasure μ
inst_9 : μ.InnerRegular
inst_10 : ErgodicSMul M X μ
this : MeasurableSpace M := borel M
this_1 : BorelSpace M
s : Set X
hsm : MeasurableSet s
hs : (fun (x : X) ↦ g • x) ⁻¹' s = s
n : ℕ
rw : (fun (x : X) ↦ g ^ n • x) ⁻¹' s = s
rw₁ : (fun (x : X) ↦ g • x)^[n] ⁻¹' s = s
rw₂ : (preimage fun (x : X) ↦ g • x)^[n] s = s
rw₃ rw₄ : s = s
⊢ Membership.mem (γ := Set M) {g : M | (fun (x : X) ↦ g • x) ⁻¹' s = s} (g ^ n)

Tactic:
rw [mem_setOf, ← smul_iterate, preimage_iterate_eq, iterate_fixed hs]

Premises used: smul_iterate, Set.preimage_iterate_eq, Set.mem_setOf, Function.iterate_fixed
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
M : Type u_1
X : Type u_2
inst : Monoid M
inst_1 : SMul M X
inst_2 : TopologicalSpace X
inst_3 : R1Space X
inst_4 : MeasurableSpace X
inst_5 : BorelSpace X
μ : Measure X
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
N : Type u_3
inst_8 : MulAction M N
inst_9 : Monoid N
inst_10 : TopologicalSpace N
inst_11 : MulAction.IsMinimal M N
inst_12 : MulAction N X
inst_13 : IsScalarTower M N X
inst_14 : ContinuousSMul N X
inst_15 : ErgodicSMul N X μ
c : M
s : Set X
hsm : MeasurableSet s
⊢ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) ((fun (x : X) ↦ c • x) ⁻¹' s) : ENNReal)
    ((μ : (a : Set X) → ENNReal) s : ENNReal)

Tactic:
simpa only [smul_one_smul] using SMulInvariantMeasure.measure_preimage_smul (c • 1 : N) hsm

Premises used: MeasureTheory.SMulInvariantMeasure.measure_preimage_smul, smul_one_smul, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
M : Type u_1
X : Type u_2
inst : Monoid M
inst_1 : SMul M X
inst_2 : TopologicalSpace X
inst_3 : R1Space X
inst_4 : MeasurableSpace X
inst_5 : BorelSpace X
μ : Measure X
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
N : Type u_3
inst_8 : MulAction M N
inst_9 : Monoid N
inst_10 : TopologicalSpace N
inst_11 : MulAction.IsMinimal M N
inst_12 : MulAction N X
inst_13 : IsScalarTower M N X
inst_14 : ContinuousSMul N X
inst_15 : ErgodicSMul N X μ
s : Set X
hsm : MeasurableSet s
hs : ∀ (g : M), (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
⊢ EventuallyConst s (ae μ)

Tactic:
aeconst_of_dense_setOf_preimage_smul_ae (M := N) hsm.nullMeasurableSet ?_

Premises used: MeasurableSet.nullMeasurableSet, aeconst_of_dense_setOf_preimage_smul_ae
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
M : Type u_1
X : Type u_2
inst : Monoid M
inst_1 : SMul M X
inst_2 : TopologicalSpace X
inst_3 : R1Space X
inst_4 : MeasurableSpace X
inst_5 : BorelSpace X
μ : Measure X
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
N : Type u_3
inst_8 : MulAction M N
inst_9 : Monoid N
inst_10 : TopologicalSpace N
inst_11 : MulAction.IsMinimal M N
inst_12 : MulAction N X
inst_13 : IsScalarTower M N X
inst_14 : ContinuousSMul N X
inst_15 : ErgodicSMul N X μ
s : Set X
hsm : MeasurableSet s
hs : ∀ (g : M), (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
refine : Dense.{u_3} (X := N) {g : N | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}
⊢ EventuallyConst s (ae μ)

Tactic:
refine aeconst_of_dense_setOf_preimage_smul_ae (M := N) hsm.nullMeasurableSet ?_

Premises used: MeasurableSet.nullMeasurableSet, aeconst_of_dense_setOf_preimage_smul_ae
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
M : Type u_1
X : Type u_2
inst : Monoid M
inst_1 : SMul M X
inst_2 : TopologicalSpace X
inst_3 : R1Space X
inst_4 : MeasurableSpace X
inst_5 : BorelSpace X
μ : Measure X
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
N : Type u_3
inst_8 : MulAction M N
inst_9 : Monoid N
inst_10 : TopologicalSpace N
inst_11 : MulAction.IsMinimal M N
inst_12 : MulAction N X
inst_13 : IsScalarTower M N X
inst_14 : ContinuousSMul N X
inst_15 : ErgodicSMul N X μ
s : Set X
hsm : MeasurableSet s
hs : ∀ (g : M), (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
⊢ Dense.{u_3} (X := N) {g : N | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}

Tactic:
(MulAction.dense_orbit M 1).mono ?_

Premises used: Dense.mono, MulAction.dense_orbit, OfNat.ofNat
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
M : Type u_1
X : Type u_2
inst : Monoid M
inst_1 : SMul M X
inst_2 : TopologicalSpace X
inst_3 : R1Space X
inst_4 : MeasurableSpace X
inst_5 : BorelSpace X
μ : Measure X
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
N : Type u_3
inst_8 : MulAction M N
inst_9 : Monoid N
inst_10 : TopologicalSpace N
inst_11 : MulAction.IsMinimal M N
inst_12 : MulAction N X
inst_13 : IsScalarTower M N X
inst_14 : ContinuousSMul N X
inst_15 : ErgodicSMul N X μ
s : Set X
hsm : MeasurableSet s
hs : ∀ (g : M), (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
refine : Subset.{u_3} (α := Set N) (MulAction.orbit M 1) {g : N | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}
⊢ Dense.{u_3} (X := N) {g : N | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}

Tactic:
refine (MulAction.dense_orbit M 1).mono ?_

Premises used: Dense.mono, MulAction.dense_orbit, OfNat.ofNat
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
Goal:
M : Type u_1
X : Type u_2
inst : Monoid M
inst_1 : SMul M X
inst_2 : TopologicalSpace X
inst_3 : R1Space X
inst_4 : MeasurableSpace X
inst_5 : BorelSpace X
μ : Measure X
inst_6 : IsFiniteMeasure μ
inst_7 : μ.InnerRegular
N : Type u_3
inst_8 : MulAction M N
inst_9 : Monoid N
inst_10 : TopologicalSpace N
inst_11 : MulAction.IsMinimal M N
inst_12 : MulAction N X
inst_13 : IsScalarTower M N X
inst_14 : ContinuousSMul N X
inst_15 : ErgodicSMul N X μ
s : Set X
hsm : MeasurableSet s
hs : ∀ (g : M), (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s
g : M
⊢ Membership.mem (γ := Set N) {g : N | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s}
    ((fun (m : M) ↦ HSMul.hSMul (β := N) m 1) g)

Tactic:
simpa using hs g
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
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
μ : Measure X
inst_9 : IsFiniteMeasure μ
inst_10 : μ.InnerRegular
inst_11 : ErgodicSMul G X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : Dense (↑(MulAction.aestabilizer G μ s) : Set G)
g : G
hg : g ∈ Inv.inv ⁻¹' (↑(MulAction.aestabilizer G μ s) : Set G)
⊢ Membership.mem (γ := Set G) {g : G | (fun (x : X) ↦ g • x) ⁻¹' s =ᶠ[ae μ] s} g

Tactic:
simpa only [preimage_smul] using hg

Premises used: Set.preimage_smul
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
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 μ
⊢ let this := borel G;
  BorelSpace G

Tactic:
borelize G
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
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
⊢ Ergodic (fun (x : X) ↦ g • x) μ

Tactic:
⟨measurePreserving_smul _ _, ⟨fun s hsm hs ↦ ?_⟩⟩

Premises used: Ergodic.mk, PreErgodic.mk, MeasureTheory.measurePreserving_smul
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
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
refine : ∀ (s : Set X) (hsm : MeasurableSet s) (hs : (fun (x : X) ↦ g • x) ⁻¹' s = s), EventuallyConst s (ae μ)
⊢ Ergodic (fun (x : X) ↦ g • x) μ

Tactic:
refine ⟨measurePreserving_smul _ _, ⟨fun s hsm hs ↦ ?_⟩⟩
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
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
⊢ EventuallyConst s (ae μ)

Tactic:
aeconst_of_dense_aestabilizer_smul hsm.nullMeasurableSet (hg.mono ?_)

Premises used: aeconst_of_dense_aestabilizer_smul, MeasurableSet.nullMeasurableSet, Dense.mono
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
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
refine : (range fun (x : ℤ) ↦ g ^ x) ⊆ (↑(MulAction.aestabilizer G μ s) : Set G)
⊢ EventuallyConst s (ae μ)

Tactic:
refine aeconst_of_dense_aestabilizer_smul hsm.nullMeasurableSet (hg.mono ?_)

Premises used: aeconst_of_dense_aestabilizer_smul, MeasurableSet.nullMeasurableSet, Dense.mono
-- Module: Mathlib.Dynamics.Ergodic.Action.OfMinimal
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
rw₆ rw₇ : s =ᶠ[ae μ] s
⊢ (range fun (x : ℤ) ↦ g ^ x) ⊆ (↑(MulAction.aestabilizer G μ s) : Set G)

Tactic:
rw [← Subgroup.coe_zpowers, SetLike.coe_subset_coe, ← Subgroup.zpowers_inv, Subgroup.zpowers_le,
    MulAction.mem_aestabilizer, ← preimage_smul, hs]

Premises used: MulAction.mem_aestabilizer, Subgroup.zpowers_inv, Subgroup.zpowers_le, Set.preimage_smul, SetLike.coe_subset_coe, Subgroup.coe_zpowers
-- 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
by_contra : ∀ (h : a ∉ closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)), False
⊢ Membership.mem (γ := Set G) (closure[inst_1] (range fun (x : ℤ) ↦ g ^ x)) a

Tactic:
by_contra h
-- 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)
⊢ (range fun (x : ℤ) ↦ g ^ x)ᶜ ∈ 𝓝 a

Tactic:
rw [← mem_compl_iff, ← interior_compl, mem_interior_iff_mem_nhds] at h

Premises used: mem_interior_iff_mem_nhds, interior_compl, Set.mem_compl_iff
-- 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
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (x : G × G) ↦
    match (motive := G × G → G) x with
    | (x, y) => a * x / y

Tactic:
fun_prop
-- 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
⊢ (match (motive := G × G → G) 1 with
    | (x, y) => a * x / y) =
    a

Tactic:
simp
-- 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
⊢ 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)