-- Mathlib/Dynamics/Ergodic/Action/OfMinimal.lean
theorem ErgodicSMul.trans_isMinimal (N : Type*) [MulAction M N]
    [Monoid N] [TopologicalSpace N] [MulAction.IsMinimal M N]
    [MulAction N X] [IsScalarTower M N X] [ContinuousSMul N X] [ErgodicSMul N X μ] :
    ErgodicSMul M X μ where
  measure_preimage_smul c s hsm

Proof state:
M : Type u_1
X : Type u_2
inst✝¹⁵ : Monoid M
inst✝¹⁴ : SMul M X
inst✝¹³ : TopologicalSpace X
inst✝¹² : R1Space X
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : BorelSpace X
μ : Measure X
inst✝⁹ : IsFiniteMeasure μ
inst✝⁸ : μ.InnerRegular
N : Type u_3
inst✝⁷ : MulAction M N
inst✝⁶ : Monoid N
inst✝⁵ : TopologicalSpace N
inst✝⁴ : MulAction.IsMinimal M N
inst✝³ : MulAction N X
inst✝² : IsScalarTower M N X
inst✝¹ : ContinuousSMul N X
inst✝ : ErgodicSMul N X μ
c : M
s : Set X
hsm : MeasurableSet s
⊢ μ ((fun x => c • x) ⁻¹' s) = μ s

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

Result:
no goals

Proof state:
M : Type u_1
X : Type u_2
inst✝¹⁵ : Monoid M
inst✝¹⁴ : SMul M X
inst✝¹³ : TopologicalSpace X
inst✝¹² : R1Space X
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : BorelSpace X
μ : Measure X
inst✝⁹ : IsFiniteMeasure μ
inst✝⁸ : μ.InnerRegular
N : Type u_3
inst✝⁷ : MulAction M N
inst✝⁶ : Monoid N
inst✝⁵ : TopologicalSpace N
inst✝⁴ : MulAction.IsMinimal M N
inst✝³ : MulAction N X
inst✝² : IsScalarTower M N X
inst✝¹ : ContinuousSMul N X
inst✝ : ErgodicSMul N X μ
s : Set X
hsm : MeasurableSet s
hs : ∀ (g : M), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s
⊢ EventuallyConst s (ae μ)

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

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

Proof state:
case intro
M : Type u_1
X : Type u_2
inst✝¹⁵ : Monoid M
inst✝¹⁴ : SMul M X
inst✝¹³ : TopologicalSpace X
inst✝¹² : R1Space X
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : BorelSpace X
μ : Measure X
inst✝⁹ : IsFiniteMeasure μ
inst✝⁸ : μ.InnerRegular
N : Type u_3
inst✝⁷ : MulAction M N
inst✝⁶ : Monoid N
inst✝⁵ : TopologicalSpace N
inst✝⁴ : MulAction.IsMinimal M N
inst✝³ : MulAction N X
inst✝² : IsScalarTower M N X
inst✝¹ : ContinuousSMul N X
inst✝ : ErgodicSMul N X μ
s : Set X
hsm : MeasurableSet s
hs : ∀ (g : M), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s
g : M
⊢ (fun m => m • 1) g ∈ {g | (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s}

Tactic:
simpa using hs g

Result:
no goals

Proof state:
M : Type u_1
X : Type u_2
inst✝¹⁵ : Monoid M
inst✝¹⁴ : SMul M X
inst✝¹³ : TopologicalSpace X
inst✝¹² : R1Space X
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : BorelSpace X
μ : Measure X
inst✝⁹ : IsFiniteMeasure μ
inst✝⁸ : μ.InnerRegular
N : Type u_3
inst✝⁷ : MulAction M N
inst✝⁶ : Monoid N
inst✝⁵ : TopologicalSpace N
inst✝⁴ : MulAction.IsMinimal M N
inst✝³ : MulAction N X
inst✝² : IsScalarTower M N X
inst✝¹ : ContinuousSMul N X
inst✝ : ErgodicSMul N X μ
s : Set X
hsm : MeasurableSet s
hs : ∀ (g : M), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s
⊢ MulAction.orbit M 1 ⊆ {g | (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s}

Tactic:
rintro _ ⟨g, rfl⟩

Result:
case intro
M : Type u_1
X : Type u_2
inst✝¹⁵ : Monoid M
inst✝¹⁴ : SMul M X
inst✝¹³ : TopologicalSpace X
inst✝¹² : R1Space X
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : BorelSpace X
μ : Measure X
inst✝⁹ : IsFiniteMeasure μ
inst✝⁸ : μ.InnerRegular
N : Type u_3
inst✝⁷ : MulAction M N
inst✝⁶ : Monoid N
inst✝⁵ : TopologicalSpace N
inst✝⁴ : MulAction.IsMinimal M N
inst✝³ : MulAction N X
inst✝² : IsScalarTower M N X
inst✝¹ : ContinuousSMul N X
inst✝ : ErgodicSMul N X μ
s : Set X
hsm : MeasurableSet s
hs : ∀ (g : M), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s
g : M
⊢ (fun m => m • 1) g ∈ {g | (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s}

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

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

Result:
M : Type u_1
X : Type u_2
inst✝¹⁵ : Monoid M
inst✝¹⁴ : SMul M X
inst✝¹³ : TopologicalSpace X
inst✝¹² : R1Space X
inst✝¹¹ : MeasurableSpace X
inst✝¹⁰ : BorelSpace X
μ : Measure X
inst✝⁹ : IsFiniteMeasure μ
inst✝⁸ : μ.InnerRegular
N : Type u_3
inst✝⁷ : MulAction M N
inst✝⁶ : Monoid N
inst✝⁵ : TopologicalSpace N
inst✝⁴ : MulAction.IsMinimal M N
inst✝³ : MulAction N X
inst✝² : IsScalarTower M N X
inst✝¹ : ContinuousSMul N X
inst✝ : ErgodicSMul N X μ
s : Set X
hsm : MeasurableSet s
hs : ∀ (g : M), (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s
⊢ MulAction.orbit M 1 ⊆ {g | (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s}