-- Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
theorem Integrable.ae_eq_zero_of_forall_setIntegral_eq_zero {f : α → E} (hf : Integrable f μ)
    (hf_zero : ∀ s, MeasurableSet s → μ s < ∞ → ∫ x in s, f x ∂μ = 0) : f =ᵐ[μ] 0

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0
hf_Lp : MemLp f 1 μ
f_Lp : ↥(Lp E 1 μ) := MemLp.toLp f hf_Lp
⊢ f =ᶠ[ae μ] 0

Tactic:
have hf_f_Lp : f =ᵐ[μ] f_Lp := (MemLp.coeFn_toLp hf_Lp).symm

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0
hf_Lp : MemLp f 1 μ
f_Lp : ↥(Lp E 1 μ) := MemLp.toLp f hf_Lp
hf_f_Lp : f =ᶠ[ae μ] ↑↑f_Lp
⊢ f =ᶠ[ae μ] 0

Proof state:
case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0
hf_Lp : MemLp f 1 μ
f_Lp : ↥(Lp E 1 μ) := MemLp.toLp f hf_Lp
hf_f_Lp : f =ᶠ[ae μ] ↑↑f_Lp
⊢ ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f_Lp x ∂μ = 0

Tactic:
intro s hs hμs

Result:
case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0
hf_Lp : MemLp f 1 μ
f_Lp : ↥(Lp E 1 μ) := MemLp.toLp f hf_Lp
hf_f_Lp : f =ᶠ[ae μ] ↑↑f_Lp
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ∫ (x : α) in s, ↑↑f_Lp x ∂μ = 0

Proof state:
case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0
hf_Lp : MemLp f 1 μ
f_Lp : ↥(Lp E 1 μ) := MemLp.toLp f hf_Lp
hf_f_Lp : f =ᶠ[ae μ] ↑↑f_Lp
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ∫ (a : α) in s, f a ∂μ = 0

Tactic:
exact hf_zero s hs hμs

Result:
no goals

Proof state:
case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0
hf_Lp : MemLp f 1 μ
f_Lp : ↥(Lp E 1 μ) := MemLp.toLp f hf_Lp
hf_f_Lp : f =ᶠ[ae μ] ↑↑f_Lp
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ∫ (x : α) in s, ↑↑f_Lp x ∂μ = 0

Tactic:
rw [integral_congr_ae (ae_restrict_of_ae hf_f_Lp.symm)]

Result:
case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0
hf_Lp : MemLp f 1 μ
f_Lp : ↥(Lp E 1 μ) := MemLp.toLp f hf_Lp
hf_f_Lp : f =ᶠ[ae μ] ↑↑f_Lp
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ∫ (a : α) in s, f a ∂μ = 0

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0
⊢ f =ᶠ[ae μ] 0

Tactic:
have hf_Lp : MemLp f 1 μ := memLp_one_iff_integrable.mpr hf

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0
hf_Lp : MemLp f 1 μ
⊢ f =ᶠ[ae μ] 0

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0
hf_Lp : MemLp f 1 μ
⊢ f =ᶠ[ae μ] 0

Tactic:
let f_Lp := hf_Lp.toLp f

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0
hf_Lp : MemLp f 1 μ
f_Lp : ↥(Lp E 1 μ) := MemLp.toLp f hf_Lp
⊢ f =ᶠ[ae μ] 0

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0
hf_Lp : MemLp f 1 μ
f_Lp : ↥(Lp E 1 μ) := MemLp.toLp f hf_Lp
hf_f_Lp : f =ᶠ[ae μ] ↑↑f_Lp
⊢ ↑↑f_Lp =ᶠ[ae μ] 0

Tactic:
refine Lp.ae_eq_zero_of_forall_setIntegral_eq_zero f_Lp one_ne_zero ENNReal.coe_ne_top ?_ ?_

Result:
case refine_1
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0
hf_Lp : MemLp f 1 μ
f_Lp : ↥(Lp E 1 μ) := MemLp.toLp f hf_Lp
hf_f_Lp : f =ᶠ[ae μ] ↑↑f_Lp
⊢ ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f_Lp) s μ

case refine_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0
hf_Lp : MemLp f 1 μ
f_Lp : ↥(Lp E 1 μ) := MemLp.toLp f hf_Lp
hf_f_Lp : f =ᶠ[ae μ] ↑↑f_Lp
⊢ ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f_Lp x ∂μ = 0

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0
hf_Lp : MemLp f 1 μ
f_Lp : ↥(Lp E 1 μ) := MemLp.toLp f hf_Lp
hf_f_Lp : f =ᶠ[ae μ] ↑↑f_Lp
⊢ f =ᶠ[ae μ] 0

Tactic:
refine hf_f_Lp.trans ?_

Result:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0
hf_Lp : MemLp f 1 μ
f_Lp : ↥(Lp E 1 μ) := MemLp.toLp f hf_Lp
hf_f_Lp : f =ᶠ[ae μ] ↑↑f_Lp
⊢ ↑↑f_Lp =ᶠ[ae μ] 0

Proof state:
case refine_1
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : α → E
hf : Integrable f μ
hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0
hf_Lp : MemLp f 1 μ
f_Lp : ↥(Lp E 1 μ) := MemLp.toLp f hf_Lp
hf_f_Lp : f =ᶠ[ae μ] ↑↑f_Lp
⊢ ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f_Lp) s μ

Tactic:
exact fun s _ _ => Integrable.integrableOn (L1.integrable_coeFn _)

Result:
no goals