-- Mathlib/MeasureTheory/Measure/AEMeasurable.lean
theorem aemeasurable_indicator_iff {s} (hs : MeasurableSet s) :
    AEMeasurable (indicator s f) μ ↔ AEMeasurable f (μ.restrict s)

Proof state:
case mpr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f (μ.restrict s)
A : s.indicator f =ᶠ[ae (μ.restrict s)] s.indicator (AEMeasurable.mk f h)
B : s.indicator f =ᶠ[ae (μ.restrict sᶜ)] s.indicator (AEMeasurable.mk f h)
⊢ s.indicator f =ᶠ[ae μ] s.indicator (AEMeasurable.mk f h)

Tactic:
exact ae_of_ae_restrict_of_ae_restrict_compl _ A B

Result:
no goals

Proof state:
case mp
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable (s.indicator f) μ
⊢ AEMeasurable f (μ.restrict s)

Tactic:
exact (h.mono_measure Measure.restrict_le_self).congr (indicator_ae_eq_restrict hs)

Result:
no goals

Proof state:
case mpr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f (μ.restrict s) → AEMeasurable (s.indicator f) μ

Tactic:
intro h

Result:
case mpr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f (μ.restrict s)
⊢ AEMeasurable (s.indicator f) μ

Proof state:
case mpr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f (μ.restrict s)
A : s.indicator f =ᶠ[ae (μ.restrict s)] s.indicator (AEMeasurable.mk f h)
⊢ s.indicator f =ᶠ[ae μ] s.indicator (AEMeasurable.mk f h)

Tactic:
have B : s.indicator f =ᵐ[μ.restrict sᶜ] s.indicator (AEMeasurable.mk f h) :=
  (indicator_ae_eq_restrict_compl hs).trans (indicator_ae_eq_restrict_compl hs).symm

Result:
case mpr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f (μ.restrict s)
A : s.indicator f =ᶠ[ae (μ.restrict s)] s.indicator (AEMeasurable.mk f h)
B : s.indicator f =ᶠ[ae (μ.restrict sᶜ)] s.indicator (AEMeasurable.mk f h)
⊢ s.indicator f =ᶠ[ae μ] s.indicator (AEMeasurable.mk f h)

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable (s.indicator f) μ ↔ AEMeasurable f (μ.restrict s)

Tactic:
constructor

Result:
case mp
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable (s.indicator f) μ → AEMeasurable f (μ.restrict s)

case mpr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable f (μ.restrict s) → AEMeasurable (s.indicator f) μ

Proof state:
case mpr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f (μ.restrict s)
⊢ s.indicator f =ᶠ[ae μ] s.indicator (AEMeasurable.mk f h)

Tactic:
have A : s.indicator f =ᵐ[μ.restrict s] s.indicator (AEMeasurable.mk f h) :=
  (indicator_ae_eq_restrict hs).trans (h.ae_eq_mk.trans <| (indicator_ae_eq_restrict hs).symm)

Result:
case mpr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f (μ.restrict s)
A : s.indicator f =ᶠ[ae (μ.restrict s)] s.indicator (AEMeasurable.mk f h)
⊢ s.indicator f =ᶠ[ae μ] s.indicator (AEMeasurable.mk f h)

Proof state:
case mpr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f (μ.restrict s)
⊢ AEMeasurable (s.indicator f) μ

Tactic:
refine ⟨indicator s (h.mk f), h.measurable_mk.indicator hs, ?_⟩

Result:
case mpr
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable f (μ.restrict s)
⊢ s.indicator f =ᶠ[ae μ] s.indicator (AEMeasurable.mk f h)

Proof state:
case mp
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEMeasurable (s.indicator f) μ → AEMeasurable f (μ.restrict s)

Tactic:
intro h

Result:
case mp
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
f : α → β
μ : Measure α
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEMeasurable (s.indicator f) μ
⊢ AEMeasurable f (μ.restrict s)