-- Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
theorem _root_.aestronglyMeasurable_indicator_iff [Zero β] {s : Set α} (hs : MeasurableSet s) :
    AEStronglyMeasurable (indicator s f) μ ↔ AEStronglyMeasurable f (μ.restrict s)

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

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

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

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

Tactic:
exact ae_of_ae_restrict_of_ae_restrict_compl _ A B

Result:
no goals

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

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

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

Proof state:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEStronglyMeasurable f (μ.restrict s)
⊢ AEStronglyMeasurable (s.indicator f) μ

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

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

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEStronglyMeasurable (s.indicator f) μ
⊢ AEStronglyMeasurable f (μ.restrict s)

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

Result:
no goals

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEStronglyMeasurable (s.indicator f) μ → AEStronglyMeasurable f (μ.restrict s)

Tactic:
intro h

Result:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEStronglyMeasurable (s.indicator f) μ
⊢ AEStronglyMeasurable f (μ.restrict s)

Proof state:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEStronglyMeasurable f (μ.restrict s) → AEStronglyMeasurable (s.indicator f) μ

Tactic:
intro h

Result:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
h : AEStronglyMeasurable f (μ.restrict s)
⊢ AEStronglyMeasurable (s.indicator f) μ

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEStronglyMeasurable (s.indicator f) μ ↔ AEStronglyMeasurable f (μ.restrict s)

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEStronglyMeasurable (s.indicator f) μ → AEStronglyMeasurable f (μ.restrict s)

case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
inst✝ : Zero β
s : Set α
hs : MeasurableSet s
⊢ AEStronglyMeasurable f (μ.restrict s) → AEStronglyMeasurable (s.indicator f) μ