case h
α : Type u_1
β : Type u_2
γ : Type ?u.172555
δ : Type ?u.172558
ι : Type ?u.172561
R : Type ?u.172564
R' : Type ?u.172567
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
f g : α → β
hf : Measurable f
hg : Measurable g
h : f =ᶠ[ae μ] g
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑(mapₗ f) μ) s = ↑↑(↑(mapₗ g) μ) s
α : Type u_1
β : Type u_2
γ : Type ?u.172555
δ : Type ?u.172558
ι : Type ?u.172561
R : Type ?u.172564
R' : Type ?u.172567
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f g : α → β
hf : Measurable f
hg : Measurable g
h : f =ᶠ[ae μ] g
⊢ ↑(mapₗ f) μ = ↑(mapₗ g) μ
ext1 s hs
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.172555
δ : Type ?u.172558
ι : Type ?u.172561
R : Type ?u.172564
R' : Type ?u.172567
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
f g : α → β
hf : Measurable f
hg : Measurable g
h : f =ᶠ[ae μ] g
s : Set β
hs : MeasurableSet s
⊢ ↑↑(↑(mapₗ f) μ) s = ↑↑(↑(mapₗ g) μ) s
simpa only [mapₗ, hf, hg, hs, dif_pos, liftLinear_apply, OuterMeasure.map_apply]
  using measure_congr (h.preimage s)