awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Set β
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:
simp [integral_iUnion g_meas g_disj hf.integrableOn, hg]

Premises used: MeasureTheory.Integrable.integrableOn, MeasureTheory.integral_iUnion
-- 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 : 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
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
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, 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]

Premises used: Compl.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 β
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
apply : ∀ (s : Set β) (hs : IsClosed[inst_3] s), Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
⊢ f =ᶠ[ae μ] 0

Tactic:
apply ae_eq_zero_of_forall_setIntegral_isClosed_eq_zero hf (fun s hs ↦ ?_)

Premises used: MeasureTheory.ae_eq_zero_of_forall_setIntegral_isClosed_eq_zero
-- 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 β
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 ∂μ))
⊢ ∀ (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)
-- 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 β
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) 0 (∫ (x : β) in s, f x ∂μ)

Tactic:
simp_rw [A, tendsto_const_nhds_iff] at H

Premises used: tendsto_const_nhds_iff
-- 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 β
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
A : ∀ (n : ℕ), Eq.{u_2 + 1} (α := E) (∫ (x : β) in t n, f x ∂μ) 0
H : Eq.{u_2 + 1} (α := E) 0 (∫ (x : β) in s, f x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0

Tactic:
H.symm

Premises used: Eq.symm
-- 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 β
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
A : ∀ (n : ℕ), Eq.{u_2 + 1} (α := E) (∫ (x : β) in t n, f x ∂μ) 0
H : Eq.{u_2 + 1} (α := E) 0 (∫ (x : β) in s, f x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0

Tactic:
exact H.symm

Premises used: Eq.symm
-- 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 β
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
suffices : 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

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
-- 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 β
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
rw₁ : s = Set.univ ∩ s
rw₂ rw₃ : s = s
⊢ s = ⋃ (n : ℕ), t n

Tactic:
rw [← Set.iUnion_inter, iUnion_closure_compactCovering, Set.univ_inter]

Premises used: iUnion_closure_compactCovering, Set.univ_inter, Set.iUnion_inter
-- 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 β
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

Tactic:
have B : s = ⋃ n, t n := by
    rw [← Set.iUnion_inter, iUnion_closure_compactCovering, Set.univ_inter]
-- 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 β
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
B : s = ⋃ (n : ℕ), t n
rw : Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ ∫ (x : β) in t n, f x ∂μ) atTop (𝓝 (∫ (x : β) in ⋃ (n : ℕ), t n, f x ∂μ))
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ ∫ (x : β) in t n, f x ∂μ) atTop (𝓝 (∫ (x : β) in s, f x ∂μ))

Tactic:
rw [B]
-- 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 β
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
B : s = ⋃ (n : ℕ), t n
hsm : ∀ (i : ℕ), MeasurableSet (t i)
h_mono : Monotone t
hfi : IntegrableOn f (⋃ (n : ℕ), t n) μ
⊢ Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ ∫ (x : β) in t n, f x ∂μ) atTop (𝓝 (∫ (x : β) in ⋃ (n : ℕ), t n, f x ∂μ))

Tactic:
apply tendsto_setIntegral_of_monotone

Premises used: MeasureTheory.tendsto_setIntegral_of_monotone
-- 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 β
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
B : s = ⋃ (n : ℕ), t n
n : ℕ
⊢ MeasurableSet (t n)

Tactic:
(isClosed_closure.inter hs).measurableSet

Premises used: IsClosed.measurableSet, IsClosed.inter, isClosed_closure
-- 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 β
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
B : s = ⋃ (n : ℕ), t n
n : ℕ
⊢ MeasurableSet (t n)

Tactic:
exact (isClosed_closure.inter hs).measurableSet

Premises used: IsClosed.measurableSet, IsClosed.inter, isClosed_closure
-- 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 β
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
B : s = ⋃ (n : ℕ), t n
m n : ℕ
hmn : m ≤ n
h_mono : closure[inst_3] (compactCovering β m) ∩ s ⊆ closure[inst_3] (compactCovering β n) ∩ s
⊢ t m ≤ t n

Tactic:
simp only [t, Set.le_iff_subset]

Premises used: Set.le_iff_subset
-- 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 β
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
B : s = ⋃ (n : ℕ), t n
m n : ℕ
hmn : m ≤ n
⊢ closure[inst_3] (compactCovering β m) ∩ s ⊆ closure[inst_3] (compactCovering β n) ∩ s

Tactic:
gcongr
-- 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 β
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
B : s = ⋃ (n : ℕ), t n
⊢ IntegrableOn f (⋃ (n : ℕ), t n) μ

Tactic:
hf.integrableOn

Premises used: 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 β
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
B : s = ⋃ (n : ℕ), t n
⊢ IntegrableOn f (⋃ (n : ℕ), t n) μ

Tactic:
exact hf.integrableOn

Premises used: 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 β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : LocallyIntegrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
rw : f =ᶠ[ae (μ.restrict (⋃ (n : ℕ), closure[inst_3] (compactCovering β n)))] 0
⊢ f =ᶠ[ae μ] 0

Tactic:
rw [← μ.restrict_univ, ← iUnion_closure_compactCovering]

Premises used: iUnion_closure_compactCovering, MeasureTheory.Measure.restrict_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 β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : LocallyIntegrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
apply : ∀ (n : ℕ), ∀ᵐ (x : β) ∂μ.restrict (closure[inst_3] (compactCovering β n)), f x = 0 x
⊢ f =ᶠ[ae (μ.restrict (⋃ (n : ℕ), closure[inst_3] (compactCovering β n)))] 0

Tactic:
apply (ae_restrict_iUnion_iff _ _).2 (fun n ↦ ?_)

