awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_zero :
  ∀ (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 ∂μ)
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HSub.hSub (α := E) (∫ (a : α) in s, f a ∂μ) (∫ (a : α) in s, g a ∂μ) = 0

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

Premises used: Iff.mpr, sub_eq_zero
-- 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_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_zero :
  ∀ (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 ∂μ)
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, (f - g) x ∂μ) 0

Tactic:
have hfg' : ∀ s : Set α, MeasurableSet s → μ s < ∞ → (∫ x in s, (f - g) x ∂μ) = 0 := by
    intro s hs hμs
    rw [integral_sub' (hf_int_finite s hs hμs) (hg_int_finite s hs hμs)]
    exact sub_eq_zero.mpr (hfg_zero s hs hμs)
-- 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_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_zero :
  ∀ (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 ∂μ)
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg' :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, (f - g) x ∂μ) 0
⊢ ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (f - g) s μ

Tactic:
have hfg_int : ∀ s, MeasurableSet s → μ s < ∞ → IntegrableOn (f - g) s μ := fun s hs hμs =>
    (hf_int_finite s hs hμs).sub (hg_int_finite s hs hμs)
-- 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_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_zero :
  ∀ (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 ∂μ)
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg' :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, (f - g) x ∂μ) 0
hfg_int :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (f - g) s μ
⊢ f - g =ᶠ[ae (μ.restrict t)] 0

Tactic:
ae_eq_zero_restrict_of_forall_setIntegral_eq_zero hfg_int hfg' ht hμt

Premises used: MeasureTheory.ae_eq_zero_restrict_of_forall_setIntegral_eq_zero
-- 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_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_zero :
  ∀ (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 ∂μ)
t : Set α
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg' :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, (f - g) x ∂μ) 0
hfg_int :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (f - g) s μ
⊢ f - g =ᶠ[ae (μ.restrict t)] 0

Tactic:
exact ae_eq_zero_restrict_of_forall_setIntegral_eq_zero hfg_int hfg' ht hμt

Premises used: MeasureTheory.ae_eq_zero_restrict_of_forall_setIntegral_eq_zero
-- 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
inst_3 : SigmaFinite μ
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
S : (i : ℕ) → Set α := spanningSets μ
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = 0 a} ∩ ⋃ (b : ℕ), spanningSets μ b) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ f =ᶠ[ae μ] 0

Tactic:
rw [← @Measure.restrict_univ _ _ μ, ← iUnion_spanningSets μ, EventuallyEq, ae_iff,
    Measure.restrict_apply' (MeasurableSet.iUnion (measurableSet_spanningSets μ))]

Premises used: Filter.EventuallyEq, MeasureTheory.measurableSet_spanningSets, MeasureTheory.ae_iff, MeasureTheory.iUnion_spanningSets, MeasurableSet.iUnion, MeasureTheory.Measure.restrict_apply', MeasureTheory.Measure.restrict_univ
-- 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
inst_3 : SigmaFinite μ
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
S : (i : ℕ) → Set α := spanningSets μ
rw : ∀ (i : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = 0 a} ∩ spanningSets μ i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = 0 a} ∩ ⋃ (b : ℕ), spanningSets μ b) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [Set.inter_iUnion, measure_iUnion_null_iff]

Premises used: MeasureTheory.measure_iUnion_null_iff, Set.inter_iUnion
-- 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
inst_3 : SigmaFinite μ
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
S : (i : ℕ) → Set α := spanningSets μ
n : ℕ
⊢ MeasurableSet (S n)

Tactic:
have h_meas_n : MeasurableSet (S n) := measurableSet_spanningSets μ n
-- 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
inst_3 : SigmaFinite μ
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
S : (i : ℕ) → Set α := spanningSets μ
n : ℕ
h_meas_n : MeasurableSet (S n)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have hμn : μ (S n) < ∞ := measure_spanningSets_lt_top μ n
-- 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
inst_3 : SigmaFinite μ
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
S : (i : ℕ) → Set α := spanningSets μ
n : ℕ
h_meas_n : MeasurableSet (S n)
hμn : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n) : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : Eq (α := ℝ≥0∞) ((μ.restrict (S n) : (a : Set α) → ℝ≥0∞) {a : α | ¬f a = 0 a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ({a : α | ¬f a = 0 a} ∩ spanningSets μ n) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← Measure.restrict_apply' h_meas_n]

Premises used: MeasureTheory.Measure.restrict_apply'
-- 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
inst_3 : SigmaFinite μ
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
S : (i : ℕ) → Set α := spanningSets μ
n : ℕ
h_meas_n : MeasurableSet (S n)
hμn : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (S n) : (a : Set α) → ℝ≥0∞) {a : α | ¬f a = 0 a} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
ae_eq_zero_restrict_of_forall_setIntegral_eq_zero hf_int_finite hf_zero h_meas_n hμn.ne

Premises used: Set.Mem, Filter.Eventually, setOf, MeasureTheory.ae_eq_zero_restrict_of_forall_setIntegral_eq_zero, Filter.EventuallyEq, LT.lt.ne
-- 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
inst_3 : SigmaFinite μ
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
S : (i : ℕ) → Set α := spanningSets μ
n : ℕ
h_meas_n : MeasurableSet (S n)
hμn : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (S n) : (a : Set α) → ℝ≥0∞) {a : α | ¬f a = 0 a} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact ae_eq_zero_restrict_of_forall_setIntegral_eq_zero hf_int_finite hf_zero h_meas_n hμn.ne

