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
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : NeBot.{u_5} (α := ι) atTop
this_1 : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
this :
  Tendsto (fun (x : ι) ↦ HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in s i₀ \ s x, f x ∂μ)) atTop
    (𝓝 (HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, f x ∂μ)))
h :
  ∫ (x : X) in ⋂ (n : ι), s n, f x ∂μ =
    HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, f x ∂μ)
convert_2 :
  ∀ (i : ι) (hi : i₀ ≤ i),
    HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in s i₀ \ s i, f x ∂μ) = ∫ (x : X) in s i, 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:
convert! this.congr' <| (eventually_ge_atTop i₀).mono fun i hi ↦ ?_

Premises used: Filter.Eventually.mono, Filter.eventually_ge_atTop, Filter.Tendsto.congr'
-- 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 : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : NeBot.{u_5} (α := ι) atTop
this_1 : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
this :
  Tendsto (fun (x : ι) ↦ HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in s i₀ \ s x, f x ∂μ)) atTop
    (𝓝 (HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, f x ∂μ)))
rw : MeasurableSet.{u_1} (α := X) (⋂ (i : ι), s i)
⊢ ∫ (x : X) in ⋂ (n : ι), s n, f x ∂μ =
    HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, f x ∂μ)

Tactic:
rw [← diff_iInter, setIntegral_diff _ hi₀ (iInter_subset _ _), sub_sub_cancel]

Premises used: MeasureTheory.setIntegral_diff, sub_sub_cancel, Set.iInter_subset, Set.diff_iInter
-- 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 : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : NeBot.{u_5} (α := ι) atTop
this_1 : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
this :
  Tendsto (fun (x : ι) ↦ HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in s i₀ \ s x, f x ∂μ)) atTop
    (𝓝 (HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, f x ∂μ)))
⊢ MeasurableSet.{u_1} (α := X) (⋂ (i : ι), s i)

Tactic:
.iInter_of_antitone h_anti hsm

Premises used: MeasurableSet.iInter_of_antitone
-- 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 : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : NeBot.{u_5} (α := ι) atTop
this_1 : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
this :
  Tendsto (fun (x : ι) ↦ HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in s i₀ \ s x, f x ∂μ)) atTop
    (𝓝 (HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, f x ∂μ)))
⊢ MeasurableSet.{u_1} (α := X) (⋂ (i : ι), s i)

Tactic:
exact .iInter_of_antitone h_anti 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 : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : NeBot.{u_5} (α := ι) atTop
this_1 : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
this :
  Tendsto (fun (x : ι) ↦ HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in s i₀ \ s x, f x ∂μ)) atTop
    (𝓝 (HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, f x ∂μ)))
i : ι
hi : i₀ ≤ i
convert_2 :
  ∫ (x : X) in s i₀, f x ∂μ - HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in s i, f x ∂μ) =
    ∫ (x : X) in s i, f x ∂μ
convert_2₁ convert_2₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s i, f x ∂μ) (∫ (x : X) in s i, f x ∂μ)
⊢ HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in s i₀ \ s i, f x ∂μ) = ∫ (x : X) in s i, f x ∂μ

Tactic:
rw [setIntegral_diff (hsm i) hi₀ (h_anti hi), sub_sub_cancel]

