α : Type u_1
β : Type u_2
γ : Type ?u.308002
δ : Type ?u.308005
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α →ₘ[μ] β
⊢ mk ↑f (_ : AEStronglyMeasurable (↑f) μ) = Quotient.mk'' (Quotient.out' f)
α : Type u_1
β : Type u_2
γ : Type ?u.308002
δ : Type ?u.308005
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α →ₘ[μ] β
⊢ mk ↑f (_ : AEStronglyMeasurable (↑f) μ) = f
conv_rhs => rw [← Quotient.out_eq' f]
α : Type u_1
β : Type u_2
γ : Type ?u.308002
δ : Type ?u.308005
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α →ₘ[μ] β
g : { f // AEStronglyMeasurable f μ } := Quotient.out' f
⊢ mk ↑f (_ : AEStronglyMeasurable (↑f) μ) = Quotient.mk'' g
α : Type u_1
β : Type u_2
γ : Type ?u.308002
δ : Type ?u.308005
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α →ₘ[μ] β
⊢ mk ↑f (_ : AEStronglyMeasurable (↑f) μ) = Quotient.mk'' (Quotient.out' f)
set g : { f : α → β // AEStronglyMeasurable f μ } := Quotient.out' f
α : Type u_1
β : Type u_2
γ : Type ?u.308002
δ : Type ?u.308005
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α →ₘ[μ] β
g : { f // AEStronglyMeasurable f μ } := Quotient.out' f
this : g = { val := ↑g, property := (_ : AEStronglyMeasurable (↑g) μ) }
⊢ mk ↑f (_ : AEStronglyMeasurable (↑f) μ) = Quotient.mk'' g
α : Type u_1
β : Type u_2
γ : Type ?u.308002
δ : Type ?u.308005
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α →ₘ[μ] β
g : { f // AEStronglyMeasurable f μ } := Quotient.out' f
⊢ mk ↑f (_ : AEStronglyMeasurable (↑f) μ) = Quotient.mk'' g
have : g = ⟨g.1, g.2⟩ := Subtype.eq rfl
α : Type u_1
β : Type u_2
γ : Type ?u.308002
δ : Type ?u.308005
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α →ₘ[μ] β
g : { f // AEStronglyMeasurable f μ } := Quotient.out' f
this : g = { val := ↑g, property := (_ : AEStronglyMeasurable (↑g) μ) }
⊢ ↑f =ᵐ[μ] ↑g
α : Type u_1
β : Type u_2
γ : Type ?u.308002
δ : Type ?u.308005
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α →ₘ[μ] β
g : { f // AEStronglyMeasurable f μ } := Quotient.out' f
this : g = { val := ↑g, property := (_ : AEStronglyMeasurable (↑g) μ) }
⊢ mk ↑f (_ : AEStronglyMeasurable (↑f) μ) = Quotient.mk'' g
rw [this, ← mk, mk_eq_mk]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.308002
δ : Type ?u.308005
inst✝³ : MeasurableSpace α
μ ν : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α →ₘ[μ] β
g : { f // AEStronglyMeasurable f μ } := Quotient.out' f
this : g = { val := ↑g, property := (_ : AEStronglyMeasurable (↑g) μ) }
⊢ ↑f =ᵐ[μ] ↑g
exact (AEStronglyMeasurable.ae_eq_mk _).symm