α : Type u_2
β : Type u_3
γ : Type u_1
δ : Type ?u.163029
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
g : α → β
e : γ ≃ᵐ α
h : MeasurePreserving ↑e
hg : MeasurePreserving (g ∘ ↑e)
⊢ MeasurePreserving g
α : Type u_2
β : Type u_3
γ : Type u_1
δ : Type ?u.163029
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
g : α → β
e : γ ≃ᵐ α
h : MeasurePreserving ↑e
⊢ MeasurePreserving (g ∘ ↑e) ↔ MeasurePreserving g
refine' ⟨fun hg => _, fun hg => hg.comp h⟩
case h.e'_5
α : Type u_2
β : Type u_3
γ : Type u_1
δ : Type ?u.163029
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
g : α → β
e : γ ≃ᵐ α
h : MeasurePreserving ↑e
hg : MeasurePreserving (g ∘ ↑e)
⊢ g = (g ∘ ↑e) ∘ ↑(MeasurableEquiv.symm e)
α : Type u_2
β : Type u_3
γ : Type u_1
δ : Type ?u.163029
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
g : α → β
e : γ ≃ᵐ α
h : MeasurePreserving ↑e
hg : MeasurePreserving (g ∘ ↑e)
⊢ MeasurePreserving g
convert hg.comp (MeasurePreserving.symm e h)
no goals
case h.e'_5
α : Type u_2
β : Type u_3
γ : Type u_1
δ : Type ?u.163029
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
μa : Measure α
μb : Measure β
μc : Measure γ
μd : Measure δ
g : α → β
e : γ ≃ᵐ α
h : MeasurePreserving ↑e
hg : MeasurePreserving (g ∘ ↑e)
⊢ g = (g ∘ ↑e) ∘ ↑(MeasurableEquiv.symm e)
simp [Function.comp.assoc g e e.symm]