Premises used: MeasureTheory.setIntegral_diff, sub_sub_cancel
-- 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 : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
suffices :
  Tendsto (fun (x : ι) ↦ HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in s i₀ \ s x, f x ∂μ)) atTop
    (𝓝 (HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, 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:
suffices Tendsto (∫ x in s i₀, f x ∂μ - ∫ x in s i₀ \ s ·, f x ∂μ) atTop
      (𝓝 (∫ x in s i₀, f x ∂μ - ∫ x in ⋃ i, s i₀ \ s i, f x ∂μ)) by
    convert! this.congr' <| (eventually_ge_atTop i₀).mono fun i hi ↦ ?_
    · rw [← diff_iInter, setIntegral_diff _ hi₀ (iInter_subset _ _), sub_sub_cancel]
      exact .iInter_of_antitone h_anti hsm
    · rw [setIntegral_diff (hsm i) hi₀ (h_anti hi), sub_sub_cancel]
-- 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 : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
apply :
  Tendsto.{u_5, u_3} (β := E) (fun (x : ι) ↦ ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, f x ∂μ))
⊢ Tendsto (fun (x : ι) ↦ HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in s i₀ \ s x, f x ∂μ)) atTop
    (𝓝 (HSub.hSub (α := E) (∫ (x : X) in s i₀, f x ∂μ) (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, f x ∂μ)))

Tactic:
apply tendsto_const_nhds.sub

Premises used: tendsto_const_nhds, Filter.Tendsto.sub
-- 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 : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ ∀ (i : ι), MeasurableSet (s i₀ \ s i)

Tactic:
measurability
-- 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 : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
refine_1 : Monotone.{u_5, u_1} (β := Set X) fun (x : ι) ↦ s i₀ \ s x
refine_2 : IntegrableOn f (⋃ (n : ι), s i₀ \ s n) μ
⊢ Tendsto.{u_5, u_3} (β := E) (fun (x : ι) ↦ ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in ⋃ (i : ι), s i₀ \ s i, f x ∂μ))

Tactic:
refine tendsto_setIntegral_of_monotone (by measurability) ?_ ?_

Premises used: MeasureTheory.tendsto_setIntegral_of_monotone
-- 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 : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ Monotone.{u_5, u_1} (β := Set X) fun (x : ι) ↦ s i₀ \ s x

Tactic:
fun i j h ↦ diff_subset_diff_right (h_anti h)

Premises used: Monotone, Set.diff_subset_diff_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
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ Monotone.{u_5, u_1} (β := Set X) fun (x : ι) ↦ s i₀ \ s x

Tactic:
exact fun i j h ↦ diff_subset_diff_right (h_anti h)

Premises used: Set.diff_subset_diff_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
inst_2 : Preorder ι
inst_3 : IsCountablyGenerated.{u_5} (α := ι) atTop
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
refine_2 : IntegrableOn f (s i₀ \ ⋂ (i : ι), s i) μ
⊢ IntegrableOn f (⋃ (n : ι), s i₀ \ s n) μ

Tactic:
rw [← diff_iInter]

Premises used: Set.diff_iInter
-- 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 : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ IntegrableOn f (s i₀ \ ⋂ (i : ι), s i) μ

Tactic:
hi₀.mono_set diff_subset

Premises used: Set.diff_subset, MeasureTheory.IntegrableOn.mono_set
-- 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 : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : NeBot.{u_5} (α := ι) atTop
this : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ IntegrableOn f (s i₀ \ ⋂ (i : ι), s i) μ

Tactic:
exact hi₀.mono_set diff_subset

Premises used: Set.diff_subset, MeasureTheory.IntegrableOn.mono_set
-- 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 : Countable ι
s : ι → Set X
hm : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
hfi : IntegrableOn f (⋃ (i : ι), s i) μ
simp :
  ∀ (hfi : @Integrable _ _ _ _ mX f (Measure.sum fun (i : ι) ↦ μ.restrict (s i))),
    HasSum.{u_3, u_5} (α := E) (fun (n : ι) ↦ ∫ (x : X) in s n, f x ∂μ)
      (@integral _ _ _ _ mX (Measure.sum fun (i : ι) ↦ μ.restrict (s i)) fun (x : X) ↦ f x)
⊢ HasSum.{u_3, u_5} (α := E) (fun (n : ι) ↦ ∫ (x : X) in s n, f x ∂μ) (∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ)

