-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem QuasiMeasurePreserving.restrict {ν : Measure β} {f : α → β}
    (hf : QuasiMeasurePreserving f μ ν) {t : Set β} (hmaps : MapsTo f s t) :
    QuasiMeasurePreserving f (μ.restrict s) (ν.restrict t) where
  measurable := hf.measurable
  absolutelyContinuous

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
hu : ν (u ∩ t) = 0
⊢ f ⁻¹' u ∩ s ⊆ f ⁻¹' u ∩ f ⁻¹' t

Tactic:
gcongr

Result:
case H
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
hu : ν (u ∩ t) = 0
⊢ s ⊆ f ⁻¹' t

Proof state:
case H
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
hu : ν (u ∩ t) = 0
⊢ s ⊆ f ⁻¹' t

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
⊢ map f (μ.restrict s) ≪ ν.restrict t

Tactic:
refine AbsolutelyContinuous.mk fun u hum ↦ ?_

Result:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
⊢ (ν.restrict t) u = 0 → (map f (μ.restrict s)) u = 0

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
hu : ν (u ∩ t) = 0
⊢ f ⁻¹' u ∩ s ⊆ f ⁻¹' (u ∩ t)

Tactic:
rw [preimage_inter]

Result:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
hu : ν (u ∩ t) = 0
⊢ f ⁻¹' u ∩ s ⊆ f ⁻¹' u ∩ f ⁻¹' t

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
⊢ ν (u ∩ t) = 0 → μ (f ⁻¹' u ∩ s) = 0

Tactic:
refine fun hu ↦ measure_mono_null ?_ (hf.preimage_null hu)

Result:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
hu : ν (u ∩ t) = 0
⊢ f ⁻¹' u ∩ s ⊆ f ⁻¹' (u ∩ t)

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
this : ν (u ∩ t) = 0 → μ (f ⁻¹' u ∩ s) = 0
⊢ (ν.restrict t) u = 0 → (map f (μ.restrict s)) u = 0

Tactic:
simpa [hum, hf.measurable, hf.measurable hum]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
⊢ (ν.restrict t) u = 0 → (map f (μ.restrict s)) u = 0

Tactic:
suffices ν (u ∩ t) = 0 → μ (f ⁻¹' u ∩ s) = 0 by simpa [hum, hf.measurable, hf.measurable hum]

Result:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
s : Set α
ν : Measure β
f : α → β
hf : QuasiMeasurePreserving f μ ν
t : Set β
hmaps : MapsTo f s t
u : Set β
hum : MeasurableSet u
⊢ ν (u ∩ t) = 0 → μ (f ⁻¹' u ∩ s) = 0