-- Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
/-- If the restriction to a set `s` of a σ-algebra `m` is included in the restriction to `s` of
another σ-algebra `m₂` (hypothesis `hs`), the set `s` is `m` measurable and a function `f` almost
everywhere supported on `s` is `m`-ae-strongly-measurable, then `f` is also
`m₂`-ae-strongly-measurable. -/
lemma of_measurableSpace_le_on {m' m₀ : MeasurableSpace α} {μ : Measure[m₀] α} [Zero β]
    (hm : m ≤ m₀) {s : Set α} (hs_m : MeasurableSet[m] s)
    (hs : ∀ t, MeasurableSet[m] (s ∩ t) → MeasurableSet[m'] (s ∩ t))
    (hf : AEStronglyMeasurable[m] f μ) (hf_zero : f =ᵐ[μ.restrict sᶜ] 0) :
    AEStronglyMeasurable[m'] f μ

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst✝ : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
x : α
hx : f x = AEStronglyMeasurable.mk f hf x
hxs : x ∉ s
⊢ s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x

Tactic:
simp [hxs]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst✝ : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
h_ind_eq : s.indicator (AEStronglyMeasurable.mk f hf) =ᶠ[ae μ] f
⊢ AEStronglyMeasurable f μ

Tactic:
suffices StronglyMeasurable[m'] (s.indicator (hf.mk f)) from
  this.aestronglyMeasurable.congr h_ind_eq

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst✝ : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
h_ind_eq : s.indicator (AEStronglyMeasurable.mk f hf) =ᶠ[ae μ] f
⊢ StronglyMeasurable (s.indicator (AEStronglyMeasurable.mk f hf))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst✝ : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
⊢ s.indicator (AEStronglyMeasurable.mk f hf) =ᶠ[ae μ] f

Tactic:
refine Filter.EventuallyEq.trans ?_ <|
  indicator_ae_eq_of_restrict_compl_ae_eq_zero (hm _ hs_m) hf_zero

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst✝ : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
⊢ s.indicator (AEStronglyMeasurable.mk f hf) =ᶠ[ae μ] s.indicator f

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst✝ : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
⊢ s.indicator (AEStronglyMeasurable.mk f hf) =ᶠ[ae μ] s.indicator f

Tactic:
filter_upwards [hf.ae_eq_mk] with x hx

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst✝ : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
x : α
hx : f x = AEStronglyMeasurable.mk f hf x
⊢ s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst✝ : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
x : α
hx : f x = AEStronglyMeasurable.mk f hf x
hxs : x ∈ s
⊢ s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x

Tactic:
simp [hxs, hx]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst✝ : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
x : α
hx : f x = AEStronglyMeasurable.mk f hf x
⊢ s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x

Tactic:
by_cases hxs : x ∈ s

Result:
case pos
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst✝ : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
x : α
hx : f x = AEStronglyMeasurable.mk f hf x
hxs : x ∈ s
⊢ s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x

case neg
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst✝ : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
x : α
hx : f x = AEStronglyMeasurable.mk f hf x
hxs : x ∉ s
⊢ s.indicator (AEStronglyMeasurable.mk f hf) x = s.indicator f x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m : MeasurableSpace α
f : α → β
m' m₀ : MeasurableSpace α
μ : Measure α
inst✝ : Zero β
hm : m ≤ m₀
s : Set α
hs_m : MeasurableSet s
hs : ∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)
hf : AEStronglyMeasurable f μ
hf_zero : f =ᶠ[ae (μ.restrict sᶜ)] 0
h_ind_eq : s.indicator (AEStronglyMeasurable.mk f hf) =ᶠ[ae μ] f
⊢ StronglyMeasurable (s.indicator (AEStronglyMeasurable.mk f hf))

Tactic:
exact (hf.stronglyMeasurable_mk.indicator hs_m).stronglyMeasurable_of_measurableSpace_le_on hs_m
  hs fun x hxs => Set.indicator_of_not_mem hxs _

Result:
no goals