awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : MeasurableSet t
rw : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ.restrict s) (∫ (x : X) in s ∩ t, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, t.indicator f x ∂μ) (∫ (x : X) in s ∩ t, f x ∂μ)
have rw₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t ∩ s, f x ∂μ) (∫ (x : X) in s ∩ t, f x ∂μ)
Tactic: rw [integral_indicator ht, Measure.restrict_restrict ht, Set.inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : MeasurableSet t
rw : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ.restrict s) (∫ (x : X) in s ∩ t, f x ∂μ)
rw₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t ∩ s, f x ∂μ) (∫ (x : X) in s ∩ t, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, t.indicator f x ∂μ) (∫ (x : X) in s ∩ t, f x ∂μ)
have rw₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∩ t, f x ∂μ) (∫ (x : X) in s ∩ t, f x ∂μ)
Tactic: rw [integral_indicator ht, Measure.restrict_restrict ht, Set.inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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) μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ)
    (∑ u ∈ t.powerset with u.Nonempty,
      HSMul.hSMul (β := E) (HPow.hPow (α := ℝ) (-1) (#u + 1)) (∫ (x : X) in ⋂ i ∈ u, s i, f x ∂μ))
have simp_rw : 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: simp_rw [← integral_smul, ← integral_indicator (Finset.measurableSet_biUnion _ hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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) μ
u : Finset ι
hu : u ∈ {x ∈ t.powerset | x.Nonempty}
⊢ MeasurableSet.{u_1} (α := X) (⋂ i ∈ u, s i)
have refine : ∀ (i : ι) (hi : i ∈ u), i ∈ t
Tactic: refine u.measurableSet_biInter fun i hi ↦ hs i ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
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) μ
⊢ 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 ∂μ)
have A : ∀ (u : Finset ι) (hu : u ∈ {x ∈ t.powerset | x.Nonempty}), MeasurableSet.{u_1} (α := X) (⋂ i ∈ u, s i)
Tactic: have A (u) (hu : u ∈ t.powerset.filter (·.Nonempty)) : MeasurableSet (⋂ i ∈ u, s i) := by
    refine u.measurableSet_biInter fun i hi ↦ hs i ?_
    grind
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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 ∂μ)
have apply : ∀ (x : Finset ι) (hx : x ∈ {x ∈ t.powerset | x.Nonempty}),
  Eq.{u_3 + 1} (α := E) (∫ (a : X) in ⋂ i ∈ x, s i, HPow.hPow (α := ℝ) (-1) (#x + 1) • f a ∂μ)
    (∫ (a : X), indicator (⋂ i ∈ x, s i) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#x + 1) • f a) a ∂μ)
Tactic: apply Finset.sum_congr rfl (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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)
x : Finset ι
hx : x ∈ {x ∈ t.powerset | x.Nonempty}
⊢ Eq.{u_3 + 1} (α := E) (∫ (a : X) in ⋂ i ∈ x, s i, HPow.hPow (α := ℝ) (-1) (#x + 1) • f a ∂μ)
    (∫ (a : X), indicator (⋂ i ∈ x, s i) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#x + 1) • f a) a ∂μ)
have rw : Eq.{u_3 + 1} (α := E)
  (∫ (x_1 : X), indicator (⋂ i ∈ x, s i) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#x + 1) • f a) x_1 ∂μ)
  (∫ (a : X), indicator (⋂ i ∈ x, s i) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#x + 1) • f a) a ∂μ)
Tactic: rw [← integral_indicator (A x hx)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
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 : 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 ∂μ)
have 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 ∂μ)
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)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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 ∂μ)
⊢ 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 ∂μ)
have 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 ∂μ)
Tactic: rw [this, ← integral_finsetSum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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 ∂μ)
⊢ 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 ∂μ)
have 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) μ
Tactic: rw [this, ← integral_finsetSum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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}
⊢ Integrable.{u_3, u_1} (ε := E) (indicator (⋂ i ∈ u, s i) fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#u + 1) • f a) μ
have hf₁ : IntegrableOn.{u_1, u_3} (ε := E) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#u + 1) • f a) (⋂ i ∈ u, s i) μ
Tactic: rw [integrable_indicator_iff (A u hu)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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}
⊢ IntegrableOn.{u_1, u_3} (ε := E) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#u + 1) • f a) (⋂ i ∈ u, s i) μ
have hf₁ : Integrable f (μ.restrict (⋂ i ∈ u, s i))
Tactic: apply Integrable.smul
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
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}
⊢ Integrable f (μ.restrict (⋂ i ∈ u, s i))
have hu₁ : u ⊆ t ∧ u.Nonempty
Tactic: simp only [Finset.mem_filter, Finset.mem_powerset] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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
⊢ Integrable f (μ.restrict (⋂ i ∈ u, s i))
have hf₁ : ∀ (i : ι) (hi : i ∈ u), Integrable f (μ.restrict (⋂ i ∈ u, s i))
Tactic: rcases hu.2 with ⟨i, hi⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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 ∂μ)
⊢ 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 ∂μ)
have 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
Tactic: congr with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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 =
    ∑ i ∈ t.powerset with i.Nonempty,
      indicator (⋂ i_1 ∈ i, s i_1) (fun (a : X) ↦ HPow.hPow (α := ℝ) (-1) (#i + 1) • f a) x
have 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
Tactic: convert! Finset.indicator_biUnion_eq_sum_powerset t s f x with u hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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}
⊢ 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
have 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
Tactic: rw [indicator_smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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}
⊢ HPow.hPow (α := ℝ) (-1) (#u + 1) • indicator (⋂ i ∈ u, s i) f x =
    HPow.hPow (α := ℤ) (-1) (#u + 1) • indicator (⋂ i ∈ u, s i) f x
have 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
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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∞)
⊢ μ.real (⋃ i ∈ t, s i) = ∑ u ∈ t.powerset with u.Nonempty, HPow.hPow (α := ℝ) (-1) (#u + 1) * μ.real (⋂ i ∈ u, s i)
have 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 ∂μ)
Tactic: simp_rw [← setIntegral_one_eq_measureReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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∞)
⊢ 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 ∂μ)
have apply : ∀ i ∈ t, IntegrableOn (ε := ℝ) (fun (x : X) ↦ 1) (s i) μ
Tactic: apply integral_biUnion_eq_sum_powerset hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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ᶜ μ
⊢ ∫ (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 ∂μ)
have 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 ∂μ)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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 ∂μ)
⊢ ∫ (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 ∂μ)
have 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 ∂μ)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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 ∂μ)
⊢ ∫ (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 ∂μ)
have 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 ∂μ)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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 ∂μ)
⊢ ∫ (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 ∂μ)
have 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 ∂μ)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
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 ∂μ))
have hne : NeBot.{u_5} (α := ι) atTop
Tactic: refine .of_neBot_imp fun hne ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (hypothesis)
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
⊢ Tendsto.{u_5, u_3} (β := E) (fun (i : ι) ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ))
have this : IsDirectedOrder ι
Tactic: have := (atTop_neBot_iff.mp hne).2