α : Type u_2
β : Type u_1
γ : Type ?u.879714
δ : Type ?u.879717
δ' : Type ?u.879720
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g✝ : β → α
g : ↑(range f) → α
hf₁ : Measurable f
hf₂ : MeasurableSet (range f)
hg : Measurable g
H : LeftInverse g (rangeFactorization f)
e : α ≃ᵐ ↑(range f) :=
  {
    toEquiv :=
      { toFun := rangeFactorization f, invFun := g, left_inv := H,
        right_inv := (_ : Function.RightInverse g (rangeFactorization f)) },
    measurable_toFun := (_ : Measurable fun x => { val := f x, property := (_ : f x ∈ range f) }),
    measurable_invFun := hg }
⊢ MeasurableEmbedding f
α : Type u_2
β : Type u_1
γ : Type ?u.879714
δ : Type ?u.879717
δ' : Type ?u.879720
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g✝ : β → α
g : ↑(range f) → α
hf₁ : Measurable f
hf₂ : MeasurableSet (range f)
hg : Measurable g
H : LeftInverse g (rangeFactorization f)
⊢ MeasurableEmbedding f
set e : α ≃ᵐ range f :=
  ⟨⟨rangeFactorization f, g, H, H.rightInverse_of_surjective surjective_onto_range⟩,
    hf₁.subtype_mk, hg⟩
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.879714
δ : Type ?u.879717
δ' : Type ?u.879720
ι : Sort uι
s t u : Set α
inst✝² : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
f : α → β
g✝ : β → α
g : ↑(range f) → α
hf₁ : Measurable f
hf₂ : MeasurableSet (range f)
hg : Measurable g
H : LeftInverse g (rangeFactorization f)
e : α ≃ᵐ ↑(range f) :=
  {
    toEquiv :=
      { toFun := rangeFactorization f, invFun := g, left_inv := H,
        right_inv := (_ : Function.RightInverse g (rangeFactorization f)) },
    measurable_toFun := (_ : Measurable fun x => { val := f x, property := (_ : f x ∈ range f) }),
    measurable_invFun := hg }
⊢ MeasurableEmbedding f
exact (MeasurableEmbedding.subtype_coe hf₂).comp e.measurableEmbedding