-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
theorem MeasureTheory.Measure.restrict_map_of_aemeasurable {f : α → δ} (hf : AEMeasurable f μ)
    {s : Set δ} (hs : MeasurableSet s) : (μ.map f).restrict s = (μ.restrict <| f ⁻¹' s).map f :=
  calc
    (μ.map f).restrict s = (μ.map (hf.mk f)).restrict s

Proof state:
case h
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
⊢ μ.restrict (AEMeasurable.mk f hf ⁻¹' s) = μ.restrict (f ⁻¹' s)

Tactic:
ext1 t ht

Result:
case h.h
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ : Measure α
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

Proof state:
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
⊢ map f (μ.restrict (AEMeasurable.mk f hf ⁻¹' s)) = map f (μ.restrict (f ⁻¹' s))

Tactic:
apply congr_arg

Result:
case h
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
⊢ μ.restrict (AEMeasurable.mk f hf ⁻¹' s) = μ.restrict (f ⁻¹' s)

Proof state:
case e_μ
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
⊢ map f μ = map (AEMeasurable.mk f hf) μ

Tactic:
apply Measure.map_congr hf.ae_eq_mk

Result:
no goals

Proof state:
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
⊢ (map f μ).restrict s = (map (AEMeasurable.mk f hf) μ).restrict s

Tactic:
congr 1

Result:
case e_μ
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
⊢ map f μ = map (AEMeasurable.mk f hf) μ

Proof state:
case h.h.H
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ t ∩ AEMeasurable.mk f hf ⁻¹' s =ᶠ[ae μ] t ∩ f ⁻¹' s

Tactic:
apply (EventuallyEq.refl _ _).inter (hf.ae_eq_mk.symm.preimage s)

Result:
no goals

Proof state:
case h.h
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ : Measure α
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

Tactic:
simp only [ht, Measure.restrict_apply]

Result:
case h.h
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ μ (t ∩ AEMeasurable.mk f hf ⁻¹' s) = μ (t ∩ f ⁻¹' s)

Proof state:
case h.h
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ μ (t ∩ AEMeasurable.mk f hf ⁻¹' s) = μ (t ∩ f ⁻¹' s)

Tactic:
apply measure_congr

Result:
case h.h.H
α : Type u_2
δ : Type u_5
m0 : MeasurableSpace α
inst✝ : MeasurableSpace δ
μ : Measure α
f : α → δ
hf : AEMeasurable f μ
s : Set δ
hs : MeasurableSet s
t : Set α
ht : MeasurableSet t
⊢ t ∩ AEMeasurable.mk f hf ⁻¹' s =ᶠ[ae μ] t ∩ f ⁻¹' s