Premises used: MeasureTheory.ae_eq_zero_restrict_of_forall_setIntegral_eq_zero, LT.lt.ne
-- 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
inst_3 : SigmaFinite μ
f g : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_eq :
  ∀ (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 ∂μ)
rw : f - g =ᶠ[ae μ] 0
⊢ f =ᶠ[ae μ] g

Tactic:
rw [← sub_ae_eq_zero]

Premises used: MeasureTheory.sub_ae_eq_zero
-- 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
inst_3 : SigmaFinite μ
f g : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_eq :
  ∀ (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 ∂μ)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : HSub.hSub (α := E) (∫ (a : α) in s, f a ∂μ) (∫ (a : α) in s, g a ∂μ) = 0
rw₁ rw₂ : Eq.{u_2 + 1} (α := E) 0 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, (f - g) x ∂μ) 0

Tactic:
rw [integral_sub' (hf_int_finite s hs hμs) (hg_int_finite s hs hμs),
      sub_eq_zero.mpr (hfg_eq s hs hμs)]

Premises used: Iff.mpr, sub_eq_zero, MeasureTheory.integral_sub'
-- 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
inst_3 : SigmaFinite μ
f g : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_eq :
  ∀ (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 ∂μ)
⊢ ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, (f - g) x ∂μ) 0

Tactic:
have hfg : ∀ s : Set α, MeasurableSet s → μ s < ∞ → (∫ x in s, (f - g) x ∂μ) = 0 := by
    intro s hs hμs
    rw [integral_sub' (hf_int_finite s hs hμs) (hg_int_finite s hs hμs),
      sub_eq_zero.mpr (hfg_eq s hs hμs)]
-- 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
inst_3 : SigmaFinite μ
f g : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_eq :
  ∀ (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 ∂μ)
hfg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, (f - g) x ∂μ) 0
⊢ ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (f - g) s μ

Tactic:
have hfg_int : ∀ s, MeasurableSet s → μ s < ∞ → IntegrableOn (f - g) s μ := fun s hs hμs =>
    (hf_int_finite s hs hμs).sub (hg_int_finite s hs hμs)
-- 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
inst_3 : SigmaFinite μ
f g : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_eq :
  ∀ (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 ∂μ)
hfg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, (f - g) x ∂μ) 0
hfg_int :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (f - g) s μ
⊢ f - g =ᶠ[ae μ] 0

Tactic:
ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite hfg_int hfg

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
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : SigmaFinite μ
f g : α → E
hf_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s μ
hg_int_finite :
  ∀ (s : Set α), MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn g s μ
hfg_eq :
  ∀ (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 ∂μ)
hfg :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, (f - g) x ∂μ) 0
hfg_int :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn (f - g) s μ
⊢ f - g =ᶠ[ae μ] 0

Tactic:
exact ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite hfg_int hfg

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
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
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 : AEFinStronglyMeasurable f μ
t : Set α := hf.sigmaFiniteSet
suffices : f =ᶠ[ae (μ.restrict t)] 0
⊢ f =ᶠ[ae μ] 0

Tactic:
suffices f =ᵐ[μ.restrict t] 0 from
    ae_of_ae_restrict_of_ae_restrict_compl _ this hf.ae_eq_zero_compl
-- 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_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 : AEFinStronglyMeasurable f μ
t : Set α := hf.sigmaFiniteSet
⊢ SigmaFinite (μ.restrict t)

Tactic:
haveI : SigmaFinite (μ.restrict t) := hf.sigmaFinite_restrict
-- 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_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 : AEFinStronglyMeasurable f μ
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
⊢ f =ᶠ[ae (μ.restrict t)] 0

Tactic:
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
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
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 : AEFinStronglyMeasurable f μ
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
refine_1 :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → IntegrableOn f s (μ.restrict t)
refine_2 :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂μ.restrict t) 0
⊢ f =ᶠ[ae (μ.restrict t)] 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
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
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 : AEFinStronglyMeasurable f μ
t : Set α := hf.sigmaFiniteSet
this : SigmaFinite (μ.restrict t)
s : Set α
hs : MeasurableSet s
hμs : LT.lt (α := ℝ≥0∞) ((μ.restrict t : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 : Integrable f (μ.restrict (s ∩ t))
⊢ IntegrableOn f s (μ.restrict t)

Tactic:
rw [IntegrableOn, Measure.restrict_restrict hs]

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.Measure.restrict_restrict