∀ {X : Type u_1} {m : MeasurableSpace X} {μ ν : MeasureTheory.Measure X} {f : X → X}
  [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure ν],
  Ergodic f μ → MeasureTheory.MeasurePreserving f ν ν → ν.AbsolutelyContinuous μ → ν = μ