case e_μ
α : Type u_2
E : Type u_3
F : Type ?u.1382470
𝕜 : Type ?u.1382473
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g✝ : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1385164
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
β : Type u_1
inst✝ : MeasurableSpace β
φ : α → β
hφ : AEMeasurable φ
f : β → E
hfm : AEStronglyMeasurable f (Measure.map φ μ)
g : β → E := AEStronglyMeasurable.mk f hfm
⊢ Measure.map φ μ = Measure.map (AEMeasurable.mk φ hφ) μ
α : Type u_2
E : Type u_3
F : Type ?u.1382470
𝕜 : Type ?u.1382473
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g✝ : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1385164
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
β : Type u_1
inst✝ : MeasurableSpace β
φ : α → β
hφ : AEMeasurable φ
f : β → E
hfm : AEStronglyMeasurable f (Measure.map φ μ)
g : β → E := AEStronglyMeasurable.mk f hfm
⊢ (∫ (y : β), g y ∂Measure.map φ μ) = ∫ (y : β), g y ∂Measure.map (AEMeasurable.mk φ hφ) μ
congr 1
no goals
case e_μ
α : Type u_2
E : Type u_3
F : Type ?u.1382470
𝕜 : Type ?u.1382473
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : CompleteSpace E
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedSpace 𝕜 E
inst✝⁶ : SMulCommClass ℝ 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
inst✝³ : CompleteSpace F
f✝ g✝ : α → E
m : MeasurableSpace α
μ : Measure α
X : Type ?u.1385164
inst✝² : TopologicalSpace X
inst✝¹ : FirstCountableTopology X
ν : Measure α
β : Type u_1
inst✝ : MeasurableSpace β
φ : α → β
hφ : AEMeasurable φ
f : β → E
hfm : AEStronglyMeasurable f (Measure.map φ μ)
g : β → E := AEStronglyMeasurable.mk f hfm
⊢ Measure.map φ μ = Measure.map (AEMeasurable.mk φ hφ) μ
exact Measure.map_congr hφ.ae_eq_mk