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
s : ι → Set X
a : ι
s_1 : Finset ι
hat : a ∉ s_1
IH :
  ∀ (hs : ∀ i ∈ s_1, MeasurableSet (s i)) (h's : (↑s_1 : Set ι).Pairwise (Disjoint on s))
    (hf : ∀ i ∈ s_1, IntegrableOn f (s i) μ),
    Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ i ∈ s_1, s i, f x ∂μ) (∑ i ∈ s_1, ∫ (x : X) in s i, f x ∂μ)
hs : MeasurableSet (s a) ∧ ∀ x ∈ s_1, MeasurableSet (s x)
hf : IntegrableOn f (s a) μ ∧ ∀ x ∈ s_1, IntegrableOn f (s x) μ
h's : (↑s_1 : Set ι).Pairwise (Disjoint on s) ∧ ∀ b ∈ (↑s_1 : Set ι), a ≠ b → (Disjoint on s) a b ∧ (Disjoint on s) b a
⊢ MeasurableSet.{u_1} (α := X) (⋃ i ∈ s_1, s i)

Tactic:
Finset.measurableSet_biUnion _ hs.2

Premises used: And.right, Finset.measurableSet_biUnion
-- 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
s : ι → Set X
a : ι
s_1 : Finset ι
hat : a ∉ s_1
IH :
  ∀ (hs : ∀ i ∈ s_1, MeasurableSet (s i)) (h's : (↑s_1 : Set ι).Pairwise (Disjoint on s))
    (hf : ∀ i ∈ s_1, IntegrableOn f (s i) μ),
    Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ i ∈ s_1, s i, f x ∂μ) (∑ i ∈ s_1, ∫ (x : X) in s i, f x ∂μ)
hs : MeasurableSet (s a) ∧ ∀ x ∈ s_1, MeasurableSet (s x)
hf : IntegrableOn f (s a) μ ∧ ∀ x ∈ s_1, IntegrableOn f (s x) μ
h's : (↑s_1 : Set ι).Pairwise (Disjoint on s) ∧ ∀ b ∈ (↑s_1 : Set ι), a ≠ b → (Disjoint on s) a b ∧ (Disjoint on s) b a
⊢ MeasurableSet.{u_1} (α := X) (⋃ i ∈ s_1, s i)

Tactic:
exact Finset.measurableSet_biUnion _ hs.2

Premises used: And.right, Finset.measurableSet_biUnion
-- 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)
h's : (↑t : Set ι).Pairwise (Disjoint on s)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
empty :
  ∀ (hs : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MeasurableSet (s i))
    (h's : (↑∅ : Set ι).Pairwise (Disjoint on s))
    (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IntegrableOn f (s i) μ),
    Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), s i, f x ∂μ)
      (∑ i ∈ ∅, ∫ (x : X) in s i, f x ∂μ)
insert :
  ∀ (a : ι) (s_1 : Finset ι) (hat : a ∉ s_1)
    (IH :
      ∀ (hs : ∀ i ∈ s_1, MeasurableSet (s i)) (h's : (↑s_1 : Set ι).Pairwise (Disjoint on s))
        (hf : ∀ i ∈ s_1, IntegrableOn f (s i) μ),
        Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ i ∈ s_1, s i, f x ∂μ) (∑ i ∈ s_1, ∫ (x : X) in s i, f x ∂μ))
    (hs : ∀ i ∈ Insert.insert a s_1, MeasurableSet (s i))
    (h's : (↑(Insert.insert a s_1) : Set ι).Pairwise (Disjoint on s))
    (hf : ∀ i ∈ Insert.insert a s_1, IntegrableOn f (s i) μ),
    Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ i ∈ Insert.insert a s_1, s i, f x ∂μ)
      (∑ i ∈ Insert.insert a s_1, ∫ (x : X) in s i, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ) (∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ)

