awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : 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 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (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

Tactic:
ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ hf.restrict hg.restrict
    fun u hu huμ ↦ ?_

Premises used: AEMeasurable.restrict, MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : 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 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
refine :
  ∀ (u : Set α) (hu : MeasurableSet u)
    (huμ : LT.lt (α := ℝ≥0∞) ((μ.restrict (s ∪ t) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)),
    ∫⁻ (x : α) in u, f x ∂μ.restrict (s ∪ t) = ∫⁻ (x : α) in u, g x ∂μ.restrict (s ∪ t)
⊢ f =ᶠ[ae (μ.restrict (s ∪ t))] g

Tactic:
refine ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ hf.restrict hg.restrict
    fun u hu huμ ↦ ?_

Premises used: AEMeasurable.restrict, MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : 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 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
u : Set α
hu : MeasurableSet u
huμ : LT.lt (α := ℝ≥0∞) ((μ.restrict (s ∪ t) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : ∫⁻ (x : α) in u ∩ (s ∪ t), f x ∂μ = ∫⁻ (x : α) in u ∩ (s ∪ t), g x ∂μ
⊢ ∫⁻ (x : α) in u, f x ∂μ.restrict (s ∪ t) = ∫⁻ (x : α) in u, g x ∂μ.restrict (s ∪ t)

Tactic:
rw [Measure.restrict_restrict hu]

Premises used: MeasureTheory.Measure.restrict_restrict
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : 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 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
u : Set α
hu : MeasurableSet u
huμ : LT.lt (α := ℝ≥0∞) ((μ.restrict (s ∪ t) : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ (s ∪ t)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [Measure.restrict_apply hu] at huμ

Premises used: MeasureTheory.Measure.restrict_apply
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : 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 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
u : Set α
hu : MeasurableSet u
huμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ (s ∪ t)) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in u ∩ (s ∪ t), f x ∂μ = ∫⁻ (x : α) in u ∩ (s ∪ t), g x ∂μ

Tactic:
hfg (hu.inter (hf'.measurableSet.union hg'.measurableSet)) huμ

Premises used: MeasureTheory.AEFinStronglyMeasurable.measurableSet, MeasurableSet.union, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : 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 →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
hf' : AEFinStronglyMeasurable f μ
hg' : AEFinStronglyMeasurable g μ
s : Set α := hf'.sigmaFiniteSet
t : Set α := hg'.sigmaFiniteSet
u : Set α
hu : MeasurableSet u
huμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ (s ∪ t)) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in u ∩ (s ∪ t), f x ∂μ = ∫⁻ (x : α) in u ∩ (s ∪ t), g x ∂μ

Tactic:
exact hfg (hu.inter (hf'.measurableSet.union hg'.measurableSet)) huμ

Premises used: MeasureTheory.AEFinStronglyMeasurable.measurableSet, MeasurableSet.union, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ ∀ (t : Set α), MeasurableSet t → ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ

Tactic:
MeasurableSpace.induction_on_inter h_eq h_inter ?_ basic ?_ ?_

Premises used: MeasurableSpace.induction_on_inter
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
refine_1 : ∫⁻ (x : α) in ∅, f x ∂μ = ∫⁻ (x : α) in ∅, g x ∂μ
refine_2 :
  ∀ (t : Set α) (htm : MeasurableSet t),
    ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ → ∫⁻ (x : α) in tᶜ, f x ∂μ = ∫⁻ (x : α) in tᶜ, g x ∂μ
refine_3 :
  ∀ (f_1 : ℕ → Set α),
    Pairwise (Function.onFun Disjoint f_1) →
      ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f_1 i)),
        (∀ (i : ℕ), ∫⁻ (x : α) in f_1 i, f x ∂μ = ∫⁻ (x : α) in f_1 i, g x ∂μ) →
          ∫⁻ (x : α) in ⋃ (i : ℕ), f_1 i, f x ∂μ = ∫⁻ (x : α) in ⋃ (i : ℕ), f_1 i, g x ∂μ
⊢ ∀ (t : Set α), MeasurableSet t → ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ

Tactic:
refine MeasurableSpace.induction_on_inter h_eq h_inter ?_ basic ?_ ?_
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
⊢ ∫⁻ (x : α) in ∅, f x ∂μ = ∫⁻ (x : α) in ∅, g x ∂μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq_1 : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
refine_2 : ∫⁻ (x : α) in t, g x ∂μ ≠ ∞
refine_2₁ : ∫⁻ (x : α) in t, f x ∂μ ≠ ∞
⊢ ∫⁻ (x : α) in tᶜ, f x ∂μ = ∫⁻ (x : α) in tᶜ, g x ∂μ

Tactic:
rw [setLIntegral_compl ht, setLIntegral_compl ht, h_eq, h_univ]

Premises used: MeasureTheory.setLIntegral_compl
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq_1 : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
⊢ ∫⁻ (x : α) in t, g x ∂μ ≠ ∞

Tactic:
ne_of_lt ?_

Premises used: ne_of_lt
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq_1 : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
refine_2 : ∫⁻ (x : α) in t, g x ∂μ < ∞
⊢ ∫⁻ (x : α) in t, g x ∂μ ≠ ∞

Tactic:
refine ne_of_lt ?_

Premises used: ne_of_lt
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq_1 : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
⊢ ∫⁻ (x : α) in t, g x ∂μ ≤ ∫⁻ (x : α), g x ∂μ

Tactic:
setLIntegral_le_lintegral t _

Premises used: MeasureTheory.setLIntegral_le_lintegral
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq_1 : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
rw : ∫⁻ (x : α), f x ∂μ < ∞
⊢ ∫⁻ (x : α), g x ∂μ < ∞

Tactic:
rw [← h_univ]
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq_1 : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
⊢ ∫⁻ (x : α), f x ∂μ < ∞

Tactic:
hf_int.lt_top

Premises used: Ne.lt_top
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq_1 : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
⊢ ∫⁻ (x : α), f x ∂μ < ∞

Tactic:
exact hf_int.lt_top

Premises used: Ne.lt_top
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq_1 : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
calc : ∫⁻ (x : α), g x ∂μ < ∞
⊢ ∫⁻ (x : α) in t, g x ∂μ < ∞

Tactic:
calc ∫⁻ x in t, g x ∂μ
      _ ≤ ∫⁻ x, g x ∂μ := setLIntegral_le_lintegral t _
      _ < ∞ := by rw [← h_univ]; exact hf_int.lt_top

Premises used: MeasureTheory.setLIntegral_le_lintegral
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq_1 : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
⊢ ∫⁻ (x : α) in t, f x ∂μ ≠ ∞

Tactic:
ne_of_lt ?_

Premises used: ne_of_lt
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq_1 : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
refine_2 : ∫⁻ (x : α) in t, f x ∂μ < ∞
⊢ ∫⁻ (x : α) in t, f x ∂μ ≠ ∞

Tactic:
refine ne_of_lt ?_

Premises used: ne_of_lt
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq_1 : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
⊢ ∫⁻ (x : α) in t, f x ∂μ ≤ ∫⁻ (x : α), f x ∂μ

Tactic:
setLIntegral_le_lintegral t _

Premises used: MeasureTheory.setLIntegral_le_lintegral
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq_1 : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
h_eq : ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
⊢ ∫⁻ (x : α) in t, f x ∂μ < ∞

Tactic:
calc ∫⁻ x in t, f x ∂μ
      _ ≤ ∫⁻ x, f x ∂μ := setLIntegral_le_lintegral t _
      _ < ∞ := hf_int.lt_top

Premises used: Ne.lt_top, MeasureTheory.setLIntegral_le_lintegral
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
h_univ : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : ℕ → Set α
htd : Pairwise (Function.onFun Disjoint t)
htm : ∀ (i : ℕ), MeasurableSet (t i)
h : ∀ (i : ℕ), ∫⁻ (x : α) in t i, f x ∂μ = ∫⁻ (x : α) in t i, g x ∂μ
refine_3 : Eq (α := ℝ≥0∞) (∑' (i : ℕ), ∫⁻ (x : α) in t i, f x ∂μ) (∑' (i : ℕ), ∫⁻ (x : α) in t i, g x ∂μ)
⊢ ∫⁻ (x : α) in ⋃ (i : ℕ), t i, f x ∂μ = ∫⁻ (x : α) in ⋃ (i : ℕ), t i, g x ∂μ

Tactic:
simp_rw [lintegral_iUnion htm htd, h]

Premises used: MeasureTheory.lintegral_iUnion
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
h_univ : Set.univ ∈ s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
⊢ ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ

Tactic:
lintegral_eq_lintegral_of_isPiSystem h_eq h_inter basic ?_ hf_int t ht

Premises used: MeasureTheory.lintegral_eq_lintegral_of_isPiSystem
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
h_univ : Set.univ ∈ s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
refine : ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ
⊢ ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ

Tactic:
refine lintegral_eq_lintegral_of_isPiSystem h_eq h_inter basic ?_ hf_int t ht

Premises used: MeasureTheory.lintegral_eq_lintegral_of_isPiSystem
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
h_univ : Set.univ ∈ s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
rw : ∫⁻ (x : α) in Set.univ, f x ∂μ = ∫⁻ (x : α) in Set.univ, g x ∂μ
⊢ ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : α), g x ∂μ

Tactic:
rw [← setLIntegral_univ, ← setLIntegral_univ g]

Premises used: MeasureTheory.setLIntegral_univ
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
h_univ : Set.univ ∈ s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
⊢ ∫⁻ (x : α) in Set.univ, f x ∂μ = ∫⁻ (x : α) in Set.univ, g x ∂μ

Tactic:
basic _ h_univ
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
f g : α → ℝ≥0∞
h_eq : m0 = MeasurableSpace.generateFrom s
h_inter : IsPiSystem s
h_univ : Set.univ ∈ s
basic : ∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
hf_int : ∫⁻ (x : α), f x ∂μ ≠ ∞
t : Set α
ht : MeasurableSet t
⊢ ∫⁻ (x : α) in Set.univ, f x ∂μ = ∫⁻ (x : α) in Set.univ, g x ∂μ

Tactic:
exact basic _ h_univ
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
β : Type u_2
mβ : MeasurableSpace β
μ : Measure (α × β)
f g : α × β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_int : ∫⁻ (x : α × β), f x ∂μ ≠ ∞
h :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      ∀ ⦃t : Set β⦄, MeasurableSet t → ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ = ∫⁻ (x : α × β) in s ×ˢ t, g x ∂μ
rwa : ∫⁻ (x : α × β) in Set.univ, g x ∂μ ≠ ∞
rwa₁ : ∫⁻ (x : α × β) in SProd.sprod (α := Set α) (β := Set β) Set.univ Set.univ, g x ∂μ ≠ ∞
rwa₂ : ∫⁻ (x : α × β) in SProd.sprod (α := Set α) (β := Set β) Set.univ Set.univ, f x ∂μ ≠ ∞
rwa₃ : ∫⁻ (x : α × β) in Set.univ, f x ∂μ ≠ ∞
rwa₄ rwa₅ rwa₆ rwa₇ : ∫⁻ (x : α × β), f x ∂μ ≠ ∞
⊢ ∫⁻ (x : α × β), g x ∂μ ≠ ∞

Tactic:
rwa [← setLIntegral_univ, ← Set.univ_prod_univ, ← h .univ .univ, Set.univ_prod_univ,
      setLIntegral_univ]

Premises used: Set.univ_prod_univ, MeasurableSet.univ, MeasureTheory.setLIntegral_univ
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
β : Type u_2
mβ : MeasurableSpace β
μ : Measure (α × β)
f g : α × β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_int : ∫⁻ (x : α × β), f x ∂μ ≠ ∞
h :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      ∀ ⦃t : Set β⦄, MeasurableSet t → ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ = ∫⁻ (x : α × β) in s ×ˢ t, g x ∂μ
⊢ ∫⁻ (x : α × β), g x ∂μ ≠ ∞

Tactic:
have hg_int : ∫⁻ x, g x ∂μ ≠ ∞ := by
    rwa [← setLIntegral_univ, ← Set.univ_prod_univ, ← h .univ .univ, Set.univ_prod_univ,
      setLIntegral_univ]
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
β : Type u_2
mβ : MeasurableSpace β
μ : Measure (α × β)
f g : α × β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_int : ∫⁻ (x : α × β), f x ∂μ ≠ ∞
h :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      ∀ ⦃t : Set β⦄, MeasurableSet t → ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ = ∫⁻ (x : α × β) in s ×ˢ t, g x ∂μ
hg_int : ∫⁻ (x : α × β), g x ∂μ ≠ ∞
⊢ f =ᶠ[ae μ] g

Tactic:
AEMeasurable.ae_eq_of_forall_setLIntegral_eq hf hg hf_int hg_int fun s hs _ ↦ ?_

Premises used: MeasureTheory.AEMeasurable.ae_eq_of_forall_setLIntegral_eq
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
β : Type u_2
mβ : MeasurableSpace β
μ : Measure (α × β)
f g : α × β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_int : ∫⁻ (x : α × β), f x ∂μ ≠ ∞
h :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      ∀ ⦃t : Set β⦄, MeasurableSet t → ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ = ∫⁻ (x : α × β) in s ×ˢ t, g x ∂μ
hg_int : ∫⁻ (x : α × β), g x ∂μ ≠ ∞
refine :
  ∀ (s : Set (α × β)) (hs : MeasurableSet s),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      ∫⁻ (x : α × β) in s, f x ∂μ = ∫⁻ (x : α × β) in s, g x ∂μ
⊢ f =ᶠ[ae μ] g

Tactic:
refine AEMeasurable.ae_eq_of_forall_setLIntegral_eq hf hg hf_int hg_int fun s hs _ ↦ ?_

Premises used: MeasureTheory.AEMeasurable.ae_eq_of_forall_setLIntegral_eq
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
β : Type u_2
mβ : MeasurableSpace β
μ : Measure (α × β)
f g : α × β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_int : ∫⁻ (x : α × β), f x ∂μ ≠ ∞
h :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      ∀ ⦃t : Set β⦄, MeasurableSet t → ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ = ∫⁻ (x : α × β) in s ×ˢ t, g x ∂μ
hg_int : ∫⁻ (x : α × β), g x ∂μ ≠ ∞
s : Set (α × β)
hs : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α × β) in s, f x ∂μ = ∫⁻ (x : α × β) in s, g x ∂μ

