-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Unique.lean
theorem ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' (hm : m ≤ m0) [SigmaFinite (μ.trim hm)]
    {f g : α → F'} (hf_int_finite : ∀ s, MeasurableSet[m] s → μ s < ∞ → IntegrableOn f s μ)
    (hg_int_finite : ∀ s, MeasurableSet[m] s → μ s < ∞ → IntegrableOn g s μ)
    (hfg_eq : ∀ s : Set α, MeasurableSet[m] s → μ s < ∞ → ∫ x in s, f x ∂μ = ∫ x in s, g x ∂μ)
    (hfm : AEStronglyMeasurable[m] f μ) (hgm : AEStronglyMeasurable[m] g μ) : f =ᵐ[μ] g

Proof state:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
hg_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)
⊢ AEStronglyMeasurable.mk f hfm =ᶠ[ae (μ.trim hm)] AEStronglyMeasurable.mk g hgm

Tactic:
have hfg_mk_eq :
  ∀ s : Set α,
    MeasurableSet[m] s →
      μ.trim hm s < ∞ → ∫ x in s, hfm.mk f x ∂μ.trim hm = ∫ x in s, hgm.mk g x ∂μ.trim hm := by
  intro s hs hμs
  rw [trim_measurableSet_eq hm hs] at hμs
  rw [restrict_trim hm _ hs, ← integral_trim hm hfm.stronglyMeasurable_mk, ←
    integral_trim hm hgm.stronglyMeasurable_mk,
    integral_congr_ae (ae_restrict_of_ae hfm.ae_eq_mk.symm),
    integral_congr_ae (ae_restrict_of_ae hgm.ae_eq_mk.symm)]
  exact hfg_eq s hs hμs

Result:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
hg_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)
hfg_mk_eq :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ.trim hm) s < ⊤ →
        ∫ (x : α) in s, AEStronglyMeasurable.mk f hfm x ∂μ.trim hm =
          ∫ (x : α) in s, AEStronglyMeasurable.mk g hgm x ∂μ.trim hm
⊢ AEStronglyMeasurable.mk f hfm =ᶠ[ae (μ.trim hm)] AEStronglyMeasurable.mk g hgm

Proof state:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ Integrable (AEStronglyMeasurable.mk g hgm) ((μ.restrict s).trim hm)

Tactic:
refine Integrable.trim hm ?_ hgm.stronglyMeasurable_mk

Result:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ Integrable (AEStronglyMeasurable.mk g hgm) (μ.restrict s)

Proof state:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
hg_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ∫ (x : α) in s, AEStronglyMeasurable.mk f hfm x ∂μ.trim hm =
    ∫ (x : α) in s, AEStronglyMeasurable.mk g hgm x ∂μ.trim hm

Tactic:
rw [restrict_trim hm _ hs, ← integral_trim hm hfm.stronglyMeasurable_mk, ←
  integral_trim hm hgm.stronglyMeasurable_mk,
  integral_congr_ae (ae_restrict_of_ae hfm.ae_eq_mk.symm),
  integral_congr_ae (ae_restrict_of_ae hgm.ae_eq_mk.symm)]

Result:
α : Type u_1
F' : Type u_3
m m0 : MeasurableSpace α
μ : Measure α
inst✝³ : NormedAddCommGroup F'
inst✝² : NormedSpace ℝ F'
inst✝¹ : CompleteSpace F'
hm : m ≤ m0
inst✝ : SigmaFinite (μ.trim hm)
f g : α → F'
hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ
hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ
hfg_eq : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ
hfm : AEStronglyMeasurable f μ
hgm : AEStronglyMeasurable g μ
hf_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable.mk f hfm) s (μ.trim hm)
hg_mk_int_finite :
  ∀ (s : Set α), MeasurableSet s → (μ.trim hm) s < ⊤ → IntegrableOn (AEStronglyMeasurable.mk g hgm) s (μ.trim hm)
s : Set α
hs : MeasurableSet s
hμs : μ s < ⊤
⊢ ∫ (a : α) in s, f a ∂μ = ∫ (a : α) in s, g a ∂μ