α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
this : MeasurePreserving (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ MeasurePreserving f
⊢ Ergodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ Ergodic f
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
⊢ Ergodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ Ergodic f
have : MeasurePreserving (e ∘ f ∘ e.symm) μ' μ' ↔ MeasurePreserving f μ μ := by
  rw [h.comp_left_iff, (MeasurePreserving.symm e h).comp_right_iff]
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
this : MeasurePreserving (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ MeasurePreserving f
h : PreErgodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ PreErgodic f
⊢ Ergodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ Ergodic f
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
this : MeasurePreserving (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ MeasurePreserving f
⊢ Ergodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ Ergodic f
replace h : PreErgodic (e ∘ f ∘ e.symm) μ' ↔ PreErgodic f μ := h.preErgodic_conjugate_iff
no goals
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
this : MeasurePreserving (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ MeasurePreserving f
h : PreErgodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ PreErgodic f
⊢ Ergodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ Ergodic f
exact ⟨fun hf => { this.mp hf.toMeasurePreserving, h.mp hf.toPreErgodic with },
  fun hf => { this.mpr hf.toMeasurePreserving, h.mpr hf.toPreErgodic with }⟩
no goals
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
⊢ MeasurePreserving (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ MeasurePreserving f
rw [h.comp_left_iff, (MeasurePreserving.symm e h).comp_right_iff]