Tactic:
induction t using Finset.induction_on with
  | empty => simp
  | insert _ _ hat IH =>
    simp only [Finset.coe_insert, Finset.forall_mem_insert, Set.pairwise_insert,
      Finset.set_biUnion_insert] at hs hf h's ⊢
    rw [setIntegral_union _ _ hf.1 (integrableOn_finset_iUnion.2 hf.2)]
    · rw [Finset.sum_insert hat, IH hs.2 h's.1 hf.2]
    · simp only [disjoint_iUnion_right]
      exact fun i hi => (h's.2 i hi (ne_of_mem_of_not_mem hi hat).symm).1
    · exact Finset.measurableSet_biUnion _ hs.2

Premises used: Finset.forall_mem_insert, Insert.insert, Set.disjoint_iUnion_right, Set.pairwise_insert, Finset.coe_insert, Finset.set_biUnion_insert
-- 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)
h's : (↑t : Set ι).Pairwise (Disjoint on s)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
empty :
  ∀ (hs : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → MeasurableSet (s i))
    (h's : (↑∅ : Set ι).Pairwise (Disjoint on s))
    (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → IntegrableOn f (s i) μ),
    Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), s i, f x ∂μ)
      (∑ i ∈ ∅, ∫ (x : X) in s i, f x ∂μ)
insert :
  ∀ (a : ι) (s_1 : Finset ι) (hat : a ∉ s_1)
    (IH :
      ∀ (hs : ∀ i ∈ s_1, MeasurableSet (s i)) (h's : (↑s_1 : Set ι).Pairwise (Disjoint on s))
        (hf : ∀ i ∈ s_1, IntegrableOn f (s i) μ),
        Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ i ∈ s_1, s i, f x ∂μ) (∑ i ∈ s_1, ∫ (x : X) in s i, f x ∂μ))
    (hs : ∀ i ∈ Insert.insert a s_1, MeasurableSet (s i))
    (h's : (↑(Insert.insert a s_1) : Set ι).Pairwise (Disjoint on s))
    (hf : ∀ i ∈ Insert.insert a s_1, IntegrableOn f (s i) μ),
    Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ i ∈ Insert.insert a s_1, s i, f x ∂μ)
      (∑ i ∈ Insert.insert a s_1, ∫ (x : X) in s i, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ) (∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ)

Tactic:
classical
  induction t using Finset.induction_on with
  | empty => simp
  | insert _ _ hat IH =>
    simp only [Finset.coe_insert, Finset.forall_mem_insert, Set.pairwise_insert,
      Finset.set_biUnion_insert] at hs hf h's ⊢
    rw [setIntegral_union _ _ hf.1 (integrableOn_finset_iUnion.2 hf.2)]
    · rw [Finset.sum_insert hat, IH hs.2 h's.1 hf.2]
    · simp only [disjoint_iUnion_right]
      exact fun i hi => (h's.2 i hi (ne_of_mem_of_not_mem hi hat).symm).1
    · exact Finset.measurableSet_biUnion _ hs.2

Premises used: Finset.forall_mem_insert, Insert.insert, Set.disjoint_iUnion_right, Set.pairwise_insert, Finset.coe_insert, Finset.set_biUnion_insert
-- 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 : Fintype ι
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), IntegrableOn f (s i) μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) Finset.univ i), s i, f x ∂μ)
    (∑ i : ι, ∫ (x : X) in s i, f x ∂μ)

Tactic:
integral_biUnion_finset Finset.univ (fun i _ => hs i) _ fun i _ => hf i

Premises used: Finset.univ, MeasureTheory.integral_biUnion_finset
-- 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 : Fintype ι
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), IntegrableOn f (s i) μ
h : ∀ (x : ι), s x = ⋃ (_ : Membership.mem (γ := Finset ι) Finset.univ x), s x
convert! : (↑Finset.univ : Set ι).Pairwise (Disjoint on s)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ (i : ι), s i, f x ∂μ) (∑ i : ι, ∫ (x : X) in s i, f x ∂μ)

Tactic:
convert! integral_biUnion_finset Finset.univ (fun i _ => hs i) _ fun i _ => hf i

