awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero_1 : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᶠ[ae (μ.restrict tᶜ)] 0
hf_meas_m : StronglyMeasurable f
refine :
  Eq (α := ℝ≥0∞) (((μ.restrict t).trim hm : (a : Set α) → ℝ≥0∞) {x : α | (fun (x : α) ↦ f x = 0 x) x}ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ f =ᶠ[ae (μ.restrict t)] 0

Tactic:
refine measure_eq_zero_of_trim_eq_zero hm ?_

Premises used: MeasureTheory.measure_eq_zero_of_trim_eq_zero
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero_1 : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᶠ[ae (μ.restrict tᶜ)] 0
hf_meas_m : StronglyMeasurable f
⊢ Eq (α := ℝ≥0∞) (((μ.restrict t).trim hm : (a : Set α) → ℝ≥0∞) {x : α | (fun (x : α) ↦ f x = 0 x) x}ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite ?_ ?_

Premises used: MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite, Set.Mem, Filter.Eventually, setOf, Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero_1 : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᶠ[ae (μ.restrict tᶜ)] 0
hf_meas_m : StronglyMeasurable f
refine_1 :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) (((μ.restrict t).trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn f s ((μ.restrict t).trim hm)
refine_2 :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) (((μ.restrict t).trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂(μ.restrict t).trim hm) 0
⊢ Eq (α := ℝ≥0∞) (((μ.restrict t).trim hm : (a : Set α) → ℝ≥0∞) {x : α | (fun (x : α) ↦ f x = 0 x) x}ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
refine ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite ?_ ?_

Premises used: MeasureTheory.ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero_1 : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᶠ[ae (μ.restrict tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) (((μ.restrict t).trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 : Integrable f ((μ.restrict (s ∩ t)).trim hm)
⊢ Integrable f (((μ.restrict t).trim hm).restrict s)

Tactic:
rw [restrict_trim hm (μ.restrict t) hs, Measure.restrict_restrict (hm s hs)]

Premises used: MeasureTheory.Measure.restrict, MeasureTheory.Measure.restrict_restrict, MeasureTheory.restrict_trim
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero_1 : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᶠ[ae (μ.restrict tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) (((μ.restrict t).trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [← restrict_trim hm μ ht_meas, Measure.restrict_apply hs,
      trim_measurableSet_eq hm (hs.inter ht_meas)] at hμs

Premises used: MeasureTheory.Measure.restrict_apply, MeasureTheory.trim_measurableSet_eq, MeasureTheory.restrict_trim, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero_1 : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᶠ[ae (μ.restrict tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable f ((μ.restrict (s ∩ t)).trim hm)

Tactic:
Integrable.trim hm ?_ hf_meas_m

Premises used: MeasureTheory.Integrable.trim
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero_1 : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᶠ[ae (μ.restrict tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 : Integrable f (μ.restrict (s ∩ t))
⊢ Integrable f ((μ.restrict (s ∩ t)).trim hm)

Tactic:
refine Integrable.trim hm ?_ hf_meas_m

Premises used: MeasureTheory.Integrable.trim
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero_1 : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᶠ[ae (μ.restrict tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable f (μ.restrict (s ∩ t))

Tactic:
hf_int_finite _ (hs.inter ht_meas) hμs

Premises used: MeasureTheory.IntegrableOn, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero_1 : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᶠ[ae (μ.restrict tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Integrable f (μ.restrict (s ∩ t))

Tactic:
exact hf_int_finite _ (hs.inter ht_meas) hμs

Premises used: MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero_1 : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᶠ[ae (μ.restrict tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) (((μ.restrict t).trim hm : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 : Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂(μ.restrict (s ∩ t)).trim hm) 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂(μ.restrict t).trim hm) 0

Tactic:
rw [restrict_trim hm (μ.restrict t) hs, Measure.restrict_restrict (hm s hs)]

Premises used: MeasureTheory.Measure.restrict, MeasureTheory.Measure.restrict_restrict, MeasureTheory.restrict_trim
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero_1 : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᶠ[ae (μ.restrict tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ t, f x ∂μ) 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂(μ.restrict (s ∩ t)).trim hm) 0

Tactic:
rw [← integral_trim hm hf_meas_m]

Premises used: MeasureTheory.integral_trim
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero_1 : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᶠ[ae (μ.restrict tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ t, f x ∂μ) 0

Tactic:
hf_zero _ (hs.inter ht_meas) hμs

Premises used: MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
hm : m ≤ m0
f : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
hf : FinStronglyMeasurable f (μ.trim hm)
t : Set α
ht_meas : MeasurableSet t
htf_zero_1 : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
htf_zero : f =ᶠ[ae (μ.restrict tᶜ)] 0
hf_meas_m : StronglyMeasurable f
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ t, f x ∂μ) 0

Tactic:
exact hf_zero _ (hs.inter ht_meas) hμs

Premises used: MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : α → E
hf : Integrable f μ
hf_zero :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) 0
⊢ f =ᶠ[ae μ] 0

Tactic:
hf.aefinStronglyMeasurable.ae_eq_zero_of_forall_setIntegral_eq_zero
    (fun _ _ _ => hf.integrableOn) hf_zero

Premises used: MeasureTheory.AEFinStronglyMeasurable.ae_eq_zero_of_forall_setIntegral_eq_zero, MeasureTheory.Integrable.aefinStronglyMeasurable, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f g : α → E
hf : Integrable f μ
hg : Integrable g μ
hfg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ) (∫ (x : α) in s, g x ∂μ)
⊢ f =ᶠ[ae μ] g

Tactic:
AEFinStronglyMeasurable.ae_eq_of_forall_setIntegral_eq (fun _ _ _ => hf.integrableOn)
    (fun _ _ _ => hg.integrableOn) hfg hf.aefinStronglyMeasurable hg.aefinStronglyMeasurable

Premises used: MeasureTheory.AEFinStronglyMeasurable.ae_eq_of_forall_setIntegral_eq, MeasureTheory.Integrable.aefinStronglyMeasurable, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsClosed[inst_3] s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
suffices : ∀ (s : Set β), MeasurableSet s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
⊢ f =ᶠ[ae μ] 0

Tactic:
suffices ∀ s, MeasurableSet s → ∫ x in s, f x ∂μ = 0 from
    hf.ae_eq_zero_of_forall_setIntegral_eq_zero (fun s hs _ ↦ this s hs)
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsClosed[inst_3] s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
t : Set β
t_meas : MeasurableSet t
ht : Eq.{u_2 + 1} (α := E) (∫ (x : β) in t, f x ∂μ) 0
rw : Eq.{u_2 + 1} (α := E) (∫ (x : β) in Set.univ, f x ∂μ) 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : β), f x ∂μ) 0

Tactic:
rw [← setIntegral_univ]

Premises used: MeasureTheory.setIntegral_univ
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsClosed[inst_3] s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
t : Set β
t_meas : MeasurableSet t
ht : Eq.{u_2 + 1} (α := E) (∫ (x : β) in t, f x ∂μ) 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : β) in Set.univ, f x ∂μ) 0

Tactic:
h'f _ isClosed_univ

Premises used: isClosed_univ
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsClosed[inst_3] s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
t : Set β
t_meas : MeasurableSet t
ht : Eq.{u_2 + 1} (α := E) (∫ (x : β) in t, f x ∂μ) 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : β) in Set.univ, f x ∂μ) 0

Tactic:
exact h'f _ isClosed_univ

Premises used: isClosed_univ
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsClosed[inst_3] s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
t : Set β
t_meas : MeasurableSet t
ht : Eq.{u_2 + 1} (α := E) (∫ (x : β) in t, f x ∂μ) 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : β), f x ∂μ) 0

Tactic:
have I : ∫ x, f x ∂μ = 0 := by rw [← setIntegral_univ]; exact h'f _ isClosed_univ
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsClosed[inst_3] s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
t : Set β
t_meas : MeasurableSet t
ht : Eq.{u_2 + 1} (α := E) (∫ (x : β) in t, f x ∂μ) 0
I : Eq.{u_2 + 1} (α := E) (∫ (x : β), f x ∂μ) 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : β) in tᶜ, f x ∂μ) 0

Tactic:
simpa [ht, I] using integral_add_compl t_meas hf

Premises used: MeasureTheory.integral_add_compl
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsClosed[inst_3] s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
⊢ ∀ (t : Set β),
    MeasurableSet t →
      Eq.{u_2 + 1} (α := E) (∫ (x : β) in t, f x ∂μ) 0 → Eq.{u_2 + 1} (α := E) (∫ (x : β) in tᶜ, f x ∂μ) 0

Tactic:
have A : ∀ (t : Set β), MeasurableSet t → ∫ (x : β) in t, f x ∂μ = 0
      → ∫ (x : β) in tᶜ, f x ∂μ = 0 := by
    intro t t_meas ht
    have I : ∫ x, f x ∂μ = 0 := by rw [← setIntegral_univ]; exact h'f _ isClosed_univ
    simpa [ht, I] using integral_add_compl t_meas hf
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsClosed[inst_3] s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
A :
  ∀ (t : Set β),
    MeasurableSet t →
      Eq.{u_2 + 1} (α := E) (∫ (x : β) in t, f x ∂μ) 0 → Eq.{u_2 + 1} (α := E) (∫ (x : β) in tᶜ, f x ∂μ) 0
s U : Set β
hU : IsOpen[inst_3] U
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : β) in U, f x ∂μ) 0

Tactic:
compl_compl U ▸ A _ hU.measurableSet.compl (h'f _ hU.isClosed_compl)

Premises used: compl_compl, Eq.rec, IsOpen.measurableSet, MeasurableSet.compl, IsOpen.isClosed_compl
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsClosed[inst_3] s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
A :
  ∀ (t : Set β),
    MeasurableSet t →
      Eq.{u_2 + 1} (α := E) (∫ (x : β) in t, f x ∂μ) 0 → Eq.{u_2 + 1} (α := E) (∫ (x : β) in tᶜ, f x ∂μ) 0
s U : Set β
hU : IsOpen[inst_3] U
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : β) in U, f x ∂μ) 0

Tactic:
exact compl_compl U ▸ A _ hU.measurableSet.compl (h'f _ hU.isClosed_compl)
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsClosed[inst_3] s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
A :
  ∀ (t : Set β),
    MeasurableSet t →
      Eq.{u_2 + 1} (α := E) (∫ (x : β) in t, f x ∂μ) 0 → Eq.{u_2 + 1} (α := E) (∫ (x : β) in tᶜ, f x ∂μ) 0
s_1 s : Set β
hs : MeasurableSet s
ihs : Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : β) in sᶜ, f x ∂μ) 0

Tactic:
A s hs ihs
-- Module: Mathlib.MeasureTheory.Function.AEEqOfIntegral
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
β : Type u_3
inst_3 : TopologicalSpace β
inst_4 : MeasurableSpace β
inst_5 : BorelSpace β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsClosed[inst_3] s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
A :
  ∀ (t : Set β),
    MeasurableSet t →
      Eq.{u_2 + 1} (α := E) (∫ (x : β) in t, f x ∂μ) 0 → Eq.{u_2 + 1} (α := E) (∫ (x : β) in tᶜ, f x ∂μ) 0
s_1 s : Set β
hs : MeasurableSet s
ihs : Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : β) in sᶜ, f x ∂μ) 0

Tactic:
exact A s hs ihs