α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.382740
δ' : Type ?u.382743
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
⊢ Measurable f
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.382740
δ' : Type ?u.382743
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
⊢ Measurable (g ∘ f) ↔ Measurable f
refine' ⟨fun H => _, hg.measurable.comp⟩
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.382740
δ' : Type ?u.382743
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
⊢ Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f)
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.382740
δ' : Type ?u.382743
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
⊢ Measurable f
suffices Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f) by
  rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this
no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.382740
δ' : Type ?u.382743
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
⊢ Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f)
exact hg.measurable_rangeSplitting.comp H.subtype_mk
no goals
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.382740
δ' : Type ?u.382743
ι : Sort uι
s t u : Set α
mα : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g : β → γ
hg : MeasurableEmbedding g
H : Measurable (g ∘ f)
this : Measurable ((rangeSplitting g ∘ rangeFactorization g) ∘ f)
⊢ Measurable f
rwa [(rightInverse_rangeSplitting hg.injective).comp_eq_id] at this