awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ (u : Finset ι) (hu : u ∈ {x ∈ t.powerset | x.Nonempty}), MeasurableSet.{u_1} (α := X) (⋂ i ∈ u, s i)
⊢ Eq.{u_3 + 1} (α := E)
    (∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, HPow.hPow (α := ℝ) (-1) (#x + 1) • f a ∂μ)
    (∑ x ∈ t.powerset with x.Nonempty,
      ∫ (a : X), indicator (⋂ i ∈ x, s i) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#x + 1) • f a) a ∂μ)

Tactic:
have : ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, (-1 : ℝ) ^ (#x + 1) • f a ∂μ
      = ∑ x ∈ t.powerset with x.Nonempty, ∫ a, indicator (⋂ i ∈ x, s i)
        (fun a ↦ (-1 : ℝ) ^ (#x + 1) • f a) a ∂μ := by
    apply Finset.sum_congr rfl (fun x hx ↦ ?_)
    rw [← integral_indicator (A x hx)]
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ (u : Finset ι) (hu : u ∈ {x ∈ t.powerset | x.Nonempty}), MeasurableSet.{u_1} (α := X) (⋂ i ∈ u, s i)
this :
  Eq.{u_3 + 1} (α := E)
    (∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, HPow.hPow (α := ℝ) (-1) (#x + 1) • f a ∂μ)
    (∑ x ∈ t.powerset with x.Nonempty,
      ∫ (a : X), indicator (⋂ i ∈ x, s i) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#x + 1) • f a) a ∂μ)
rw :
  Eq.{u_3 + 1} (α := E) (∫ (x : X), indicator (⋃ i ∈ t, s i) f x ∂μ)
    (∫ (a : X),
      ∑ i ∈ t.powerset with i.Nonempty,
        indicator (⋂ i_1 ∈ i, s i_1) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#i + 1) • f a) a ∂μ)
hf₁ :
  ∀ i ∈ {x ∈ t.powerset | x.Nonempty},
    Integrable.{u_3, u_1} (ε := E) (indicator (⋂ i_1 ∈ i, s i_1) fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#i + 1) • f a) μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), indicator (⋃ i ∈ t, s i) f x ∂μ)
    (∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, HPow.hPow (α := ℝ) (-1) (#x + 1) • f a ∂μ)

Tactic:
rw [this, ← integral_finsetSum]

Premises used: MeasureTheory.integral_finsetSum
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ (u : Finset ι) (hu : u ∈ {x ∈ t.powerset | x.Nonempty}), MeasurableSet.{u_1} (α := X) (⋂ i ∈ u, s i)
this :
  Eq.{u_3 + 1} (α := E)
    (∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, HPow.hPow (α := ℝ) (-1) (#x + 1) • f a ∂μ)
    (∑ x ∈ t.powerset with x.Nonempty,
      ∫ (a : X), indicator (⋂ i ∈ x, s i) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#x + 1) • f a) a ∂μ)
u : Finset ι
hu : u ∈ {x ∈ t.powerset | x.Nonempty}
hf₁ : IntegrableOn.{u_1, u_3} (ε := E) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#u + 1) • f a) (⋂ i ∈ u, s i) μ
⊢ Integrable.{u_3, u_1} (ε := E) (indicator (⋂ i ∈ u, s i) fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#u + 1) • f a) μ

Tactic:
rw [integrable_indicator_iff (A u hu)]

Premises used: MeasureTheory.integrable_indicator_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ (u : Finset ι) (hu : u ∈ {x ∈ t.powerset | x.Nonempty}), MeasurableSet.{u_1} (α := X) (⋂ i ∈ u, s i)
this :
  Eq.{u_3 + 1} (α := E)
    (∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, HPow.hPow (α := ℝ) (-1) (#x + 1) • f a ∂μ)
    (∑ x ∈ t.powerset with x.Nonempty,
      ∫ (a : X), indicator (⋂ i ∈ x, s i) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#x + 1) • f a) a ∂μ)
u : Finset ι
hu : u ∈ {x ∈ t.powerset | x.Nonempty}
hf₁ : Integrable f (μ.restrict (⋂ i ∈ u, s i))
⊢ IntegrableOn.{u_1, u_3} (ε := E) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#u + 1) • f a) (⋂ i ∈ u, s i) μ

Tactic:
apply Integrable.smul

Premises used: MeasureTheory.Integrable.smul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ (u : Finset ι) (hu : u ∈ {x ∈ t.powerset | x.Nonempty}), MeasurableSet.{u_1} (α := X) (⋂ i ∈ u, s i)
this :
  Eq.{u_3 + 1} (α := E)
    (∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, HPow.hPow (α := ℝ) (-1) (#x + 1) • f a ∂μ)
    (∑ x ∈ t.powerset with x.Nonempty,
      ∫ (a : X), indicator (⋂ i ∈ x, s i) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#x + 1) • f a) a ∂μ)
u : Finset ι
hu : u ∈ {x ∈ t.powerset | x.Nonempty}
⊢ u ⊆ t ∧ u.Nonempty

Tactic:
simp only [Finset.mem_filter, Finset.mem_powerset] at hu

Premises used: Finset.mem_powerset, Finset.mem_filter
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ (u : Finset ι) (hu : u ∈ {x ∈ t.powerset | x.Nonempty}), MeasurableSet.{u_1} (α := X) (⋂ i ∈ u, s i)
this :
  Eq.{u_3 + 1} (α := E)
    (∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, HPow.hPow (α := ℝ) (-1) (#x + 1) • f a ∂μ)
    (∑ x ∈ t.powerset with x.Nonempty,
      ∫ (a : X), indicator (⋂ i ∈ x, s i) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#x + 1) • f a) a ∂μ)
u : Finset ι
hu : u ⊆ t ∧ u.Nonempty
hf₁ : ∀ (i : ι) (hi : i ∈ u), Integrable f (μ.restrict (⋂ i ∈ u, s i))
⊢ Integrable f (μ.restrict (⋂ i ∈ u, s i))

Tactic:
rcases hu.2 with ⟨i, hi⟩

Premises used: And.right
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ (u : Finset ι) (hu : u ∈ {x ∈ t.powerset | x.Nonempty}), MeasurableSet.{u_1} (α := X) (⋂ i ∈ u, s i)
this :
  Eq.{u_3 + 1} (α := E)
    (∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, HPow.hPow (α := ℝ) (-1) (#x + 1) • f a ∂μ)
    (∑ x ∈ t.powerset with x.Nonempty,
      ∫ (a : X), indicator (⋂ i ∈ x, s i) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#x + 1) • f a) a ∂μ)
u : Finset ι
hu : u ⊆ t ∧ u.Nonempty
i : ι
hi : i ∈ u
⊢ Integrable f (μ.restrict (⋂ i ∈ u, s i))

Tactic:
(hf i (hu.1 hi)).mono (biInter_subset_of_mem hi) le_rfl

Premises used: le_rfl, MeasureTheory.IntegrableOn, Set.biInter_subset_of_mem, And.left, MeasureTheory.IntegrableOn.mono
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ (u : Finset ι) (hu : u ∈ {x ∈ t.powerset | x.Nonempty}), MeasurableSet.{u_1} (α := X) (⋂ i ∈ u, s i)
this :
  Eq.{u_3 + 1} (α := E)
    (∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, HPow.hPow (α := ℝ) (-1) (#x + 1) • f a ∂μ)
    (∑ x ∈ t.powerset with x.Nonempty,
      ∫ (a : X), indicator (⋂ i ∈ x, s i) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#x + 1) • f a) a ∂μ)
u : Finset ι
hu : u ⊆ t ∧ u.Nonempty
i : ι
hi : i ∈ u
⊢ Integrable f (μ.restrict (⋂ i ∈ u, s i))

Tactic:
exact (hf i (hu.1 hi)).mono (biInter_subset_of_mem hi) le_rfl

Premises used: le_rfl, Set.biInter_subset_of_mem, And.left, MeasureTheory.IntegrableOn.mono
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ (u : Finset ι) (hu : u ∈ {x ∈ t.powerset | x.Nonempty}), MeasurableSet.{u_1} (α := X) (⋂ i ∈ u, s i)
this :
  Eq.{u_3 + 1} (α := E)
    (∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, HPow.hPow (α := ℝ) (-1) (#x + 1) • f a ∂μ)
    (∑ x ∈ t.powerset with x.Nonempty,
      ∫ (a : X), indicator (⋂ i ∈ x, s i) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#x + 1) • f a) a ∂μ)
e_f :
  ∀ (x : X),
    indicator (⋃ i ∈ t, s i) f x =
      ∑ i ∈ t.powerset with i.Nonempty,
        indicator (⋂ i_1 ∈ i, s i_1) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#i + 1) • f a) x
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), indicator (⋃ i ∈ t, s i) f x ∂μ)
    (∫ (a : X),
      ∑ i ∈ t.powerset with i.Nonempty,
        indicator (⋂ i_1 ∈ i, s i_1) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#i + 1) • f a) a ∂μ)

Tactic:
congr with x
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ (u : Finset ι) (hu : u ∈ {x ∈ t.powerset | x.Nonempty}), MeasurableSet.{u_1} (α := X) (⋂ i ∈ u, s i)
this :
  Eq.{u_3 + 1} (α := E)
    (∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, HPow.hPow (α := ℝ) (-1) (#x + 1) • f a ∂μ)
    (∑ x ∈ t.powerset with x.Nonempty,
      ∫ (a : X), indicator (⋂ i ∈ x, s i) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#x + 1) • f a) a ∂μ)
x : X
⊢ indicator (⋃ i ∈ t, s i) f x =
    ∑ t ∈ t.powerset with t.Nonempty, HPow.hPow (α := ℤ) (-1) (#t + 1) • indicator (⋂ i ∈ t, s i) f x

Tactic:
Finset.indicator_biUnion_eq_sum_powerset t s f x

Premises used: Finset.indicator_biUnion_eq_sum_powerset
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ (u : Finset ι) (hu : u ∈ {x ∈ t.powerset | x.Nonempty}), MeasurableSet.{u_1} (α := X) (⋂ i ∈ u, s i)
this :
  Eq.{u_3 + 1} (α := E)
    (∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, HPow.hPow (α := ℝ) (-1) (#x + 1) • f a ∂μ)
    (∑ x ∈ t.powerset with x.Nonempty,
      ∫ (a : X), indicator (⋂ i ∈ x, s i) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#x + 1) • f a) a ∂μ)
x : X
h :
  ∀ (u : Finset ι) (hu : u ∈ {t ∈ t.powerset | t.Nonempty}),
    indicator (⋂ i ∈ u, s i) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#u + 1) • f a) x =
      HPow.hPow (α := ℤ) (-1) (#u + 1) • indicator (⋂ i ∈ u, s i) f x
⊢ indicator (⋃ i ∈ t, s i) f x =
    ∑ i ∈ t.powerset with i.Nonempty,
      indicator (⋂ i_1 ∈ i, s i_1) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#i + 1) • f a) x

Tactic:
convert! Finset.indicator_biUnion_eq_sum_powerset t s f x with u hu

Premises used: Finset.indicator_biUnion_eq_sum_powerset
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ (u : Finset ι) (hu : u ∈ {x ∈ t.powerset | x.Nonempty}), MeasurableSet.{u_1} (α := X) (⋂ i ∈ u, s i)
this :
  Eq.{u_3 + 1} (α := E)
    (∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, HPow.hPow (α := ℝ) (-1) (#x + 1) • f a ∂μ)
    (∑ x ∈ t.powerset with x.Nonempty,
      ∫ (a : X), indicator (⋂ i ∈ x, s i) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#x + 1) • f a) a ∂μ)
x : X
u : Finset ι
hu : u ∈ {t ∈ t.powerset | t.Nonempty}
h :
  HPow.hPow (α := ℝ) (-1) (#u + 1) • indicator (⋂ i ∈ u, s i) f x =
    HPow.hPow (α := ℤ) (-1) (#u + 1) • indicator (⋂ i ∈ u, s i) f x
⊢ indicator (⋂ i ∈ u, s i) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#u + 1) • f a) x =
    HPow.hPow (α := ℤ) (-1) (#u + 1) • indicator (⋂ i ∈ u, s i) f x

Tactic:
rw [indicator_smul_apply]

Premises used: Set.indicator_smul_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ (u : Finset ι) (hu : u ∈ {x ∈ t.powerset | x.Nonempty}), MeasurableSet.{u_1} (α := X) (⋂ i ∈ u, s i)
this :
  Eq.{u_3 + 1} (α := E)
    (∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, HPow.hPow (α := ℝ) (-1) (#x + 1) • f a ∂μ)
    (∑ x ∈ t.powerset with x.Nonempty,
      ∫ (a : X), indicator (⋂ i ∈ x, s i) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#x + 1) • f a) a ∂μ)
x : X
u : Finset ι
hu : u ∈ {t ∈ t.powerset | t.Nonempty}
h h₁ h₂ h₃ :
  Int.negSucc 0 ^ (#u + 1) • indicator (⋂ i ∈ u, s i) f x = Int.negSucc 0 ^ (#u + 1) • indicator (⋂ i ∈ u, s i) f x
⊢ HPow.hPow (α := ℝ) (-1) (#u + 1) • indicator (⋂ i ∈ u, s i) f x =
    HPow.hPow (α := ℤ) (-1) (#u + 1) • indicator (⋂ i ∈ u, s i) f x

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_5
m : MeasurableSpace X
μ : Measure X
s : Set X
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.ofReal (∫ (x : X) in s, 1 ∂μ) = ENNReal.ofReal (∫ (x : X) in s, norm (E := ℝ) 1 ∂μ)

Tactic:
simp only [norm_one]

Premises used: NormOneClass.norm_one
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_5
m : MeasurableSpace X
μ : Measure X
s : Set X
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.ofReal (∫ (x : X) in s, norm (E := ℝ) 1 ∂μ) = ∫⁻ (x : X) in s, 1 ∂μ

Tactic:
simp [measureReal_def, hs]

Premises used: MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_5
x : MeasurableSpace X
μ : Measure X
inst : IsFiniteMeasure μ
s : Set X
⊢ ENNReal.ofReal (∫ (x : X) in s, 1 ∂μ) = (μ : (a : Set X) → ℝ≥0∞) s

Tactic:
ofReal_setIntegral_one_of_measure_ne_top

Premises used: MeasureTheory.ofReal_setIntegral_one_of_measure_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_5
m : MeasurableSpace X
μ : Measure X
s : Set X
⊢ ∫ (x : X) in s, 1 ∂μ = μ.real s

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
simp_rw :
  Eq (α := ℝ) (∫ (x : X) in ⋃ i ∈ t, s i, 1 ∂μ)
    (∑ x ∈ t.powerset with x.Nonempty, HPow.hPow (α := ℝ) (-1) (#x + 1) * ∫ (x : X) in ⋂ i ∈ x, s i, 1 ∂μ)
⊢ μ.real (⋃ i ∈ t, s i) = ∑ u ∈ t.powerset with u.Nonempty, HPow.hPow (α := ℝ) (-1) (#u + 1) * μ.real (⋂ i ∈ u, s i)

Tactic:
simp_rw [← setIntegral_one_eq_measureReal]

Premises used: MeasureTheory.setIntegral_one_eq_measureReal
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
apply : ∀ i ∈ t, IntegrableOn (ε := ℝ) (fun (x : X) ↦ 1) (s i) μ
⊢ Eq (α := ℝ) (∫ (x : X) in ⋃ i ∈ t, s i, 1 ∂μ)
    (∑ x ∈ t.powerset with x.Nonempty, HPow.hPow (α := ℝ) (-1) (#x + 1) * ∫ (x : X) in ⋂ i ∈ x, s i, 1 ∂μ)

Tactic:
apply integral_biUnion_eq_sum_powerset hs

Premises used: MeasureTheory.integral_biUnion_eq_sum_powerset
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
i : ι
hi : i ∈ t
⊢ IntegrableOn (ε := ℝ) (fun (x : X) ↦ 1) (s i) μ

Tactic:
simpa using (hf i hi).lt_top

Premises used: Ne.lt_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : X → E
s : Set X
μ : Measure X
inst_2 : DecidablePred fun (x : X) ↦ x ∈ s
hs : MeasurableSet s
hf : IntegrableOn f s μ
hg : IntegrableOn g sᶜ μ
rw :
  ∫ (x : X), (s.indicator f + sᶜ.indicator g) x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, g x ∂μ)
rw₁ :
  HAdd.hAdd (α := E) (∫ (a : X), s.indicator f a ∂μ) (∫ (a : X), sᶜ.indicator g a ∂μ) =
    HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, g x ∂μ)
rw₂ :
  HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (a : X), sᶜ.indicator g a ∂μ) =
    HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, g x ∂μ)
rw₃ rw₄ :
  HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, g x ∂μ) =
    HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, g x ∂μ)
⊢ ∫ (x : X), s.piecewise (β := fun (i : X) ↦ E) f g x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, g x ∂μ)

Tactic:
rw [← Set.indicator_add_compl_eq_piecewise,
    integral_add' (hf.integrable_indicator hs) (hg.integrable_indicator hs.compl),
    integral_indicator hs, integral_indicator hs.compl]

Premises used: MeasureTheory.integral_indicator, MeasureTheory.IntegrableOn.integrable_indicator, MeasurableSet.compl, Set.indicator_add_compl_eq_piecewise, MeasureTheory.integral_add'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hfi : IntegrableOn f (⋃ (n : ι), s n) μ
⊢ Tendsto.{u_5, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ))

Tactic:
.of_neBot_imp fun hne ↦ ?_

Premises used: Filter.Tendsto.of_neBot_imp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hfi : IntegrableOn f (⋃ (n : ι), s n) μ
⊢ NeBot.{u_5} (α := ι) atTop

Tactic:
refine .of_neBot_imp fun hne ↦ ?_
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hfi : IntegrableOn f (⋃ (n : ι), s n) μ
hne : NeBot.{u_5} (α := ι) atTop
⊢ IsDirectedOrder ι

Tactic:
have := (atTop_neBot_iff.mp hne).2
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hfi : IntegrableOn f (⋃ (n : ι), s n) μ
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
⊢ ∫⁻ (x : X) in ⋃ (n : ι), s n, (↑‖f x‖₊ : ℝ≥0∞) ∂μ < ∞

Tactic:
have hfi' : ∫⁻ x in ⋃ n, s n, ‖f x‖₊ ∂μ < ∞ := hfi.2
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hfi : IntegrableOn f (⋃ (n : ι), s n) μ
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
hfi' : ∫⁻ (x : X) in ⋃ (n : ι), s n, (↑‖f x‖₊ : ℝ≥0∞) ∂μ < ∞
set :
  let S : Set X := ⋃ (i : ι), s i;
  ∀ (hfi : IntegrableOn f S μ) (hfi' : ∫⁻ (x : X) in S, (↑‖f x‖₊ : ℝ≥0∞) ∂μ < ∞),
    Tendsto.{u_5, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in S, f x ∂μ))
⊢ Tendsto.{u_5, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ))

Tactic:
set S := ⋃ i, s i
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
S : Set X := ⋃ (i : ι), s i
hfi : IntegrableOn f S μ
hfi' : ∫⁻ (x : X) in S, (↑‖f x‖₊ : ℝ≥0∞) ∂μ < ∞
⊢ NullMeasurableSet S μ

Tactic:
have hSm : NullMeasurableSet S μ := MeasurableSet.iUnion_of_monotone h_mono hsm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
S : Set X := ⋃ (i : ι), s i
hfi : IntegrableOn f S μ
hfi' : ∫⁻ (x : X) in S, (↑‖f x‖₊ : ℝ≥0∞) ∂μ < ∞
hSm : NullMeasurableSet S μ
⊢ ∀ {i : ι}, s i ⊆ S

Tactic:
have hsub {i} : s i ⊆ S := subset_iUnion s i
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
S : Set X := ⋃ (i : ι), s i
hfi : IntegrableOn f S μ
hfi' : ∫⁻ (x : X) in S, (↑‖f x‖₊ : ℝ≥0∞) ∂μ < ∞
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
⊢ LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑‖f x‖₊ : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [← withDensity_apply₀ _ hSm] at hfi'

Premises used: MeasureTheory.withDensity_apply₀
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
S : Set X := ⋃ (i : ι), s i
hfi : IntegrableOn f S μ
hfi' : ∫⁻ (x : X) in S, (↑‖f x‖₊ : ℝ≥0∞) ∂μ < ∞
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
hfi'₁ : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑‖f x‖₊ : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ NullMeasurableSet S μ

Tactic:
rw [← withDensity_apply₀ _ hSm] at hfi'

Premises used: MeasureTheory.withDensity_apply₀
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
S : Set X := ⋃ (i : ι), s i
hfi : IntegrableOn f S μ
hfi' : ∫⁻ (x : X) in S, (↑‖f x‖₊ : ℝ≥0∞) ∂μ < ∞
hSm : NullMeasurableSet S μ
hsub : ∀ {i : ι}, s i ⊆ S
hfi'₁ : LT.lt (α := ℝ≥0∞) ((μ.withDensity fun (x : X) ↦ (↑‖f x‖₊ : ℝ≥0∞) : (a : Set X) → ℝ≥0∞) S : ℝ≥0∞) (∞ : ℝ≥0∞)
hSm₁ : NullMeasurableSet S μ
⊢ ∀ {i : ι}, s i ⊆ S

Tactic:
rw [← withDensity_apply₀ _ hSm] at hfi'

Premises used: MeasureTheory.withDensity_apply₀