case e_μ
ι : Type ?u.4969569
α : Type u_1
β : Type ?u.4969575
γ : Type ?u.4969578
δ : Type u_2
R : Type ?u.4969584
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : Zero β
f : α → δ
hf : AEMeasurable f
s : Set δ
hs : MeasurableSet s
⊢ map f μ = map (AEMeasurable.mk f hf) μ
ι : Type ?u.4969569
α : Type u_1
β : Type ?u.4969575
γ : Type ?u.4969578
δ : Type u_2
R : Type ?u.4969584
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : Zero β
f : α → δ
hf : AEMeasurable f
s : Set δ
hs : MeasurableSet s
⊢ restrict (map f μ) s = restrict (map (AEMeasurable.mk f hf) μ) s
congr 1
no goals
case e_μ
ι : Type ?u.4969569
α : Type u_1
β : Type ?u.4969575
γ : Type ?u.4969578
δ : Type u_2
R : Type ?u.4969584
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : Zero β
f : α → δ
hf : AEMeasurable f
s : Set δ
hs : MeasurableSet s
⊢ map f μ = map (AEMeasurable.mk f hf) μ
apply Measure.map_congr hf.ae_eq_mk
case h
ι : Type ?u.4969569
α : Type u_1
β : Type ?u.4969575
γ : Type ?u.4969578
δ : Type u_2
R : Type ?u.4969584
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : Zero β
f : α → δ
hf : AEMeasurable f
s : Set δ
hs : MeasurableSet s
⊢ restrict μ (AEMeasurable.mk f hf ⁻¹' s) = restrict μ (f ⁻¹' s)
ι : Type ?u.4969569
α : Type u_1
β : Type ?u.4969575
γ : Type ?u.4969578
δ : Type u_2
R : Type ?u.4969584
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : Zero β
f : α → δ
hf : AEMeasurable f
s : Set δ
hs : MeasurableSet s
⊢ map f (restrict μ (AEMeasurable.mk f hf ⁻¹' s)) = map f (restrict μ (f ⁻¹' s))
apply congr_arg
case h.h
ι : Type ?u.4969569
α : Type u_1
β : Type ?u.4969575
γ : Type ?u.4969578
δ : Type u_2
R : Type ?u.4969584
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : Zero β
f : α → δ
hf : AEMeasurable f
s : Set δ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ↑↑(restrict μ (AEMeasurable.mk f hf ⁻¹' s)) t = ↑↑(restrict μ (f ⁻¹' s)) t
case h
ι : Type ?u.4969569
α : Type u_1
β : Type ?u.4969575
γ : Type ?u.4969578
δ : Type u_2
R : Type ?u.4969584
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : Zero β
f : α → δ
hf : AEMeasurable f
s : Set δ
hs : MeasurableSet s
⊢ restrict μ (AEMeasurable.mk f hf ⁻¹' s) = restrict μ (f ⁻¹' s)
ext1 t ht
case h.h
ι : Type ?u.4969569
α : Type u_1
β : Type ?u.4969575
γ : Type ?u.4969578
δ : Type u_2
R : Type ?u.4969584
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : Zero β
f : α → δ
hf : AEMeasurable f
s : Set δ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ↑↑μ (t ∩ AEMeasurable.mk f hf ⁻¹' s) = ↑↑μ (t ∩ f ⁻¹' s)
case h.h
ι : Type ?u.4969569
α : Type u_1
β : Type ?u.4969575
γ : Type ?u.4969578
δ : Type u_2
R : Type ?u.4969584
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : Zero β
f : α → δ
hf : AEMeasurable f
s : Set δ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ↑↑(restrict μ (AEMeasurable.mk f hf ⁻¹' s)) t = ↑↑(restrict μ (f ⁻¹' s)) t
simp only [ht, Measure.restrict_apply]
case h.h.H
ι : Type ?u.4969569
α : Type u_1
β : Type ?u.4969575
γ : Type ?u.4969578
δ : Type u_2
R : Type ?u.4969584
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : Zero β
f : α → δ
hf : AEMeasurable f
s : Set δ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ t ∩ AEMeasurable.mk f hf ⁻¹' s =ᶠ[ae μ] t ∩ f ⁻¹' s
case h.h
ι : Type ?u.4969569
α : Type u_1
β : Type ?u.4969575
γ : Type ?u.4969578
δ : Type u_2
R : Type ?u.4969584
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : Zero β
f : α → δ
hf : AEMeasurable f
s : Set δ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ ↑↑μ (t ∩ AEMeasurable.mk f hf ⁻¹' s) = ↑↑μ (t ∩ f ⁻¹' s)
apply measure_congr
no goals
case h.h.H
ι : Type ?u.4969569
α : Type u_1
β : Type ?u.4969575
γ : Type ?u.4969578
δ : Type u_2
R : Type ?u.4969584
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
inst✝¹ : MeasurableSpace δ
f✝ g : α → β
μ ν : Measure α
inst✝ : Zero β
f : α → δ
hf : AEMeasurable f
s : Set δ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ t ∩ AEMeasurable.mk f hf ⁻¹' s =ᶠ[ae μ] t ∩ f ⁻¹' s
apply (EventuallyEq.refl _ _).inter (hf.ae_eq_mk.symm.preimage s)