∀ {X : Type u_2} [inst : TopologicalSpace X] [R1Space X] [inst_2 : MeasurableSpace X] [BorelSpace X] {M : Type u_3}
  [inst_4 : Monoid M] [inst_5 : TopologicalSpace M] [inst_6 : MulAction M X] [ContinuousSMul M X] {g : M},
  (DenseRange fun x => g ^ x) →
    ∀ (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicSMul M X μ],
      Ergodic (fun x => g • x) μ