ι : Type ?u.3461513
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.3461525
R : Type ?u.3461528
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
g : β → γ
hg : MeasurableEmbedding g
μ : MeasureTheory.Measure α
H : AEMeasurable (g ∘ f)
⊢ AEMeasurable f
ι : Type ?u.3461513
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.3461525
R : Type ?u.3461528
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
g : β → γ
hg : MeasurableEmbedding g
μ : MeasureTheory.Measure α
⊢ AEMeasurable (g ∘ f) ↔ AEMeasurable f
refine' ⟨fun H => _, hg.measurable.comp_aemeasurable⟩
ι : Type ?u.3461513
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.3461525
R : Type ?u.3461528
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
g : β → γ
hg : MeasurableEmbedding g
μ : MeasureTheory.Measure α
H : AEMeasurable (g ∘ f)
⊢ AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f)
ι : Type ?u.3461513
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.3461525
R : Type ?u.3461528
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
g : β → γ
hg : MeasurableEmbedding g
μ : MeasureTheory.Measure α
H : AEMeasurable (g ∘ f)
⊢ AEMeasurable f
suffices AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) μ by
  rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this
no goals
ι : Type ?u.3461513
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.3461525
R : Type ?u.3461528
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
g : β → γ
hg : MeasurableEmbedding g
μ : MeasureTheory.Measure α
H : AEMeasurable (g ∘ f)
⊢ AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f)
exact hg.measurable_rangeSplitting.comp_aemeasurable H.subtype_mk
no goals
ι : Type ?u.3461513
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.3461525
R : Type ?u.3461528
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f g✝ : α → β
μ✝ ν : MeasureTheory.Measure α
g : β → γ
hg : MeasurableEmbedding g
μ : MeasureTheory.Measure α
H : AEMeasurable (g ∘ f)
this : AEMeasurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f)
⊢ AEMeasurable f
rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this