awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
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 : ∀ x ∈ tᶜ, f x = 0
htμ : SigmaFinite ((μ.trim hm).restrict t)
this : SigmaFinite ((μ.restrict t).trim hm)
⊢ f =ᶠ[ae μ] 0
have htf_zero₁ : f =ᶠ[ae (μ.restrict tᶜ)] 0
Tactic: have htf_zero : f =ᵐ[μ.restrict tᶜ] 0 := by
    rw [EventuallyEq, ae_restrict_iff' (MeasurableSet.compl (hm _ ht_meas))]
    exact Eventually.of_forall htf_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
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
⊢ f =ᶠ[ae μ] 0
have hf_meas_m : StronglyMeasurable f
Tactic: have hf_meas_m : StronglyMeasurable[m] f := hf.stronglyMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
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
⊢ f =ᶠ[ae μ] 0
have suffices : f =ᶠ[ae (μ.restrict t)] 0
Tactic: suffices f =ᵐ[μ.restrict t] 0 from
    ae_of_ae_restrict_of_ae_restrict_compl _ this htf_zero
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
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
⊢ f =ᶠ[ae (μ.restrict t)] 0
have refine : Eq (α := ℝ≥0∞) (((μ.restrict t).trim hm : (a : Set α) → ℝ≥0∞) {x : α | (fun (x : α) ↦ f x = 0 x) x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine measure_eq_zero_of_trim_eq_zero hm ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
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∞)
have 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)
Tactic: refine ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
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)
⊢ Eq (α := ℝ≥0∞) (((μ.restrict t).trim hm : (a : Set α) → ℝ≥0∞) {x : α | (fun (x : α) ↦ f x = 0 x) x}ᶜ : ℝ≥0∞)
    (0 : ℝ≥0∞)
