case pos
α : Type u_1
β : Type u_2
γ : Type ?u.186508
δ : Type ?u.186511
ι : Type ?u.186514
R : Type ?u.186517
R' : Type ?u.186520
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f g : α → β
h : f =ᶠ[ae μ] g
hf : AEMeasurable f
⊢ map f μ = map g μ

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.186508
δ : Type ?u.186511
ι : Type ?u.186514
R : Type ?u.186517
R' : Type ?u.186520
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f g : α → β
h : f =ᶠ[ae μ] g
hf : ¬AEMeasurable f
⊢ map f μ = map g μ
α : Type u_1
β : Type u_2
γ : Type ?u.186508
δ : Type ?u.186511
ι : Type ?u.186514
R : Type ?u.186517
R' : Type ?u.186520
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f g : α → β
h : f =ᶠ[ae μ] g
⊢ map f μ = map g μ
by_cases hf : AEMeasurable f μ
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.186508
δ : Type ?u.186511
ι : Type ?u.186514
R : Type ?u.186517
R' : Type ?u.186520
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f g : α → β
h : f =ᶠ[ae μ] g
hf : AEMeasurable f
hg : AEMeasurable g
⊢ map f μ = map g μ
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.186508
δ : Type ?u.186511
ι : Type ?u.186514
R : Type ?u.186517
R' : Type ?u.186520
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f g : α → β
h : f =ᶠ[ae μ] g
hf : AEMeasurable f
⊢ map f μ = map g μ
have hg : AEMeasurable g μ := hf.congr h
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.186508
δ : Type ?u.186511
ι : Type ?u.186514
R : Type ?u.186517
R' : Type ?u.186520
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f g : α → β
h : f =ᶠ[ae μ] g
hf : AEMeasurable f
hg : AEMeasurable g
⊢ ↑(mapₗ (AEMeasurable.mk f hf)) μ = ↑(mapₗ (AEMeasurable.mk g hg)) μ
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.186508
δ : Type ?u.186511
ι : Type ?u.186514
R : Type ?u.186517
R' : Type ?u.186520
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f g : α → β
h : f =ᶠ[ae μ] g
hf : AEMeasurable f
hg : AEMeasurable g
⊢ map f μ = map g μ
simp only [← mapₗ_mk_apply_of_aemeasurable hf, ← mapₗ_mk_apply_of_aemeasurable hg]
no goals
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.186508
δ : Type ?u.186511
ι : Type ?u.186514
R : Type ?u.186517
R' : Type ?u.186520
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f g : α → β
h : f =ᶠ[ae μ] g
hf : AEMeasurable f
hg : AEMeasurable g
⊢ ↑(mapₗ (AEMeasurable.mk f hf)) μ = ↑(mapₗ (AEMeasurable.mk g hg)) μ
exact
  mapₗ_congr hf.measurable_mk hg.measurable_mk (hf.ae_eq_mk.symm.trans (h.trans hg.ae_eq_mk))
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.186508
δ : Type ?u.186511
ι : Type ?u.186514
R : Type ?u.186517
R' : Type ?u.186520
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f g : α → β
h : f =ᶠ[ae μ] g
hf : ¬AEMeasurable f
hg : ¬AEMeasurable g
⊢ map f μ = map g μ
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.186508
δ : Type ?u.186511
ι : Type ?u.186514
R : Type ?u.186517
R' : Type ?u.186520
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f g : α → β
h : f =ᶠ[ae μ] g
hf : ¬AEMeasurable f
⊢ map f μ = map g μ
have hg : ¬AEMeasurable g μ := by simpa [← aemeasurable_congr h] using hf
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.186508
δ : Type ?u.186511
ι : Type ?u.186514
R : Type ?u.186517
R' : Type ?u.186520
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f g : α → β
h : f =ᶠ[ae μ] g
hf : ¬AEMeasurable f
hg : ¬AEMeasurable g
⊢ map f μ = map g μ
simp [map_of_not_aemeasurable, hf, hg]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.186508
δ : Type ?u.186511
ι : Type ?u.186514
R : Type ?u.186517
R' : Type ?u.186520
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
f g : α → β
h : f =ᶠ[ae μ] g
hf : ¬AEMeasurable f
⊢ ¬AEMeasurable g
simpa [← aemeasurable_congr h] using hf