Premises used: Iff.mpr, MeasureTheory.ae_restrict_iUnion_iff
-- 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 β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : LocallyIntegrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
n : ℕ
hf₁ : Integrable f (μ.restrict (closure[inst_3] (compactCovering β n)))
h'f₁ :
  ∀ (s : Set β),
    IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ.restrict (closure[inst_3] (compactCovering β n))) 0
⊢ ∀ᵐ (x : β) ∂μ.restrict (closure[inst_3] (compactCovering β n)), f x = 0 x

Tactic:
apply ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero

Premises used: MeasureTheory.ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero
-- 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 β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : LocallyIntegrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
n : ℕ
⊢ Integrable f (μ.restrict (closure[inst_3] (compactCovering β n)))

Tactic:
hf.integrableOn_isCompact (isCompact_compactCovering β n).closure

Premises used: IsCompact.closure, MeasureTheory.IntegrableOn, isCompact_compactCovering, MeasureTheory.LocallyIntegrable.integrableOn_isCompact
-- 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 β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : LocallyIntegrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
n : ℕ
⊢ Integrable f (μ.restrict (closure[inst_3] (compactCovering β n)))

Tactic:
exact hf.integrableOn_isCompact (isCompact_compactCovering β n).closure

Premises used: IsCompact.closure, isCompact_compactCovering, MeasureTheory.LocallyIntegrable.integrableOn_isCompact
-- 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 β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : LocallyIntegrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
n : ℕ
s : Set β
hs : IsCompact s
h'f₁ : Eq.{u_2 + 1} (α := E) (∫ (x : β) in s ∩ closure[inst_3] (compactCovering β n), f x ∂μ) 0
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ.restrict (closure[inst_3] (compactCovering β n))) 0

Tactic:
rw [Measure.restrict_restrict' measurableSet_closure]

Premises used: measurableSet_closure, MeasureTheory.Measure.restrict_restrict'
-- 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 β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : LocallyIntegrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
n : ℕ
s : Set β
hs : IsCompact s
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : β) in s ∩ closure[inst_3] (compactCovering β n), f x ∂μ) 0

Tactic:
h'f _ (hs.inter_right isClosed_closure)

Premises used: IsCompact.inter_right, isClosed_closure
-- 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 β
inst_6 : SigmaCompactSpace β
inst_7 : R1Space β
μ : Measure β
f : β → E
hf : LocallyIntegrable f μ
h'f : ∀ (s : Set β), IsCompact s → Eq.{u_2 + 1} (α := E) (∫ (x : β) in s, f x ∂μ) 0
n : ℕ
s : Set β
hs : IsCompact s
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : β) in s ∩ closure[inst_3] (compactCovering β n), f x ∂μ) 0

Tactic:
exact h'f _ (hs.inter_right isClosed_closure)

Premises used: IsCompact.inter_right, isClosed_closure
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst : LinearOrder β
inst_1 : TopologicalSpace β
inst_2 : OrderTopology β
inst_3 : FirstCountableTopology β
f : α → β
c : β
simp_rw :
  (∀ b < c, ∀ᵐ (x : α) ∂μ, b < f x) ↔
    ∀ b < c, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ b} : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₁ :
  (∀ b < c, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬b < f a} : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ∀ b < c, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ b} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (∀ᵐ (x : α) ∂μ, c ≤ f x) ↔ ∀ b < c, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | f x ≤ b} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp_rw [eventually_const_le_iff_forall_lt_eventually_const_lt, ae_iff, not_lt]

Premises used: MeasureTheory.ae_iff, not_lt, eventually_const_le_iff_forall_lt_eventually_const_lt
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
β : Type u_2
inst : LinearOrder β
inst_1 : TopologicalSpace β
inst_2 : OrderTopology β
inst_3 : FirstCountableTopology β
μ : Measure α
f : α → β
c : β
⊢ (∀ᵐ (x : α) ∂μ, f x ≤ c) ↔
    ∀ (b : β), c < b → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | b ≤ f x} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
ae_const_le_iff_forall_lt_measure_zero (β := βᵒᵈ) _ _

Premises used: setOf, MeasureTheory.ae_const_le_iff_forall_lt_measure_zero, OrderDual
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
ε N : ℝ≥0
p : ℕ
εpos : 0 < ε
s : Set α := {x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have s_lt_top : μ s < ∞ :=
      (measure_mono (Set.inter_subset_right)).trans_lt (measure_spanningSets_lt_top μ p)
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
ε N : ℝ≥0
p : ℕ
εpos : 0 < ε
s : Set α := {x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p
s_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, g x ∂μ + HMul.hMul (β := ℝ≥0∞) (↑ε : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    ∫⁻ (x : α) in s, g x ∂μ + ∫⁻ (x : α) in s, (↑ε : ℝ≥0∞) ∂μ

Tactic:
simp only [lintegral_const, Set.univ_inter, MeasurableSet.univ, Measure.restrict_apply]

Premises used: MeasureTheory.lintegral_const, MeasureTheory.Measure.restrict_apply, Set.univ_inter, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Function.AEEqOfLIntegral
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ
ε N : ℝ≥0
p : ℕ
εpos : 0 < ε
s : Set α := {x : α | g x + (↑ε : ℝ≥0∞) ≤ f x ∧ g x ≤ (↑N : ℝ≥0∞)} ∩ spanningSets μ p
s_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : ∫⁻ (x : α) in toMeasurable μ s, f x ∂μ ≤ ∫⁻ (x : α) in toMeasurable μ s, g x ∂μ
⊢ ∫⁻ (x : α) in s, f x ∂μ ≤ ∫⁻ (x : α) in s, g x ∂μ + 0

Tactic:
rw [add_zero, ← Measure.restrict_toMeasurable s_lt_top.ne]

Premises used: MeasureTheory.Measure.restrict_toMeasurable, add_zero, LT.lt.ne