-- Mathlib/MeasureTheory/Function/AEEqOfLIntegral.lean
theorem AEMeasurable.ae_eq_of_forall_setLIntegral_eq {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ)
    (hg : AEMeasurable g μ) (hfi : ∫⁻ x, f x ∂μ ≠ ∞) (hgi : ∫⁻ x, g x ∂μ ≠ ∞)
    (hfg : ∀ ⦃s⦄, MeasurableSet s → μ s < ∞ → ∫⁻ x in s, f x ∂μ = ∫⁻ x in s, g x ∂μ) :
    f =ᵐ[μ] g

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᶠ[ae (μ.restrict (s ∪ t))] g
h1 : f =ᶠ[ae (μ.restrict sᶜ)] 0
h2 : g =ᶠ[ae (μ.restrict tᶜ)] 0
⊢ ∀ᵐ (x : α) ∂μ.restrict (sᶜ ∩ tᶜ), f x = g x

Tactic:
rw [ae_restrict_iff' (hf'.measurableSet.compl.inter hg'.measurableSet.compl)]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᶠ[ae (μ.restrict (s ∪ t))] g
h1 : f =ᶠ[ae (μ.restrict sᶜ)] 0
h2 : g =ᶠ[ae (μ.restrict tᶜ)] 0
⊢ ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ → f x = g x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
⊢ f =ᶠ[ae μ] g

Tactic:
suffices f =ᵐ[μ.restrict (s ∪ t)] g by
  refine ae_of_ae_restrict_of_ae_restrict_compl _ this ?_
  simp only [Set.compl_union]
  have h1 : f =ᵐ[μ.restrict sᶜ] 0 := hf'.ae_eq_zero_compl
  have h2 : g =ᵐ[μ.restrict tᶜ] 0 := hg'.ae_eq_zero_compl
  rw [ae_restrict_iff' (hf'.measurableSet.compl.inter hg'.measurableSet.compl)]
  rw [EventuallyEq, ae_restrict_iff' hf'.measurableSet.compl] at h1
  rw [EventuallyEq, ae_restrict_iff' hg'.measurableSet.compl] at h2
  filter_upwards [h1, h2] with x h1 h2 hx
  rw [h1 (Set.inter_subset_left hx), h2 (Set.inter_subset_right hx)]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
⊢ f =ᶠ[ae (μ.restrict (s ∪ t))] g

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᶠ[ae (μ.restrict (s ∪ t))] g
h1 : ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ → f x = 0 x
h2 : g =ᶠ[ae (μ.restrict tᶜ)] 0
⊢ ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ → f x = g x

Tactic:
rw [EventuallyEq, ae_restrict_iff' hg'.measurableSet.compl] at h2

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᶠ[ae (μ.restrict (s ∪ t))] g
h1 : ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ → f x = 0 x
h2 : ∀ᵐ (x : α) ∂μ, x ∈ hg'.sigmaFiniteSetᶜ → g x = 0 x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ → f x = g x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
⊢ f =ᶠ[ae μ] g

Tactic:
let s := hf'.sigmaFiniteSet

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
⊢ f =ᶠ[ae μ] g

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᶠ[ae (μ.restrict (s ∪ t))] g
h1 : f =ᶠ[ae (μ.restrict sᶜ)] 0
h2 : g =ᶠ[ae (μ.restrict tᶜ)] 0
⊢ ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ → f x = g x

Tactic:
rw [EventuallyEq, ae_restrict_iff' hf'.measurableSet.compl] at h1

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᶠ[ae (μ.restrict (s ∪ t))] g
h1 : ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ → f x = 0 x
h2 : g =ᶠ[ae (μ.restrict tᶜ)] 0
⊢ ∀ᵐ (x : α) ∂μ, x ∈ hf'.sigmaFiniteSetᶜ ∩ hg'.sigmaFiniteSetᶜ → f x = g x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᶠ[ae (μ.restrict (s ∪ t))] g
⊢ ∀ᵐ (x : α) ∂μ.restrict (s ∪ t)ᶜ, f x = g x

Tactic:
simp only [Set.compl_union]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hgi : ∫⁻ (x : α), g x ∂μ ≠ ⊤
hfg : ∀ ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
this : f =ᶠ[ae (μ.restrict (s ∪ t))] g
⊢ ∀ᵐ (x : α) ∂μ.restrict (sᶜ ∩ tᶜ), f x = g x