Premises used: Finset.univ, MeasureTheory.integral_biUnion_finset
-- 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 : Fintype ι
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), IntegrableOn f (s i) μ
x : ι
⊢ s x = ⋃ (_ : Membership.mem (γ := Finset ι) Finset.univ x), s x

Tactic:
simp
-- 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 : Fintype ι
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), IntegrableOn f (s i) μ
⊢ (↑Finset.univ : Set ι).Pairwise (Disjoint on s)

Tactic:
simp [pairwise_univ, h's]

Premises used: Set.pairwise_univ
-- 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
rw : Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mX 0 fun (x : X) ↦ f x) 0
rw₁ rw₂ : Eq.{u_3 + 1} (α := E) 0 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in ∅, f x ∂μ) 0

Tactic:
rw [Measure.restrict_empty, integral_zero_measure]

Premises used: MeasureTheory.Measure.restrict_empty, MeasureTheory.integral_zero_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
rw rw₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X), f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in univ, f x ∂μ) (∫ (x : X), f x ∂μ)

Tactic:
rw [Measure.restrict_univ]

Premises used: MeasureTheory.Measure.restrict_univ
-- 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
s : Set X
μ : Measure X
hs : ∀ᵐ (x : X) ∂μ, x ∈ s
f : X → E
rw : s =ᶠ[ae μ] univ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ)

Tactic:
rw [← setIntegral_univ, ← setIntegral_congr_set]

Premises used: MeasureTheory.setIntegral_congr_set, MeasureTheory.setIntegral_univ
-- 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
s : Set X
μ : Measure X
hs : ∀ᵐ (x : X) ∂μ, x ∈ s
f : X → E
rwa rwa₁ rwa₂ rwa₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s =ᶠ[ae μ] univ

Tactic:
rwa [ae_eq_univ]

Premises used: MeasureTheory.ae_eq_univ
-- 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
s : Set X
μ : Measure X
hs : NullMeasurableSet s μ
hfi : Integrable f μ
⊢ ∫ (x : X) in s ∪ sᶜ, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, f x ∂μ)

Tactic:
have := setIntegral_union₀ disjoint_compl_right.aedisjoint
    hs.compl hfi.integrableOn hfi.integrableOn
-- 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
s : Set X
μ : Measure X
hs : NullMeasurableSet s μ
hfi : Integrable f μ
this : ∫ (x : X) in s ∪ sᶜ, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, f x ∂μ)
rw : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ sᶜ, f x ∂μ) (∫ (x : X), f x ∂μ)
rw₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in univ, f x ∂μ) (∫ (x : X), f x ∂μ)
rw₂ rw₃ : Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X), f x ∂μ)
⊢ HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, f x ∂μ) = ∫ (x : X), f x ∂μ

Tactic:
rw [← this, union_compl_self, setIntegral_univ]

Premises used: Set.union_compl_self, MeasureTheory.setIntegral_univ
-- 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
s : Set X
μ : Measure X
hs : MeasurableSet s
hfi : Integrable f μ
⊢ HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, f x ∂μ) = ∫ (x : X), f x ∂μ

Tactic:
integral_add_compl₀ hs.nullMeasurableSet hfi

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.integral_add_compl₀
-- 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
s : Set X
μ : Measure X
hs : NullMeasurableSet s μ
hfi : Integrable f μ
rw :
  ∫ (x : X) in sᶜ, f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, f x ∂μ) - ∫ (x : X) in s, f x ∂μ
rw₁ rw₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in sᶜ, f x ∂μ) (∫ (x : X) in sᶜ, f x ∂μ)
⊢ ∫ (x : X) in sᶜ, f x ∂μ = HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ)

Tactic:
rw [← integral_add_compl₀ (μ := μ) hs hfi, add_sub_cancel_left]

Premises used: add_sub_cancel_left, MeasureTheory.integral_add_compl₀
-- 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
s : Set X
μ : Measure X
hs : MeasurableSet s
hfi : Integrable f μ
⊢ ∫ (x : X) in sᶜ, f x ∂μ = HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ)

