-- Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
theorem piecewise {s : Set α} [DecidablePred (· ∈ s)]
    (hs : MeasurableSet s) (hf : AEStronglyMeasurable f (μ.restrict s))
    (hg : AEStronglyMeasurable g (μ.restrict sᶜ)) :
    AEStronglyMeasurable (s.piecewise f g) μ

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = AEStronglyMeasurable.mk f hf x
x : α
hx : x ∈ s → f x = AEStronglyMeasurable.mk f hf x
hx_mem : x ∈ s
⊢ s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
simp only [hx_mem, Set.piecewise_eq_of_mem, hx hx_mem]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : f =ᶠ[ae (μ.restrict s)] AEStronglyMeasurable.mk f hf
⊢ ∀ᵐ (x : α) ∂μ.restrict s,
    s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
rw [Filter.EventuallyEq, ae_restrict_iff' hs] at h

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ s → f x = AEStronglyMeasurable.mk f hf x
⊢ ∀ᵐ (x : α) ∂μ.restrict s,
    s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
x : α
hx : x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
hx_mem : x ∈ sᶜ
⊢ s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
rw [Set.mem_compl_iff] at hx_mem

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
x : α
hx : x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
hx_mem : x ∉ s
⊢ s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Proof state:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
⊢ ∀ᵐ (x : α) ∂μ.restrict s,
    s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
have h := hf.ae_eq_mk

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : f =ᶠ[ae (μ.restrict s)] AEStronglyMeasurable.mk f hf
⊢ ∀ᵐ (x : α) ∂μ.restrict s,
    s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
⊢ ∀ᵐ (x : α) ∂μ.restrict sᶜ,
    s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
rw [ae_restrict_iff' hs.compl]

Result:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
⊢ ∀ᵐ (x : α) ∂μ,
    x ∈ sᶜ → s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
⊢ s.piecewise f g =ᶠ[ae μ] s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg)

Tactic:
refine ae_of_ae_restrict_of_ae_restrict_compl s ?_ ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
⊢ ∀ᵐ (x : α) ∂μ.restrict s,
    s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
⊢ ∀ᵐ (x : α) ∂μ.restrict sᶜ,
    s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
⊢ ∀ᵐ (x : α) ∂μ,
    x ∈ sᶜ → s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x

Tactic:
filter_upwards [h] with x hx

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f g : α → β
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
hs : MeasurableSet s
hf : AEStronglyMeasurable f (μ.restrict s)
hg : AEStronglyMeasurable g (μ.restrict sᶜ)
h : ∀ᵐ (x : α) ∂μ, x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
x : α
hx : x ∈ sᶜ → g x = AEStronglyMeasurable.mk g hg x
⊢ x ∈ sᶜ → s.piecewise f g x = s.piecewise (AEStronglyMeasurable.mk f hf) (AEStronglyMeasurable.mk g hg) x