have 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
Tactic: refine ae_eq_zero_of_forall_setIntegral_eq_of_sigmaFinite ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
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∞)
⊢ Integrable f (((μ.restrict t).trim hm).restrict s)
have refine_1 : Integrable f ((μ.restrict (s ∩ t)).trim hm)
Tactic: rw [restrict_trim hm (μ.restrict t) hs, Measure.restrict_restrict (hm s hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
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∞)
⊢ Integrable f ((μ.restrict (s ∩ t)).trim hm)
have hμs₁ : 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
Cleared hypotheses: hμs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
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)
have refine_1 : Integrable f (μ.restrict (s ∩ t))
Tactic: refine Integrable.trim hm ?_ hf_meas_m
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
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∞)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, f x ∂(μ.restrict t).trim hm) 0
have refine_2 : Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂(μ.restrict (s ∩ t)).trim hm) 0
Tactic: rw [restrict_trim hm (μ.restrict t) hs, Measure.restrict_restrict (hm s hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
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∞)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), f x ∂(μ.restrict (s ∩ t)).trim hm) 0
have hμs₁ : 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
Cleared hypotheses: hμs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
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 : α), f x ∂(μ.restrict (s ∩ t)).trim hm) 0
have refine_2 : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s ∩ t, f x ∂μ) 0
Tactic: rw [← integral_trim hm hf_meas_m]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
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
⊢ f =ᶠ[ae μ] 0
have suffices : ∀ (s : Set β), MeasurableSet s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
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
have rw : Eq.{u_2 + 1} (α := E) (∫ (x : β) in Set.univ, f x ∂μ) 0
Tactic: rw [← setIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
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 tᶜ, f x ∂μ) 0
have I : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
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
⊢ ∀ (s : Set β), MeasurableSet s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
have 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
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
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 : Set β
hs : MeasurableSet s
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
have isOpen : ∀ (U : Set β) (hU : IsOpen[inst_3] U), Eq.{u_2 + 1} (α := E) (∫ (x : β) in U, f x ∂μ) 0
Tactic: induction s, hs using MeasurableSet.induction_on_open with
  | isOpen U hU => exact compl_compl U ▸ A _ hU.measurableSet.compl (h'f _ hU.isClosed_compl)
  | compl s hs ihs => exact A s hs ihs
  | iUnion g g_disj g_meas hg => simp [integral_iUnion g_meas g_disj hf.integrableOn, hg]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
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 : Set β
hs : MeasurableSet s
isOpen : ∀ (U : Set β) (hU : IsOpen[inst_3] U), Eq.{u_2 + 1} (α := E) (∫ (x : β) in U, f x ∂μ) 0
compl :
  ∀ (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
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
have iUnion : ∀ (g : ℕ → Set β) (g_disj : Pairwise (Function.onFun Disjoint g)) (g_meas : ∀ (i : ℕ), MeasurableSet (g i))
  (hg : ∀ (i : ℕ), Eq.{u_2 + 1} (α := E) (∫ (x : β) in g i, f x ∂μ) 0),
  Eq.{u_2 + 1} (α := E) (∫ (x : β) in ⋃ (i : ℕ), g i, f x ∂μ) 0
Tactic: induction s, hs using MeasurableSet.induction_on_open with
  | isOpen U hU => exact compl_compl U ▸ A _ hU.measurableSet.compl (h'f _ hU.isClosed_compl)
  | compl s hs ihs => exact A s hs ihs
  | iUnion g g_disj g_meas hg => simp [integral_iUnion g_meas g_disj hf.integrableOn, hg]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
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 β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
⊢ f =ᶠ[ae μ] 0
have apply : ∀ (s : Set β) (hs : IsClosed[inst_3] s), Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
Tactic: apply ae_eq_zero_of_forall_setIntegral_isClosed_eq_zero hf (fun s hs ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
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 β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
s : Set β
hs : IsClosed[inst_3] s
t : ℕ → Set β := fun (n : ℕ) ↦ closure[inst_3] (compactCovering β n) ∩ s
H : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ ∫ (x : β) in t n, f x ∂μ) atTop (𝓝 (∫ (x : β) in s, f x ∂μ))
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
have A : ∀ (n : ℕ), Eq.{u_2 + 1} (α := E) (∫ (x : β) in t n, f x ∂μ) 0
Tactic: have A : ∀ n, ∫ x in t n, f x ∂μ = 0 :=
      fun n ↦ h'f _ ((isCompact_compactCovering β n).closure.inter_right hs)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (hypothesis)
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 β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
s : Set β
hs : IsClosed[inst_3] s
t : ℕ → Set β := fun (n : ℕ) ↦ closure[inst_3] (compactCovering β n) ∩ s
H : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ ∫ (x : β) in t n, f x ∂μ) atTop (𝓝 (∫ (x : β) in s, f x ∂μ))
A : ∀ (n : ℕ), Eq.{u_2 + 1} (α := E) (∫ (x : β) in t n, f x ∂μ) 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
have H₁ : Eq.{u_2 + 1} (α := E) 0 (∫ (x : β) in s, f x ∂μ)
Tactic: simp_rw [A, tendsto_const_nhds_iff] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
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 β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
s : Set β
hs : IsClosed[inst_3] s
t : ℕ → Set β := fun (n : ℕ) ↦ closure[inst_3] (compactCovering β n) ∩ s
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
have suffices : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ ∫ (x : β) in t n, f x ∂μ) atTop (𝓝 (∫ (x : β) in s, f x ∂μ))
Tactic: suffices H : Tendsto (fun n ↦ ∫ x in t n, f x ∂μ) atTop (𝓝 (∫ x in s, f x ∂μ)) by
    have A : ∀ n, ∫ x in t n, f x ∂μ = 0 :=
      fun n ↦ h'f _ ((isCompact_compactCovering β n).closure.inter_right hs)
    simp_rw [A, tendsto_const_nhds_iff] at H
    exact H.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
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 β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
s : Set β
hs : IsClosed[inst_3] s
t : ℕ → Set β := fun (n : ℕ) ↦ closure[inst_3] (compactCovering β n) ∩ s
⊢ s = ⋃ (n : ℕ), t n
have rw : s = (⋃ (i : ℕ), closure[inst_3] (compactCovering β i)) ∩ s
Tactic: rw [← Set.iUnion_inter, iUnion_closure_compactCovering, Set.univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.AEEqOfIntegral (goal)
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 β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
s : Set β
hs : IsClosed[inst_3] s
t : ℕ → Set β := fun (n : ℕ) ↦ closure[inst_3] (compactCovering β n) ∩ s
rw : s = (⋃ (i : ℕ), closure[inst_3] (compactCovering β i)) ∩ s
⊢ s = ⋃ (n : ℕ), t n
have rw₁ : s = Set.univ ∩ s
Tactic: rw [← Set.iUnion_inter, iUnion_closure_compactCovering, Set.univ_inter]