Tactic:
setIntegral_compl₀ hs.nullMeasurableSet hfi

Premises used: MeasureTheory.setIntegral_compl₀, MeasurableSet.nullMeasurableSet
-- 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
s : Set X
μ : Measure X
hs : MeasurableSet s
pos : ∀ (hfi : IntegrableOn f s μ), Eq.{u_3 + 1} (α := E) (∫ (x : X), s.indicator f x ∂μ) (∫ (x : X) in s, f x ∂μ)
neg : ∀ (hfi : ¬IntegrableOn f s μ), Eq.{u_3 + 1} (α := E) (∫ (x : X), s.indicator f x ∂μ) (∫ (x : X) in s, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), s.indicator f x ∂μ) (∫ (x : X) in s, f x ∂μ)

Tactic:
by_cases hfi : IntegrableOn f s μ

Premises used: MeasureTheory.IntegrableOn
-- 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
s : Set X
μ : Measure X
hs : MeasurableSet s
hfi : ¬IntegrableOn f s μ
neg : ¬Integrable (s.indicator f) μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), s.indicator f x ∂μ) (∫ (x : X) in s, f x ∂μ)

Tactic:
rw [integral_undef hfi, 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
s : Set X
μ : Measure X
hs : MeasurableSet s
hfi : ¬IntegrableOn f s μ
neg neg₁ neg₂ neg₃ : ¬IntegrableOn f s μ
⊢ ¬Integrable (s.indicator f) μ

Tactic:
rwa [integrable_indicator_iff hs]

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
s : Set X
μ : Measure X
hs : MeasurableSet s
hfi : IntegrableOn f s μ
⊢ ∫ (x : X), s.indicator f x ∂μ =
    HAdd.hAdd (α := E) (∫ (x : X) in s, s.indicator f x ∂μ) (∫ (x : X) in sᶜ, s.indicator f x ∂μ)

Tactic:
(integral_add_compl hs (hfi.integrable_indicator hs)).symm

Premises used: MeasureTheory.IntegrableOn.integrable_indicator, MeasureTheory.integral_add_compl, 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
s : Set X
μ : Measure X
hs : MeasurableSet s
hfi : IntegrableOn f s μ
⊢ HAdd.hAdd (α := E) (∫ (x : X) in s, s.indicator f x ∂μ) (∫ (x : X) in sᶜ, s.indicator f x ∂μ) =
    HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, 0 ∂μ)

Tactic:
(congr_arg₂ (· + ·) (integral_congr_ae (indicator_ae_eq_restrict hs))
        (integral_congr_ae (indicator_ae_eq_restrict_compl hs)))

Premises used: MeasureTheory.integral_congr_ae, indicator_ae_eq_restrict_compl, HAdd.hAdd, indicator_ae_eq_restrict, congr_arg₂
-- 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
s : Set X
μ : Measure X
hs : MeasurableSet s
hfi : IntegrableOn f s μ
⊢ HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, 0 ∂μ) = ∫ (x : X) in s, f x ∂μ

Tactic:
simp
-- 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
s : Set X
μ : Measure X
hs : MeasurableSet s
hfi : IntegrableOn f s μ
indicator : HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, 0 ∂μ) = ∫ (x : X) in s, f x ∂μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), s.indicator f x ∂μ) (∫ (x : X) in s, f x ∂μ)

Tactic:
calc
    ∫ x, indicator s f x ∂μ = ∫ x in s, indicator s f x ∂μ + ∫ x in sᶜ, indicator s f x ∂μ :=
      (integral_add_compl hs (hfi.integrable_indicator hs)).symm
    _ = ∫ x in s, f x ∂μ + ∫ x in sᶜ, 0 ∂μ :=
      (congr_arg₂ (· + ·) (integral_congr_ae (indicator_ae_eq_restrict hs))
        (integral_congr_ae (indicator_ae_eq_restrict_compl hs)))
    _ = ∫ x in s, f x ∂μ := by simp

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.IntegrableOn.integrable_indicator, MeasureTheory.integral_add_compl, indicator_ae_eq_restrict_compl, HAdd.hAdd, Eq.symm, indicator_ae_eq_restrict, congr_arg₂
-- 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
s : Set X
μ : Measure X
hs : NullMeasurableSet s μ
rw : Eq.{u_3 + 1} (α := E) (∫ (a : X), (toMeasurable μ s).indicator f a ∂μ) (∫ (x : X) in s, f x ∂μ)
rw₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in toMeasurable μ s, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
rw₂ rw₃ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), s.indicator f x ∂μ) (∫ (x : X) in s, f x ∂μ)

