-- Mathlib/Dynamics/Ergodic/Action/OfMinimal.lean
theorem aeconst_of_dense_setOf_preimage_smul_ae (hsm : NullMeasurableSet s μ)
    (hd : Dense {g : M | (g • ·) ⁻¹' s =ᵐ[μ] s}) : EventuallyConst s (ae μ)

Proof state:
M : Type u_1
inst✝⁹ : TopologicalSpace M
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : SMul M X
inst✝³ : ContinuousSMul M X
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : Dense {g | (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s}
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
⊢ ∀ (g : M), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s

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

Result:
M : Type u_1
inst✝⁹ : TopologicalSpace M
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : SMul M X
inst✝³ : ContinuousSMul M X
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : closure {g | (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s} = univ
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
⊢ IsClosed {g | (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s}

Proof state:
M : Type u_1
inst✝⁹ : TopologicalSpace M
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : SMul M X
inst✝³ : ContinuousSMul M X
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : Dense {g | (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s}
⊢ EventuallyConst s (ae μ)

Tactic:
borelize M

Result:
M : Type u_1
inst✝⁹ : TopologicalSpace M
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : SMul M X
inst✝³ : ContinuousSMul M X
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : Dense {g | (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s}
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
⊢ EventuallyConst s (ae μ)

Proof state:
M : Type u_1
inst✝⁹ : TopologicalSpace M
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : SMul M X
inst✝³ : ContinuousSMul M X
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : Dense {g | (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s}
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
⊢ EventuallyConst s (ae μ)

Tactic:
refine aeconst_of_forall_preimage_smul_ae_eq M hsm ?_

Result:
M : Type u_1
inst✝⁹ : TopologicalSpace M
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : SMul M X
inst✝³ : ContinuousSMul M X
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul M X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : Dense {g | (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s}
this✝¹ : MeasurableSpace M := borel M
this✝ : BorelSpace M
⊢ ∀ (g : M), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s