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
μ : 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
insert :
  HAdd.hAdd (α := E) (∫ (x : X) in s a, f x ∂μ) (∫ (x : X) in ⋃ i ∈ s_1, s i, f x ∂μ) =
    ∑ i ∈ Insert.insert a s_1, ∫ (x : X) in s i, f x ∂μ
rw : Disjoint (s a) (⋃ i ∈ s_1, s i)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s a ∪ ⋃ x ∈ s_1, s x, f x ∂μ)
    (∑ i ∈ Insert.insert a s_1, ∫ (x : X) in s i, f x ∂μ)
have rw₁ : MeasurableSet.{u_1} (α := X) (⋃ i ∈ s_1, s i)
Tactic: rw [setIntegral_union _ _ hf.1 (integrableOn_finset_iUnion.2 hf.2)]
-- 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
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
⊢ HAdd.hAdd (α := E) (∫ (x : X) in s a, f x ∂μ) (∫ (x : X) in ⋃ i ∈ s_1, s i, f x ∂μ) =
    ∑ i ∈ insert a s_1, ∫ (x : X) in s i, f x ∂μ
have insert : HAdd.hAdd (α := E) (∫ (x : X) in s a, f x ∂μ) (∫ (x : X) in ⋃ i ∈ s_1, s i, f x ∂μ) =
  HAdd.hAdd (α := E) (∫ (x : X) in s a, f x ∂μ) (∑ x ∈ s_1, ∫ (x : X) in s x, f x ∂μ)
