case h
ι : Type ?u.2309729
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.2309741
R : Type ?u.2309744
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
⊢ ↑↑(Measure.map g (Measure.map f μ)) s = ↑↑(Measure.map (g ∘ f) μ) s
ι : Type ?u.2309729
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.2309741
R : Type ?u.2309744
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
⊢ Measure.map g (Measure.map f μ) = Measure.map (g ∘ f) μ
ext1 s hs
case h
ι : Type ?u.2309729
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.2309741
R : Type ?u.2309744
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
⊢ ↑↑(Measure.map g (Measure.map f μ)) s = ↑↑(Measure.map (g ∘ f) μ) s
case h
ι : Type ?u.2309729
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.2309741
R : Type ?u.2309744
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
⊢ ↑↑(Measure.map g (Measure.map f μ)) s = ↑↑(Measure.map (g ∘ f) μ) s
let g' := hg.mk g
case h
ι : Type ?u.2309729
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.2309741
R : Type ?u.2309744
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
A : Measure.map g (Measure.map f μ) = Measure.map g' (Measure.map f μ)
⊢ ↑↑(Measure.map g (Measure.map f μ)) s = ↑↑(Measure.map (g ∘ f) μ) s
case h
ι : Type ?u.2309729
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.2309741
R : Type ?u.2309744
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
⊢ ↑↑(Measure.map g (Measure.map f μ)) s = ↑↑(Measure.map (g ∘ f) μ) s
have A : map g (map f μ) = map g' (map f μ) := by
  apply MeasureTheory.Measure.map_congr
  exact hg.ae_eq_mk
case h
ι : Type ?u.2309729
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.2309741
R : Type ?u.2309744
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
A : Measure.map g (Measure.map f μ) = Measure.map g' (Measure.map f μ)
B : Measure.map (g ∘ f) μ = Measure.map (g' ∘ f) μ
⊢ ↑↑(Measure.map g (Measure.map f μ)) s = ↑↑(Measure.map (g ∘ f) μ) s
case h
ι : Type ?u.2309729
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.2309741
R : Type ?u.2309744
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
A : Measure.map g (Measure.map f μ) = Measure.map g' (Measure.map f μ)
⊢ ↑↑(Measure.map g (Measure.map f μ)) s = ↑↑(Measure.map (g ∘ f) μ) s
have B : map (g ∘ f) μ = map (g' ∘ f) μ := by
  apply MeasureTheory.Measure.map_congr
  exact ae_of_ae_map hf hg.ae_eq_mk
case h
ι : Type ?u.2309729
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.2309741
R : Type ?u.2309744
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
A : Measure.map g (Measure.map f μ) = Measure.map g' (Measure.map f μ)
B : Measure.map (g ∘ f) μ = Measure.map (g' ∘ f) μ
⊢ ↑↑μ (f ⁻¹' (mk g hg ⁻¹' s)) = ↑↑μ (mk g hg ∘ f ⁻¹' s)
case h
ι : Type ?u.2309729
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.2309741
R : Type ?u.2309744
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
A : Measure.map g (Measure.map f μ) = Measure.map g' (Measure.map f μ)
B : Measure.map (g ∘ f) μ = Measure.map (g' ∘ f) μ
⊢ ↑↑(Measure.map g (Measure.map f μ)) s = ↑↑(Measure.map (g ∘ f) μ) s
simp only [A, B, hs, hg.measurable_mk.aemeasurable.comp_aemeasurable hf, hg.measurable_mk,
  hg.measurable_mk hs, hf, map_apply, map_apply_of_aemeasurable]
no goals
case h
ι : Type ?u.2309729
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.2309741
R : Type ?u.2309744
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
A : Measure.map g (Measure.map f μ) = Measure.map g' (Measure.map f μ)
B : Measure.map (g ∘ f) μ = Measure.map (g' ∘ f) μ
⊢ ↑↑μ (f ⁻¹' (mk g hg ⁻¹' s)) = ↑↑μ (mk g hg ∘ f ⁻¹' s)
rfl
case h
ι : Type ?u.2309729
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.2309741
R : Type ?u.2309744
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
⊢ g =ᶠ[ae (Measure.map f μ)] g'
ι : Type ?u.2309729
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.2309741
R : Type ?u.2309744
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
⊢ Measure.map g (Measure.map f μ) = Measure.map g' (Measure.map f μ)
apply MeasureTheory.Measure.map_congr
no goals
case h
ι : Type ?u.2309729
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.2309741
R : Type ?u.2309744
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
⊢ g =ᶠ[ae (Measure.map f μ)] g'
exact hg.ae_eq_mk
case h
ι : Type ?u.2309729
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.2309741
R : Type ?u.2309744
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
A : Measure.map g (Measure.map f μ) = Measure.map g' (Measure.map f μ)
⊢ g ∘ f =ᶠ[ae μ] g' ∘ f
ι : Type ?u.2309729
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.2309741
R : Type ?u.2309744
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
A : Measure.map g (Measure.map f μ) = Measure.map g' (Measure.map f μ)
⊢ Measure.map (g ∘ f) μ = Measure.map (g' ∘ f) μ
apply MeasureTheory.Measure.map_congr
no goals
case h
ι : Type ?u.2309729
α : Type u_3
β : Type u_1
γ : Type u_2
δ : Type ?u.2309741
R : Type ?u.2309744
m0 : MeasurableSpace α
inst✝² : MeasurableSpace β
inst✝¹ : MeasurableSpace γ
inst✝ : MeasurableSpace δ
f✝ g✝ : α → β
μ ν : MeasureTheory.Measure α
g : β → γ
f : α → β
hg : AEMeasurable g
hf : AEMeasurable f
s : Set γ
hs : MeasurableSet s
g' : β → γ := mk g hg
A : Measure.map g (Measure.map f μ) = Measure.map g' (Measure.map f μ)
⊢ g ∘ f =ᶠ[ae μ] g' ∘ f
exact ae_of_ae_map hf hg.ae_eq_mk