-- Mathlib/MeasureTheory/Measure/Restrict.lean
lemma NullMeasurable.measure_preimage_eq_measure_restrict_preimage_of_ae_compl_eq_const
    {β : Type*} [MeasurableSpace β] {b : β} {f : α → β} {s : Set α}
    (f_mble : NullMeasurable f (μ.restrict s)) (hs : f =ᵐ[Measure.restrict μ sᶜ] (fun _ ↦ b))
    {t : Set β} (t_mble : MeasurableSet t) (ht : b ∉ t) :
    μ (f ⁻¹' t) = μ.restrict s (f ⁻¹' t)

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t) = μ (f ⁻¹' t ∩ s)

Tactic:
apply le_antisymm _ (measure_mono inter_subset_left)

Result:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t) ≤ μ (f ⁻¹' t ∩ s)

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t) ≤ μ (f ⁻¹' t ∩ s)

Tactic:
apply (measure_mono (Eq.symm (inter_union_compl (f ⁻¹' t) s)).le).trans

Result:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t ∩ s ∪ f ⁻¹' t ∩ sᶜ) ≤ μ (f ⁻¹' t ∩ s)

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : f =ᶠ[ae (μ.restrict sᶜ)] fun x => b
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t) = (μ.restrict s) (f ⁻¹' t)

Tactic:
rw [Measure.restrict_apply₀ (f_mble t_mble)]

Result:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : f =ᶠ[ae (μ.restrict sᶜ)] fun x => b
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t) = μ (f ⁻¹' t ∩ s)

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
x : α
hfx : f x = b
hx : f x ∈ t
⊢ False

Tactic:
exact ht (hfx ▸ hx)

Result:
no goals

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t ∩ s ∪ f ⁻¹' t ∩ sᶜ) ≤ μ (f ⁻¹' t ∩ s)

Tactic:
apply (measure_union_le _ _).trans

Result:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t ∩ s) + μ (f ⁻¹' t ∩ sᶜ) ≤ μ (f ⁻¹' t ∩ s)

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
obs : μ (f ⁻¹' t ∩ sᶜ) = 0
⊢ μ (f ⁻¹' t ∩ s) + μ (f ⁻¹' t ∩ sᶜ) ≤ μ (f ⁻¹' t ∩ s)

Tactic:
simp only [obs, add_zero, le_refl]

Result:
no goals

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
x : α
hx : x ∈ f ⁻¹' t
hfx : f x = b
⊢ False

Tactic:
simp only [mem_preimage, mem_setOf_eq] at hx hfx

Result:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
x : α
hfx : f x = b
hx : f x ∈ t
⊢ False

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t ∩ sᶜ) = 0

Tactic:
apply le_antisymm _ (zero_le _)

Result:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t ∩ sᶜ) ≤ 0

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t ∩ sᶜ) ≤ 0

Tactic:
rw [← hs]

Result:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t ∩ sᶜ) ≤ μ ({a | ¬f a = b} ∩ sᶜ)

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t ∩ sᶜ) ≤ μ ({a | ¬f a = b} ∩ sᶜ)

Tactic:
apply measure_mono (inter_subset_inter_left _ _)

Result:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ f ⁻¹' t ⊆ {a | ¬f a = b}

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ f ⁻¹' t ⊆ {a | ¬f a = b}

Tactic:
intro x hx hfx

Result:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
x : α
hx : x ∈ f ⁻¹' t
hfx : f x = b
⊢ False

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
⊢ μ (f ⁻¹' t ∩ s) + μ (f ⁻¹' t ∩ sᶜ) ≤ μ (f ⁻¹' t ∩ s)

Tactic:
have obs : μ ((f ⁻¹' t) ∩ sᶜ) = 0 := by
  apply le_antisymm _ (zero_le _)
  rw [← hs]
  apply measure_mono (inter_subset_inter_left _ _)
  intro x hx hfx
  simp only [mem_preimage, mem_setOf_eq] at hx hfx
  exact ht (hfx ▸ hx)

Result:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
β : Type u_7
inst✝ : MeasurableSpace β
b : β
f : α → β
s : Set α
f_mble : NullMeasurable f (μ.restrict s)
hs : μ ({a | ¬f a = b} ∩ sᶜ) = 0
t : Set β
t_mble : MeasurableSet t
ht : b ∉ t
obs : μ (f ⁻¹' t ∩ sᶜ) = 0
⊢ μ (f ⁻¹' t ∩ s) + μ (f ⁻¹' t ∩ sᶜ) ≤ μ (f ⁻¹' t ∩ s)