Tactic:
lintegral_eq_lintegral_of_isPiSystem_of_univ_mem generateFrom_prod.symm isPiSystem_prod
    ?_ ?_ hf_int hs

Premises used: isPiSystem_prod, generateFrom_prod, MeasureTheory.lintegral_eq_lintegral_of_isPiSystem_of_univ_mem, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
β : Type u_2
mβ : MeasurableSpace β
μ : Measure (α × β)
f g : α × β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_int : ∫⁻ (x : α × β), f x ∂μ ≠ ∞
h :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      ∀ ⦃t : Set β⦄, MeasurableSet t → ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ = ∫⁻ (x : α × β) in s ×ˢ t, g x ∂μ
hg_int : ∫⁻ (x : α × β), g x ∂μ ≠ ∞
s : Set (α × β)
hs : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 :
  Membership.mem (γ := Set (Set (α × β)))
    (Set.image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
    Set.univ
refine_2 :
  ∀ (t : Set (α × β)),
    Membership.mem (γ := Set (Set (α × β)))
        (Set.image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s}
          {t : Set β | MeasurableSet t})
        t →
      ∫⁻ (x : α × β) in t, f x ∂μ = ∫⁻ (x : α × β) in t, g x ∂μ
⊢ ∫⁻ (x : α × β) in s, f x ∂μ = ∫⁻ (x : α × β) in s, g x ∂μ