Tactic:
simp only [IntegrableOn, Measure.restrict_iUnion_ae hd hm] at hfi ⊢

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.Measure.restrict_iUnion_ae
-- 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 : Countable ι
s : ι → Set X
hm : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
hfi : @Integrable _ _ _ _ mX f (Measure.sum fun (i : ι) ↦ μ.restrict (s i))
⊢ HasSum.{u_3, u_5} (α := E) (fun (n : ι) ↦ ∫ (x : X) in s n, f x ∂μ)
    (@integral _ _ _ _ mX (Measure.sum fun (i : ι) ↦ μ.restrict (s i)) fun (x : X) ↦ f x)

Tactic:
hasSum_integral_measure hfi

Premises used: MeasureTheory.hasSum_integral_measure
-- 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 : Countable ι
s : ι → Set X
hm : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
hfi : @Integrable _ _ _ _ mX f (Measure.sum fun (i : ι) ↦ μ.restrict (s i))
⊢ HasSum.{u_3, u_5} (α := E) (fun (n : ι) ↦ ∫ (x : X) in s n, f x ∂μ)
    (@integral _ _ _ _ mX (Measure.sum fun (i : ι) ↦ μ.restrict (s i)) fun (x : X) ↦ f x)

Tactic:
exact hasSum_integral_measure hfi

Premises used: MeasureTheory.hasSum_integral_measure
-- 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 : Countable ι
s : ι → Set X
hm : ∀ (i : ι), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : IntegrableOn f (⋃ (i : ι), s i) μ
⊢ HasSum.{u_3, u_5} (α := E) (fun (n : ι) ↦ ∫ (x : X) in s n, f x ∂μ) (∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ)

Tactic:
hasSum_integral_iUnion_ae (fun i => (hm i).nullMeasurableSet) (hd.mono fun _ _ h => h.aedisjoint)
    hfi

Premises used: MeasurableSet.nullMeasurableSet, Disjoint.aedisjoint, MeasureTheory.hasSum_integral_iUnion_ae, Pairwise.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
inst_2 : Countable ι
s : ι → Set X
hm : ∀ (i : ι), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
hfi : IntegrableOn f (⋃ (i : ι), s i) μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ) (∑' (n : ι), ∫ (x : X) in s n, f x ∂μ)

Tactic:
(HasSum.tsum_eq (hasSum_integral_iUnion hm hd hfi)).symm

Premises used: HasSum.tsum_eq, MeasureTheory.hasSum_integral_iUnion, Eq.symm
-- 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 : Countable ι
s : ι → Set X
hm : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
hfi : IntegrableOn f (⋃ (i : ι), s i) μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ (n : ι), s n, f x ∂μ) (∑' (n : ι), ∫ (x : X) in s n, f x ∂μ)

Tactic:
(HasSum.tsum_eq (hasSum_integral_iUnion_ae hm hd hfi)).symm

Premises used: HasSum.tsum_eq, MeasureTheory.hasSum_integral_iUnion_ae, Eq.symm
-- 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
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
pos : ∀ (hf : AEStronglyMeasurable f (μ.restrict t)), Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) 0
neg : ∀ (hf : ¬AEStronglyMeasurable f (μ.restrict t)), Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) 0

Tactic:
by_cases hf : AEStronglyMeasurable f (μ.restrict t)

Premises used: MeasureTheory.Measure.restrict, MeasureTheory.AEStronglyMeasurable
-- 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
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : ¬AEStronglyMeasurable f (μ.restrict t)
neg : ¬Integrable f (μ.restrict t)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) 0

Tactic:
rw [integral_undef]

Premises used: MeasureTheory.integral_undef
-- 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
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : ¬AEStronglyMeasurable f (μ.restrict t)
neg : ∀ (hf : Integrable f (μ.restrict t)), AEStronglyMeasurable f (μ.restrict t)
⊢ ¬Integrable f (μ.restrict t)

Tactic:
contrapose hf
-- 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
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : Integrable f (μ.restrict t)
⊢ AEStronglyMeasurable f (μ.restrict t)

