-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Unique.lean
theorem lpMeas.ae_eq_zero_of_forall_setIntegral_eq_zero (hm : m ≤ m0) (f : lpMeas E' 𝕜 m p μ)
    (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞)
    (hf_int_finite : ∀ s, MeasurableSet[m] s → μ s < ∞ → IntegrableOn (f : Lp E' p μ) s μ)
    (hf_zero : ∀ s : Set α, MeasurableSet[m] s → μ s < ∞ → ∫ x in s, (f : Lp E' p μ) x ∂μ = 0) :
    f =ᵐ[μ] (0 : α → E')

Proof state:
case intro.intro.refine_2
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑↑f) s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : ↑↑↑f =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
hfg_restrict : ↑↑↑f =ᶠ[ae (μ.restrict s)] g
⊢ ∫ (a : α) in s, ↑↑↑f a ∂μ = 0

Tactic:
exact hf_zero s hs hμs

Result:
no goals

Proof state:
case intro.intro.refine_1
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑↑f) s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : ↑↑↑f =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
hfg_restrict : ↑↑↑f =ᶠ[ae (μ.restrict s)] g
⊢ Integrable (↑↑↑f) (μ.restrict s)

Tactic:
exact hf_int_finite s hs hμs

Result:
no goals

Proof state:
case intro.intro.refine_2
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑↑f) s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : ↑↑↑f =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ∫ (x : α) in s, g x ∂μ = 0

Tactic:
have hfg_restrict : f =ᵐ[μ.restrict s] g := ae_restrict_of_ae hfg

Result:
case intro.intro.refine_2
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑↑f) s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : ↑↑↑f =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
hfg_restrict : ↑↑↑f =ᶠ[ae (μ.restrict s)] g
⊢ ∫ (x : α) in s, g x ∂μ = 0

Proof state:
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑↑f) s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
⊢ ↑↑↑f =ᶠ[ae μ] 0

Tactic:
obtain ⟨g, hg_sm, hfg⟩ := lpMeas.ae_fin_strongly_measurable' hm f hp_ne_zero hp_ne_top

Result:
case intro.intro
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑↑f) s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : ↑↑↑f =ᶠ[ae μ] g
⊢ ↑↑↑f =ᶠ[ae μ] 0

Proof state:
case intro.intro.refine_1
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑↑f) s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : ↑↑↑f =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
hfg_restrict : ↑↑↑f =ᶠ[ae (μ.restrict s)] g
⊢ IntegrableOn g s μ

Tactic:
rw [IntegrableOn, integrable_congr hfg_restrict.symm]

Result:
case intro.intro.refine_1
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑↑f) s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : ↑↑↑f =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
hfg_restrict : ↑↑↑f =ᶠ[ae (μ.restrict s)] g
⊢ Integrable (↑↑↑f) (μ.restrict s)

Proof state:
case intro.intro.refine_2
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑↑f) s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : ↑↑↑f =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
hfg_restrict : ↑↑↑f =ᶠ[ae (μ.restrict s)] g
⊢ ∫ (x : α) in s, g x ∂μ = 0

Tactic:
rw [integral_congr_ae hfg_restrict.symm]

Result:
case intro.intro.refine_2
α : Type u_1
E' : Type u_2
𝕜 : Type u_4
p : ℝ≥0∞
m m0 : MeasurableSpace α
μ : Measure α
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E'
inst✝² : InnerProductSpace 𝕜 E'
inst✝¹ : CompleteSpace E'
inst✝ : NormedSpace ℝ E'
hm : m ≤ m0
f : ↥(lpMeas E' 𝕜 m p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑↑f) s μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑↑f x ∂μ = 0
g : α → E'
hg_sm : FinStronglyMeasurable g (μ.trim hm)
hfg : ↑↑↑f =ᶠ[ae μ] g
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
hfg_restrict : ↑↑↑f =ᶠ[ae (μ.restrict s)] g
⊢ ∫ (a : α) in s, ↑↑↑f a ∂μ = 0