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