Tactic:
hf.1

Premises used: And.left
-- 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
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : Integrable f (μ.restrict t)
⊢ AEStronglyMeasurable f (μ.restrict t)

Tactic:
exact hf.1

Premises used: And.left
-- 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
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ) 0

Tactic:
integral_eq_zero_of_ae ?_

Premises used: MeasureTheory.integral_eq_zero_of_ae
-- 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
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
refine : AEStronglyMeasurable.mk f hf =ᶠ[ae (μ.restrict t)] 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ) 0

Tactic:
refine integral_eq_zero_of_ae ?_

Premises used: MeasureTheory.integral_eq_zero_of_ae
-- 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
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
rw : ∀ᵐ (x : X) ∂μ, x ∈ t → AEStronglyMeasurable.mk f hf x = 0 x
⊢ AEStronglyMeasurable.mk f hf =ᶠ[ae (μ.restrict t)] 0

Tactic:
rw [EventuallyEq,
      ae_restrict_iff (hf.stronglyMeasurable_mk.measurableSet_eq_fun stronglyMeasurable_zero)]

Premises used: Filter.EventuallyEq, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.StronglyMeasurable.measurableSet_eq_fun, MeasureTheory.ae_restrict_iff, MeasureTheory.stronglyMeasurable_zero
-- 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
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
h :
  ∀ (x : X) (hx : x ∈ t → f x = AEStronglyMeasurable.mk f hf x) (h'x : x ∈ t → f x = 0) (h''x : x ∈ t),
    AEStronglyMeasurable.mk f hf x = 0 x
⊢ ∀ᵐ (x : X) ∂μ, x ∈ t → AEStronglyMeasurable.mk f hf x = 0 x

Tactic:
filter_upwards [ae_imp_of_ae_restrict hf.ae_eq_mk, ht_eq] with x hx h'x h''x

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.ae_imp_of_ae_restrict
-- 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
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
x : X
hx : x ∈ t → f x = AEStronglyMeasurable.mk f hf x
h'x : x ∈ t → f x = 0
h''x : x ∈ t
h : f x = 0 x
⊢ AEStronglyMeasurable.mk f hf x = 0 x

Tactic:
rw [← hx h''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
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
x : X
hx : x ∈ t → f x = AEStronglyMeasurable.mk f hf x
h'x : x ∈ t → f x = 0
h''x : x ∈ t
⊢ f x = 0 x

Tactic:
h'x h''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
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
x : X
hx : x ∈ t → f x = AEStronglyMeasurable.mk f hf x
h'x : x ∈ t → f x = 0
h''x : x ∈ t
⊢ f x = 0 x

Tactic:
exact h'x h''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
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ) 0

Tactic:
have : ∫ x in t, hf.mk f x ∂μ = 0 := by
    refine integral_eq_zero_of_ae ?_
    rw [EventuallyEq,
      ae_restrict_iff (hf.stronglyMeasurable_mk.measurableSet_eq_fun stronglyMeasurable_zero)]
    filter_upwards [ae_imp_of_ae_restrict hf.ae_eq_mk, ht_eq] with x hx h'x h''x
    rw [← hx h''x]
    exact h'x h''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
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
this : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ) 0
pos : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) 0

Tactic:
rw [← this]
-- 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
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
this : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ) 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ)

Tactic:
integral_congr_ae hf.ae_eq_mk

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.AEStronglyMeasurable.ae_eq_mk
-- 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
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
this : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ) 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ)

Tactic:
exact integral_congr_ae hf.ae_eq_mk

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.AEStronglyMeasurable.ae_eq_mk
-- 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
t : Set X
μ : Measure X
ht_eq : ∀ x ∈ t, f x = 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) 0

Tactic:
setIntegral_eq_zero_of_ae_eq_zero (Eventually.of_forall ht_eq)

Premises used: Filter.Eventually.of_forall, MeasureTheory.setIntegral_eq_zero_of_ae_eq_zero