Tactic:
rw [← integral_congr_ae (indicator_ae_eq_of_ae_eq_set hs.toMeasurable_ae_eq),
    integral_indicator (measurableSet_toMeasurable _ _),
    Measure.restrict_congr_set hs.toMeasurable_ae_eq]

Premises used: MeasureTheory.integral_indicator, MeasureTheory.Measure.restrict_congr_set, MeasureTheory.integral_congr_ae, indicator_ae_eq_of_ae_eq_set, MeasureTheory.measurableSet_toMeasurable, MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
Y : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure X
mY : MeasurableSpace Y
ν : Measure Y
f : X → Y → E
s : Set X
hs : MeasurableSet s
simp_rw :
  Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y), s.indicator (fun (x : X) ↦ f x y) x ∂ν ∂μ)
    (∫ (x : X), s.indicator (fun (x : X) ↦ ∫ (y : Y), f x y ∂ν) x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y), s.indicator (fun (x : X) ↦ f x y) x ∂ν ∂μ)
    (∫ (x : X) in s, ∫ (y : Y), f x y ∂ν ∂μ)

Tactic:
simp_rw [← integral_indicator hs, integral_indicator₂]

Premises used: MeasureTheory.integral_indicator₂, MeasureTheory.integral_indicator
-- 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
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 ∂μ)
rw₂ rw₃ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∩ t, 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 ∂μ)

Tactic:
rw [integral_indicator ht, Measure.restrict_restrict ht, Set.inter_comm]

Premises used: MeasureTheory.integral_indicator, MeasureTheory.Measure.restrict_restrict, Set.inter_comm
-- 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) μ
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 ∂μ)
⊢ 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 ∂μ))

Tactic:
simp_rw [← integral_smul, ← integral_indicator (Finset.measurableSet_biUnion _ hs)]

Premises used: MeasureTheory.integral_indicator, MeasureTheory.integral_smul, Finset.measurableSet_biUnion
-- 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) μ
u : Finset ι
hu : u ∈ {x ∈ t.powerset | x.Nonempty}
⊢ MeasurableSet.{u_1} (α := X) (⋂ i ∈ u, s i)

Tactic:
u.measurableSet_biInter fun i hi ↦ hs i ?_

Premises used: Finset.measurableSet_biInter
-- 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) μ
u : Finset ι
hu : u ∈ {x ∈ t.powerset | x.Nonempty}
refine : ∀ (i : ι) (hi : i ∈ u), i ∈ t
⊢ MeasurableSet.{u_1} (α := X) (⋂ i ∈ u, s i)

Tactic:
refine u.measurableSet_biInter fun i hi ↦ hs i ?_

Premises used: Finset.measurableSet_biInter
-- 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) μ
u : Finset ι
hu : u ∈ {x ∈ t.powerset | x.Nonempty}
i : ι
hi : i ∈ u
⊢ i ∈ t

Tactic:
grind
-- 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) μ
⊢ ∀ (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
-- 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)
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 ∂μ)
⊢ 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:
apply Finset.sum_congr rfl (fun x hx ↦ ?_)

Premises used: Finset.sum_congr, rfl
-- 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)
x : Finset ι
hx : x ∈ {x ∈ t.powerset | x.Nonempty}
rw 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 ∂μ)
⊢ 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:
rw [← integral_indicator (A x hx)]

Premises used: MeasureTheory.integral_indicator