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

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 g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f) s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑g) s μ
hfg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable (↑↑f) μ
hg_meas : AEStronglyMeasurable (↑↑g) μ
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ∫ (a : α) in s, (↑↑f - ↑↑g) a ∂μ = 0

Tactic:
rw [integral_sub' (hf_int_finite s hs hμs) (hg_int_finite s hs hμs)]

Result:
α : 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 g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f) s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑g) s μ
hfg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable (↑↑f) μ
hg_meas : AEStronglyMeasurable (↑↑g) μ
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ∫ (a : α) in s, ↑↑f a ∂μ - ∫ (a : α) in s, ↑↑g a ∂μ = 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 g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f) s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑g) s μ
hfg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable (↑↑f) μ
hg_meas : AEStronglyMeasurable (↑↑g) μ
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ∫ (a : α) in s, ↑↑f a ∂μ - ∫ (a : α) in s, ↑↑g a ∂μ = 0

Tactic:
exact sub_eq_zero.mpr (hfg s hs hμs)

Result:
no goals

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 g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f) s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑g) s μ
hfg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable (↑↑f) μ
hg_meas : AEStronglyMeasurable (↑↑g) μ
hfg' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑(f - g) x ∂μ = 0
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ IntegrableOn (↑↑(f - g)) s μ

Tactic:
rw [IntegrableOn, integrable_congr (ae_restrict_of_ae (Lp.coeFn_sub f g))]

Result:
α : 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 g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f) s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑g) s μ
hfg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable (↑↑f) μ
hg_meas : AEStronglyMeasurable (↑↑g) μ
hfg' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑(f - g) x ∂μ = 0
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ Integrable (↑↑f - ↑↑g) (μ.restrict s)

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 g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f) s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑g) s μ
hfg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable (↑↑f) μ
hg_meas : AEStronglyMeasurable (↑↑g) μ
⊢ ↑↑(f - g) =ᶠ[ae μ] 0

Tactic:
have hfg' : ∀ s : Set α, MeasurableSet[m] s → μ s < ∞ → (∫ x in s, (f - g) x ∂μ) = 0 := by
  intro s hs hμs
  rw [integral_congr_ae (ae_restrict_of_ae (Lp.coeFn_sub f g))]
  rw [integral_sub' (hf_int_finite s hs hμs) (hg_int_finite s hs hμs)]
  exact sub_eq_zero.mpr (hfg s hs hμs)

Result:
α : 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 g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f) s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑g) s μ
hfg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable (↑↑f) μ
hg_meas : AEStronglyMeasurable (↑↑g) μ
hfg' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑(f - g) x ∂μ = 0
⊢ ↑↑(f - g) =ᶠ[ae μ] 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 g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f) s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑g) s μ
hfg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable (↑↑f) μ
hg_meas : AEStronglyMeasurable (↑↑g) μ
⊢ ↑↑f =ᶠ[ae μ] ↑↑g

Tactic:
suffices h_sub : ⇑(f - g) =ᵐ[μ] 0 by
  rw [← sub_ae_eq_zero]; exact (Lp.coeFn_sub f g).symm.trans h_sub

Result:
α : 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 g : ↥(Lp E' p μ)
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑f) s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (↑↑g) s μ
hfg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, ↑↑f x ∂μ = ∫ (x : α) in s, ↑↑g x ∂μ
hf_meas : AEStronglyMeasurable (↑↑f) μ
hg_meas : AEStronglyMeasurable (↑↑g) μ
⊢ ↑↑(f - g) =ᶠ[ae μ] 0