Tactic: rw [Finset.sum_insert hat, IH hs.2 h's.1 hf.2]
-- 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
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
insert :
  HAdd.hAdd (α := E) (∫ (x : X) in s a, f x ∂μ) (∫ (x : X) in ⋃ i ∈ s_1, s i, f x ∂μ) =
    HAdd.hAdd (α := E) (∫ (x : X) in s a, f x ∂μ) (∑ x ∈ s_1, ∫ (x : X) in s x, f x ∂μ)
⊢ HAdd.hAdd (α := E) (∫ (x : X) in s a, f x ∂μ) (∫ (x : X) in ⋃ i ∈ s_1, s i, f x ∂μ) =
    ∑ i ∈ Insert.insert a s_1, ∫ (x : X) in s i, f x ∂μ
have insert₁ : HAdd.hAdd (α := E) (∫ (x : X) in s a, f x ∂μ) (∑ i ∈ s_1, ∫ (x : X) in s i, f x ∂μ) =
  HAdd.hAdd (α := E) (∫ (x : X) in s a, f x ∂μ) (∑ x ∈ s_1, ∫ (x : X) in s x, f x ∂μ)
Tactic: rw [Finset.sum_insert hat, IH hs.2 h's.1 hf.2]
-- 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
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
⊢ Disjoint (s a) (⋃ i ∈ s_1, s i)
have simp : ∀ (i : ι) (i_1 : i ∈ s_1), Disjoint (s a) (s i)
Tactic: simp only [disjoint_iUnion_right]
-- 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)
h's : (↑t : Set ι).Pairwise (Disjoint on s)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ) (∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ)
have 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 ∂μ)
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
Cleared hypotheses: t, hs, h's, hf
-- 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)
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 ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ) (∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ)
have 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 a s_1, MeasurableSet (s i)) (h's : (↑(insert a s_1) : Set ι).Pairwise (Disjoint on s))
  (hf : ∀ i ∈ insert a s_1, IntegrableOn f (s i) μ),
  Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ i ∈ insert a s_1, s i, f x ∂μ) (∑ i ∈ insert a s_1, ∫ (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
Cleared hypotheses: t, hs, h's, hf
-- 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)
h's : (↑t : Set ι).Pairwise (Disjoint on s)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ) (∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ)
have 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 ∂μ)
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
Cleared hypotheses: t, hs, h's, hf
-- 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)
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 ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ) (∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ)
have 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 a s_1, MeasurableSet (s i)) (h's : (↑(insert a s_1) : Set ι).Pairwise (Disjoint on s))
  (hf : ∀ i ∈ insert a s_1, IntegrableOn f (s i) μ),
  Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ i ∈ insert a s_1, s i, f x ∂μ) (∑ i ∈ insert a s_1, ∫ (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
Cleared hypotheses: t, hs, h's, hf
-- 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
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 : ι), s i, f x ∂μ) (∑ i : ι, ∫ (x : X) in s i, f x ∂μ)
have h : ∀ (x : ι), s x = ⋃ (_ : Membership.mem (γ := Finset ι) Finset.univ x), s x
Tactic: convert! integral_biUnion_finset Finset.univ (fun i _ => hs i) _ fun i _ => hf i
-- 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
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
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ (i : ι), s i, f x ∂μ) (∑ i : ι, ∫ (x : X) in s i, f x ∂μ)
have convert! : (↑Finset.univ : Set ι).Pairwise (Disjoint on s)
Tactic: convert! integral_biUnion_finset Finset.univ (fun i _ => hs i) _ fun i _ => hf i
-- 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
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in ∅, f x ∂μ) 0
have rw : Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mX 0 fun (x : X) ↦ f x) 0
Tactic: rw [Measure.restrict_empty, integral_zero_measure]
-- 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
rw : Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mX 0 fun (x : X) ↦ f x) 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in ∅, f x ∂μ) 0
have rw₁ : Eq.{u_3 + 1} (α := E) 0 0
Tactic: rw [Measure.restrict_empty, integral_zero_measure]
-- 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
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in univ, f x ∂μ) (∫ (x : X), f x ∂μ)
have rw : Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X), f x ∂μ)
Tactic: rw [Measure.restrict_univ]
-- 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
s : Set X
μ : Measure X
hs : ∀ᵐ (x : X) ∂μ, x ∈ s
f : X → E
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have rw : s =ᶠ[ae μ] univ
Tactic: rw [← setIntegral_univ, ← setIntegral_congr_set]
-- 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
s : Set X
μ : Measure X
hs : ∀ᵐ (x : X) ∂μ, x ∈ s
f : X → E
⊢ s =ᶠ[ae μ] univ
have rwa : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rwa [ae_eq_univ]
-- 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
s : Set X
μ : Measure X
hs : NullMeasurableSet s μ
hfi : Integrable f μ
⊢ HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, f x ∂μ) = ∫ (x : X), f x ∂μ
have this : ∫ (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
-- 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 : 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 ∂μ)
⊢ HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, f x ∂μ) = ∫ (x : X), f x ∂μ
have rw : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ sᶜ, f x ∂μ) (∫ (x : X), f x ∂μ)
Tactic: rw [← this, union_compl_self, setIntegral_univ]
-- 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 : 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 ∂μ)
⊢ HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, f x ∂μ) = ∫ (x : X), f x ∂μ
have rw₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in univ, f x ∂μ) (∫ (x : X), f x ∂μ)
Tactic: rw [← this, union_compl_self, setIntegral_univ]
-- 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 : 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 ∂μ)
⊢ HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, f x ∂μ) = ∫ (x : X), f x ∂μ
have rw₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X), f x ∂μ)
Tactic: rw [← this, union_compl_self, setIntegral_univ]
-- 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 : Set X
μ : Measure X
hs : NullMeasurableSet s μ
hfi : Integrable f μ
⊢ ∫ (x : X) in sᶜ, f x ∂μ = HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have 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 ∂μ
Tactic: rw [← integral_add_compl₀ (μ := μ) hs hfi, add_sub_cancel_left]
-- 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 : 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 ∂μ
⊢ ∫ (x : X) in sᶜ, f x ∂μ = HSub.hSub (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have rw₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in sᶜ, f x ∂μ) (∫ (x : X) in sᶜ, f x ∂μ)
Tactic: rw [← integral_add_compl₀ (μ := μ) hs hfi, add_sub_cancel_left]
-- 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 : Set X
μ : Measure X
hs : MeasurableSet s
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), s.indicator f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have pos : ∀ (hfi : IntegrableOn f s μ), Eq.{u_3 + 1} (α := E) (∫ (x : X), s.indicator f x ∂μ) (∫ (x : X) in s, f x ∂μ)
Tactic: by_cases hfi : IntegrableOn f s μ
-- 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 : 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 ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), s.indicator f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have neg : ∀ (hfi : ¬IntegrableOn f s μ), Eq.{u_3 + 1} (α := E) (∫ (x : X), s.indicator f x ∂μ) (∫ (x : X) in s, f x ∂μ)
Tactic: by_cases hfi : IntegrableOn f s μ
-- 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 : Set X
μ : Measure X
hs : MeasurableSet s
hfi : ¬IntegrableOn f s μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), s.indicator f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have neg : ¬Integrable (s.indicator f) μ
Tactic: rw [integral_undef hfi, integral_undef]
-- 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 : Set X
μ : Measure X
hs : MeasurableSet s
hfi : IntegrableOn f s μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), s.indicator f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have indicator : HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in sᶜ, 0 ∂μ) = ∫ (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
-- 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 : Set X
μ : Measure X
hs : NullMeasurableSet s μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), s.indicator f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have rw : Eq.{u_3 + 1} (α := E) (∫ (a : X), (toMeasurable μ s).indicator f a ∂μ) (∫ (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]
-- 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 : 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 ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), s.indicator f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have rw₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in toMeasurable μ s, 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]
-- 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 : 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 ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), s.indicator f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have rw₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Set (goal)
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
⊢ 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 ∂ν ∂μ)
have 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 ∂μ)
Tactic: simp_rw [← integral_indicator hs, integral_indicator₂]
-- 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
⊢ 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, f x ∂μ.restrict s) (∫ (x : X) in s ∩ t, f x ∂μ)
Tactic: rw [integral_indicator ht, Measure.restrict_restrict ht, Set.inter_comm]