α : Type u_1
β : Type u_2
γ : Type ?u.176472
δ : Type ?u.176475
ι : Type ?u.176478
R : Type ?u.176481
R' : Type ?u.176484
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f : α → β
hf : Measurable f
μ : Measure α
⊢ ↑(mapₗ f) μ = ↑(mapₗ (AEMeasurable.mk f (_ : AEMeasurable f))) μ
α : Type u_1
β : Type u_2
γ : Type ?u.176472
δ : Type ?u.176475
ι : Type ?u.176478
R : Type ?u.176481
R' : Type ?u.176484
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f : α → β
hf : Measurable f
μ : Measure α
⊢ ↑(mapₗ f) μ = map f μ
simp only [← mapₗ_mk_apply_of_aemeasurable hf.aemeasurable]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.176472
δ : Type ?u.176475
ι : Type ?u.176478
R : Type ?u.176481
R' : Type ?u.176484
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f : α → β
hf : Measurable f
μ : Measure α
⊢ ↑(mapₗ f) μ = ↑(mapₗ (AEMeasurable.mk f (_ : AEMeasurable f))) μ
exact mapₗ_congr hf hf.aemeasurable.measurable_mk hf.aemeasurable.ae_eq_mk