case refine'_1
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
hf : PreErgodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e))
⊢ ↑(MeasurableEquiv.symm e) ∘ ↑e ∘ f ∘ ↑(MeasurableEquiv.symm e) = f ∘ ↑(MeasurableEquiv.symm e)

case refine'_2
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
hf : PreErgodic f
⊢ ↑e ∘ f = (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ∘ ↑e
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
⊢ PreErgodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ↔ PreErgodic f
refine' ⟨fun hf => preErgodic_of_preErgodic_conjugate (h.symm e) hf _,
    fun hf => preErgodic_of_preErgodic_conjugate h hf _⟩
case refine'_1
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
hf : PreErgodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e))
⊢ (↑(MeasurableEquiv.symm e) ∘ ↑e) ∘ f ∘ ↑(MeasurableEquiv.symm e) = f ∘ ↑(MeasurableEquiv.symm e)
case refine'_1
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
hf : PreErgodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e))
⊢ ↑(MeasurableEquiv.symm e) ∘ ↑e ∘ f ∘ ↑(MeasurableEquiv.symm e) = f ∘ ↑(MeasurableEquiv.symm e)
change (e.symm ∘ e) ∘ f ∘ e.symm = f ∘ e.symm
no goals
case refine'_1
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
hf : PreErgodic (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e))
⊢ (↑(MeasurableEquiv.symm e) ∘ ↑e) ∘ f ∘ ↑(MeasurableEquiv.symm e) = f ∘ ↑(MeasurableEquiv.symm e)
rw [MeasurableEquiv.symm_comp_self, comp.left_id]
case refine'_2
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
hf : PreErgodic f
⊢ ↑e ∘ f = ↑e ∘ f ∘ ↑(MeasurableEquiv.symm e) ∘ ↑e
case refine'_2
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
hf : PreErgodic f
⊢ ↑e ∘ f = (↑e ∘ f ∘ ↑(MeasurableEquiv.symm e)) ∘ ↑e
change e ∘ f = e ∘ f ∘ e.symm ∘ e
no goals
case refine'_2
α : Type u_1
m : MeasurableSpace α
f : α → α
s : Set α
μ : Measure α
β : Type u_2
m' : MeasurableSpace β
μ' : Measure β
s' : Set β
g : α → β
e : α ≃ᵐ β
h : MeasurePreserving ↑e
hf : PreErgodic f
⊢ ↑e ∘ f = ↑e ∘ f ∘ ↑(MeasurableEquiv.symm e) ∘ ↑e
rw [MeasurableEquiv.symm_comp_self, comp.right_id]