Tactic:
refine lintegral_eq_lintegral_of_isPiSystem_of_univ_mem generateFrom_prod.symm isPiSystem_prod
    ?_ ?_ hf_int hs

Premises used: isPiSystem_prod, generateFrom_prod, MeasureTheory.lintegral_eq_lintegral_of_isPiSystem_of_univ_mem, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
β : Type u_2
mβ : MeasurableSpace β
μ : Measure (α × β)
f g : α × β → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
hf_int : ∫⁻ (x : α × β), f x ∂μ ≠ ∞
h :
  ∀ ⦃s : Set α⦄,
    MeasurableSet s →
      ∀ ⦃t : Set β⦄, MeasurableSet t → ∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ = ∫⁻ (x : α × β) in s ×ˢ t, g x ∂μ
hg_int : ∫⁻ (x : α × β), g x ∂μ ≠ ∞
s : Set (α × β)
hs : MeasurableSet s
h_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set (α × β)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Membership.mem (γ := Set (Set (α × β)))
    (Set.image2 (fun (x1 : Set α) (x2 : Set β) ↦ x1 ×ˢ x2) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t})
    Set.univ

Tactic:
⟨Set.univ, .univ, Set.univ, .univ, Set.univ_prod_univ⟩

Premises used: Set.Mem, Set.univ, setOf, Set.univ_prod_univ, Set.image2, And.intro, Exists.intro, MeasurableSet.univ