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_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
ht : IntegrableOn f t μ
H : IntegrableOn f (s ∪ t) μ
f' : X → E := AEStronglyMeasurable.mk f ⋯
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have x : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f' x ∂μ) (∫ (x : X) in s, f' x ∂μ)
Tactic: calc
    ∫ x : X in s ∪ t, f x ∂μ = ∫ x : X in s ∪ t, f' x ∂μ := integral_congr_ae H.1.ae_eq_mk
    _ = ∫ x in s, f' x ∂μ := by
      apply
        integral_union_eq_left_of_ae_aux _ H.1.stronglyMeasurable_mk (H.congr_fun_ae H.1.ae_eq_mk)
      filter_upwards [ht_eq,
        ae_mono (Measure.restrict_mono subset_union_right le_rfl) H.1.ae_eq_mk] with x hx h'x
      rw [← h'x, hx]
    _ = ∫ x in s, f x ∂μ :=
      integral_congr_ae
        (ae_mono (Measure.restrict_mono subset_union_left le_rfl) H.1.ae_eq_mk.symm)
-- 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 t : Set X
μ : Measure X
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
⊢ MeasurableSet k
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- 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 t : Set X
μ : Measure X
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have hk : MeasurableSet k
Tactic: have hk : MeasurableSet k := by borelize E; exact haux.measurable (measurableSet_singleton _)
-- 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
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
⊢ ∫ (x : X) in t, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in t ∩ k, f x ∂μ) (∫ (x : X) in t \ k, f x ∂μ)
have rw : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in t, f x ∂μ)
Tactic: rw [integral_inter_add_diff hk h'aux]
-- 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
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
⊢ HAdd.hAdd (α := E) (∫ (x : X) in t ∩ k, f x ∂μ) (∫ (x : X) in t \ k, f x ∂μ) = ∫ (x : X) in t \ k, f x ∂μ
have rw : ∀ (x : X) (hx : x ∈ t ∩ k), f x = 0
Tactic: rw [setIntegral_eq_zero_of_forall_eq_zero fun x hx => ?_, zero_add]
-- 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
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t \ k, f x ∂μ) (∫ (x : X) in s \ k, f x ∂μ)
have hst : t \ k =ᶠ[ae μ] s \ k
Tactic: apply 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
f : X → E
s t : Set X
μ : Measure X
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
⊢ t \ k =ᶠ[ae μ] s \ k
have h : ∀ (x : X) (hx : x ∈ t \ s → f x = 0), (t \ k) x = (s \ k) x
Tactic: filter_upwards [h't] with 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
s t : Set X
μ : Measure X
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
x : X
hx : x ∈ t \ s → f x = 0
⊢ (x ∈ t \ k) = (x ∈ s \ k)
have h : x ∉ k → (x ∈ t ↔ x ∈ s)
Tactic: simp only [eq_iff_iff, and_congr_left_iff, mem_diff]
-- 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
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
x : X
hx : x ∈ t \ s → f x = 0
h'x : x ∉ k
⊢ x ∈ t ↔ x ∈ s
have pos : ∀ (xs : x ∈ s), x ∈ t ↔ x ∈ s
Tactic: by_cases xs : x ∈ 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 t : Set X
μ : Measure X
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
x : X
hx : x ∈ t \ s → f x = 0
h'x : x ∉ k
pos : ∀ (xs : x ∈ s), x ∈ t ↔ x ∈ s
⊢ x ∈ t ↔ x ∈ s
have neg : ∀ (xs : x ∉ s), x ∈ t ↔ x ∈ s
Tactic: by_cases xs : x ∈ 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 t : Set X
μ : Measure X
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
x : X
hx : x ∈ t \ s → f x = 0
h'x : x ∉ k
xs : x ∉ s
⊢ x ∈ t ↔ x ∈ s
have neg : x ∉ t
Tactic: simp only [xs, iff_false]
-- 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 t : Set X
μ : Measure X
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
⊢ ∫ (x : X) in s \ k, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in s ∩ k, f x ∂μ) (∫ (x : X) in s \ k, f x ∂μ)
have this : ∀ x ∈ s ∩ k, f x = 0
Tactic: have : ∀ x ∈ s ∩ k, f x = 0 := fun x hx => hx.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
s t : Set X
μ : Measure X
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
this : ∀ x ∈ s ∩ k, f x = 0
⊢ ∫ (x : X) in s \ k, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in s ∩ k, f x ∂μ) (∫ (x : X) in s \ k, f x ∂μ)
have rw : ∫ (x : X) in s \ k, f x ∂μ = HAdd.hAdd (α := E) 0 (∫ (x : X) in s \ k, f x ∂μ)
Tactic: rw [setIntegral_eq_zero_of_forall_eq_zero this, zero_add]
-- 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
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
this : ∀ x ∈ s ∩ k, f x = 0
rw : ∫ (x : X) in s \ k, f x ∂μ = HAdd.hAdd (α := E) 0 (∫ (x : X) in s \ k, f x ∂μ)
⊢ ∫ (x : X) in s \ k, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in s ∩ k, f x ∂μ) (∫ (x : X) in s \ k, f x ∂μ)
have rw₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s \ k, f x ∂μ) (∫ (x : X) in s \ k, f x ∂μ)
Tactic: rw [setIntegral_eq_zero_of_forall_eq_zero this, zero_add]
-- 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
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
⊢ HAdd.hAdd (α := E) (∫ (x : X) in s ∩ k, f x ∂μ) (∫ (x : X) in s \ k, 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_inter_add_diff hk (h'aux.mono hts le_rfl)]
-- 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
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have x : ∫ (x : X) in t, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in t ∩ k, f x ∂μ) (∫ (x : X) in t \ k, f x ∂μ)
Tactic: calc
    ∫ x in t, f x ∂μ = ∫ x in t ∩ k, f x ∂μ + ∫ x in t \ k, f x ∂μ := by
      rw [integral_inter_add_diff hk h'aux]
    _ = ∫ x in t \ k, f x ∂μ := by
      rw [setIntegral_eq_zero_of_forall_eq_zero fun x hx => ?_, zero_add]; exact hx.2
    _ = ∫ x in s \ k, f x ∂μ := by
      apply setIntegral_congr_set
      filter_upwards [h't] with x hx
      change (x ∈ t \ k) = (x ∈ s \ k)
      simp only [eq_iff_iff, and_congr_left_iff, mem_diff]
      intro h'x
      by_cases xs : x ∈ s
      · simp only [xs, hts xs]
      · simp only [xs, iff_false]
        intro xt
        exact h'x (hx ⟨xt, xs⟩)
    _ = ∫ x in s ∩ k, f x ∂μ + ∫ x in s \ k, f x ∂μ := by
      have : ∀ x ∈ s ∩ k, f x = 0 := fun x hx => hx.2
      rw [setIntegral_eq_zero_of_forall_eq_zero this, zero_add]
    _ = ∫ x in s, f x ∂μ := by rw [integral_inter_add_diff hk (h'aux.mono hts le_rfl)]
-- 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
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
x : ∫ (x : X) in t, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in t ∩ k, f x ∂μ) (∫ (x : X) in t \ k, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have x₁ : HAdd.hAdd (α := E) (∫ (x : X) in t ∩ k, f x ∂μ) (∫ (x : X) in t \ k, f x ∂μ) = ∫ (x : X) in t \ k, f x ∂μ
Tactic: calc
    ∫ x in t, f x ∂μ = ∫ x in t ∩ k, f x ∂μ + ∫ x in t \ k, f x ∂μ := by
      rw [integral_inter_add_diff hk h'aux]
    _ = ∫ x in t \ k, f x ∂μ := by
      rw [setIntegral_eq_zero_of_forall_eq_zero fun x hx => ?_, zero_add]; exact hx.2
    _ = ∫ x in s \ k, f x ∂μ := by
      apply setIntegral_congr_set
      filter_upwards [h't] with x hx
      change (x ∈ t \ k) = (x ∈ s \ k)
      simp only [eq_iff_iff, and_congr_left_iff, mem_diff]
      intro h'x
      by_cases xs : x ∈ s
      · simp only [xs, hts xs]
      · simp only [xs, iff_false]
        intro xt
        exact h'x (hx ⟨xt, xs⟩)
    _ = ∫ x in s ∩ k, f x ∂μ + ∫ x in s \ k, f x ∂μ := by
      have : ∀ x ∈ s ∩ k, f x = 0 := fun x hx => hx.2
      rw [setIntegral_eq_zero_of_forall_eq_zero this, zero_add]
    _ = ∫ x in s, f x ∂μ := by rw [integral_inter_add_diff hk (h'aux.mono hts le_rfl)]
-- 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
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
x : ∫ (x : X) in t, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in t ∩ k, f x ∂μ) (∫ (x : X) in t \ k, f x ∂μ)
x₁ : HAdd.hAdd (α := E) (∫ (x : X) in t ∩ k, f x ∂μ) (∫ (x : X) in t \ k, f x ∂μ) = ∫ (x : X) in t \ k, f x ∂μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have x₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t \ k, f x ∂μ) (∫ (x : X) in s \ k, f x ∂μ)
Tactic: calc
    ∫ x in t, f x ∂μ = ∫ x in t ∩ k, f x ∂μ + ∫ x in t \ k, f x ∂μ := by
      rw [integral_inter_add_diff hk h'aux]
    _ = ∫ x in t \ k, f x ∂μ := by
      rw [setIntegral_eq_zero_of_forall_eq_zero fun x hx => ?_, zero_add]; exact hx.2
    _ = ∫ x in s \ k, f x ∂μ := by
      apply setIntegral_congr_set
      filter_upwards [h't] with x hx
      change (x ∈ t \ k) = (x ∈ s \ k)
      simp only [eq_iff_iff, and_congr_left_iff, mem_diff]
      intro h'x
      by_cases xs : x ∈ s
      · simp only [xs, hts xs]
      · simp only [xs, iff_false]
        intro xt
        exact h'x (hx ⟨xt, xs⟩)
    _ = ∫ x in s ∩ k, f x ∂μ + ∫ x in s \ k, f x ∂μ := by
      have : ∀ x ∈ s ∩ k, f x = 0 := fun x hx => hx.2
      rw [setIntegral_eq_zero_of_forall_eq_zero this, zero_add]
    _ = ∫ x in s, f x ∂μ := by rw [integral_inter_add_diff hk (h'aux.mono hts le_rfl)]
-- 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
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
x : ∫ (x : X) in t, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in t ∩ k, f x ∂μ) (∫ (x : X) in t \ k, f x ∂μ)
x₁ : HAdd.hAdd (α := E) (∫ (x : X) in t ∩ k, f x ∂μ) (∫ (x : X) in t \ k, f x ∂μ) = ∫ (x : X) in t \ k, f x ∂μ
x₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t \ k, f x ∂μ) (∫ (x : X) in s \ k, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have x₃ : ∫ (x : X) in s \ k, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in s ∩ k, f x ∂μ) (∫ (x : X) in s \ k, f x ∂μ)
Tactic: calc
    ∫ x in t, f x ∂μ = ∫ x in t ∩ k, f x ∂μ + ∫ x in t \ k, f x ∂μ := by
      rw [integral_inter_add_diff hk h'aux]
    _ = ∫ x in t \ k, f x ∂μ := by
      rw [setIntegral_eq_zero_of_forall_eq_zero fun x hx => ?_, zero_add]; exact hx.2
    _ = ∫ x in s \ k, f x ∂μ := by
      apply setIntegral_congr_set
      filter_upwards [h't] with x hx
      change (x ∈ t \ k) = (x ∈ s \ k)
      simp only [eq_iff_iff, and_congr_left_iff, mem_diff]
      intro h'x
      by_cases xs : x ∈ s
      · simp only [xs, hts xs]
      · simp only [xs, iff_false]
        intro xt
        exact h'x (hx ⟨xt, xs⟩)
    _ = ∫ x in s ∩ k, f x ∂μ + ∫ x in s \ k, f x ∂μ := by
      have : ∀ x ∈ s ∩ k, f x = 0 := fun x hx => hx.2
      rw [setIntegral_eq_zero_of_forall_eq_zero this, zero_add]
    _ = ∫ x in s, f x ∂μ := by rw [integral_inter_add_diff hk (h'aux.mono hts le_rfl)]
-- 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
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
haux : StronglyMeasurable f
h'aux : IntegrableOn f t μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
x : ∫ (x : X) in t, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in t ∩ k, f x ∂μ) (∫ (x : X) in t \ k, f x ∂μ)
x₁ : HAdd.hAdd (α := E) (∫ (x : X) in t ∩ k, f x ∂μ) (∫ (x : X) in t \ k, f x ∂μ) = ∫ (x : X) in t \ k, f x ∂μ
x₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t \ k, f x ∂μ) (∫ (x : X) in s \ k, f x ∂μ)
x₃ : ∫ (x : X) in s \ k, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in s ∩ k, f x ∂μ) (∫ (x : X) in s \ k, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have x₄ : HAdd.hAdd (α := E) (∫ (x : X) in s ∩ k, f x ∂μ) (∫ (x : X) in s \ k, f x ∂μ) = ∫ (x : X) in s, f x ∂μ
Tactic: calc
    ∫ x in t, f x ∂μ = ∫ x in t ∩ k, f x ∂μ + ∫ x in t \ k, f x ∂μ := by
      rw [integral_inter_add_diff hk h'aux]
    _ = ∫ x in t \ k, f x ∂μ := by
      rw [setIntegral_eq_zero_of_forall_eq_zero fun x hx => ?_, zero_add]; exact hx.2
    _ = ∫ x in s \ k, f x ∂μ := by
      apply setIntegral_congr_set
      filter_upwards [h't] with x hx
      change (x ∈ t \ k) = (x ∈ s \ k)
      simp only [eq_iff_iff, and_congr_left_iff, mem_diff]
      intro h'x
      by_cases xs : x ∈ s
      · simp only [xs, hts xs]
      · simp only [xs, iff_false]
        intro xt
        exact h'x (hx ⟨xt, xs⟩)
    _ = ∫ x in s ∩ k, f x ∂μ + ∫ x in s \ k, f x ∂μ := by
      have : ∀ x ∈ s ∩ k, f x = 0 := fun x hx => hx.2
      rw [setIntegral_eq_zero_of_forall_eq_zero this, zero_add]
    _ = ∫ x in s, f x ∂μ := by rw [integral_inter_add_diff hk (h'aux.mono hts le_rfl)]
-- 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 : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have pos : ∀ (h : IntegrableOn f t μ), Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
Tactic: by_cases h : IntegrableOn f t μ
-- 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 : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
pos : ∀ (h : IntegrableOn f t μ), Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have neg : ∀ (h : ¬IntegrableOn f t μ), Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
Tactic: by_cases h : IntegrableOn f t μ
-- 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 t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
h : ¬IntegrableOn f t μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have this : ¬IntegrableOn f s μ
Tactic: have : ¬IntegrableOn f s μ := fun H => h (H.of_ae_diff_eq_zero ht h't)
-- 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 : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
h : ¬IntegrableOn f t μ
this : ¬IntegrableOn f s μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have neg : Eq.{u_3 + 1} (α := E) 0 (∫ (x : X) in s, f x ∂μ)
Tactic: rw [integral_undef h, integral_undef this]
-- 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 : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
h : ¬IntegrableOn f t μ
this : ¬IntegrableOn f s μ
neg : Eq.{u_3 + 1} (α := E) 0 (∫ (x : X) in s, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have neg₁ : Eq.{u_3 + 1} (α := E) 0 0
Tactic: rw [integral_undef h, integral_undef this]
-- 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 : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t μ
f' : X → E := AEStronglyMeasurable.mk f ⋯
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f' x ∂μ) (∫ (x : X) in s, f' x ∂μ)
have setIntegral_eq_of_subset_of_ae_diff_eq_zero_aux : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → AEStronglyMeasurable.mk f sorry x = 0
Tactic: apply
        setIntegral_eq_of_subset_of_ae_diff_eq_zero_aux hts _ h.1.stronglyMeasurable_mk
          (h.congr h.1.ae_eq_mk)
-- 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 : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t μ
f' : X → E := AEStronglyMeasurable.mk f ⋯
⊢ ∀ᵐ (x : X) ∂μ, x ∈ t \ s → AEStronglyMeasurable.mk f ⋯ x = 0
have h₁ : ∀ (x : X) (hx : x ∈ t \ s → f x = 0) (h'x : x ∈ t → f x = AEStronglyMeasurable.mk f sorry x) (h''x : x ∈ t \ s),
  AEStronglyMeasurable.mk f sorry x = 0
Tactic: filter_upwards [h't, ae_imp_of_ae_restrict h.1.ae_eq_mk] with x hx h'x h''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
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t μ
f' : X → E := AEStronglyMeasurable.mk f ⋯
x : X
hx : x ∈ t \ s → f x = 0
h'x : x ∈ t → f x = AEStronglyMeasurable.mk f ⋯ x
h''x : x ∈ t \ s
⊢ AEStronglyMeasurable.mk f ⋯ x = 0
have h₁ : f x = 0
Tactic: rw [← h'x h''x.1, hx h''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
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t μ
f' : X → E := AEStronglyMeasurable.mk f ⋯
x : X
hx : x ∈ t \ s → f x = 0
h'x : x ∈ t → f x = AEStronglyMeasurable.mk f ⋯ x
h''x : x ∈ t \ s
h₁ : f x = 0
⊢ AEStronglyMeasurable.mk f ⋯ x = 0
have h₂ : Eq.{u_3 + 1} (α := E) 0 0
Tactic: rw [← h'x h''x.1, hx h''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
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t μ
f' : X → E := AEStronglyMeasurable.mk f ⋯
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f' x ∂μ) (∫ (x : X) in s, f x ∂μ)
have h₁ : f' =ᶠ[ae (μ.restrict s)] f
Tactic: apply integral_congr_ae
-- 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 : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t μ
f' : X → E := AEStronglyMeasurable.mk f ⋯
⊢ f' =ᶠ[ae (μ.restrict s)] f
have h₁ : ∀ᵐ (x : X) ∂μ.restrict t, f' x = f x
Tactic: apply ae_restrict_of_ae_restrict_of_subset hts
-- 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 : NullMeasurableSet t μ
hts : s ⊆ t
h't : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0
h : IntegrableOn f t μ
f' : X → E := AEStronglyMeasurable.mk f ⋯
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
have x : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f' x ∂μ) (∫ (x : X) in s, f' x ∂μ)
Tactic: calc
    ∫ x in t, f x ∂μ = ∫ x in t, f' x ∂μ := integral_congr_ae h.1.ae_eq_mk
    _ = ∫ x in s, f' x ∂μ := by
      apply
        setIntegral_eq_of_subset_of_ae_diff_eq_zero_aux hts _ h.1.stronglyMeasurable_mk
          (h.congr h.1.ae_eq_mk)
      filter_upwards [h't, ae_imp_of_ae_restrict h.1.ae_eq_mk] with x hx h'x h''x
      rw [← h'x h''x.1, hx h''x]
    _ = ∫ x in s, f x ∂μ := by
      apply integral_congr_ae
      apply ae_restrict_of_ae_restrict_of_subset hts
      exact h.1.ae_eq_mk.symm