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
t : Set X
μ : Measure X
hU : Ne.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) 0
⊢ ∃ᵐ (x : X) ∂μ.restrict t, f x ≠ 0

Tactic:
frequently_ae_ne_zero_of_integral_ne_zero hU

Premises used: MeasureTheory.frequently_ae_ne_zero_of_integral_ne_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
hU : Ne.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) 0
contrapose! : ∀ (hU : ∀ (x : X) (_ : x ∈ t), f x = 0), Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) 0
⊢ ∃ x ∈ t, f x ≠ 0

Tactic:
contrapose! hU
-- 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
hU : ∀ (x : X) (_ : x ∈ t), f x = 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) 0

Tactic:
setIntegral_eq_zero_of_forall_eq_zero hU

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

Tactic:
exact setIntegral_eq_zero_of_forall_eq_zero hU

Premises used: MeasureTheory.setIntegral_eq_zero_of_forall_eq_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
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- 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_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ MeasurableSet k

Tactic:
haux.measurable (measurableSet_singleton _)

Premises used: MeasurableSingletonClass.measurableSet_singleton, MeasureTheory.StronglyMeasurable.measurable
-- 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_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ MeasurableSet k

Tactic:
exact haux.measurable (measurableSet_singleton _)

Premises used: MeasurableSingletonClass.measurableSet_singleton, MeasureTheory.StronglyMeasurable.measurable
-- 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_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
⊢ MeasurableSet k

Tactic:
have hk : MeasurableSet k := by borelize E; exact haux.measurable (measurableSet_singleton _)
-- 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_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
⊢ IntegrableOn f s μ

Tactic:
have h's : IntegrableOn f s μ := H.mono subset_union_left le_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
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
⊢ ∀ (u : Set X), Eq.{u_3 + 1} (α := E) (∫ (x : X) in u ∩ k, f x ∂μ) 0

Tactic:
have A : ∀ u : Set X, ∫ x in u ∩ k, f x ∂μ = 0 := fun u =>
    setIntegral_eq_zero_of_forall_eq_zero fun x hx => hx.2
-- 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_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), Eq.{u_3 + 1} (α := E) (∫ (x : X) in u ∩ k, f x ∂μ) 0
rw : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t \ k ∪ s \ k, f x ∂μ) (∫ (x : X) in s \ k, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)

Tactic:
rw [← integral_inter_add_diff hk h's, ← integral_inter_add_diff hk H, A, A, zero_add, zero_add,
    union_diff_distrib, union_comm]

Premises used: MeasureTheory.integral_inter_add_diff, Set.union_comm, zero_add, Set.union_diff_distrib
-- 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_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), Eq.{u_3 + 1} (α := E) (∫ (x : X) in u ∩ k, f x ∂μ) 0
hst : t \ k ∪ s \ k =ᶠ[ae μ] s \ k
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t \ k ∪ s \ k, f x ∂μ) (∫ (x : X) in s \ k, f x ∂μ)

Tactic:
apply setIntegral_congr_set

Premises used: MeasureTheory.setIntegral_congr_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
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), Eq.{u_3 + 1} (α := E) (∫ (x : X) in u ∩ k, f x ∂μ) 0
hst : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((t \ k) \ (s \ k)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ t \ k ∪ s \ k =ᶠ[ae μ] s \ k

Tactic:
rw [union_ae_eq_right]

Premises used: MeasureTheory.union_ae_eq_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
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), Eq.{u_3 + 1} (α := E) (∫ (x : X) in u ∩ k, f x ∂μ) 0
hst : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (t \ k) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) ((t \ k) \ (s \ k)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
apply measure_mono_null diff_subset

Premises used: Set.diff_subset, MeasureTheory.measure_mono_null
-- 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_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), Eq.{u_3 + 1} (α := E) (∫ (x : X) in u ∩ k, f x ∂μ) 0
hst : ∀ᵐ (a : X) ∂μ, a ∉ t \ k
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (t \ k) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [measure_eq_zero_iff_ae_notMem]

Premises used: MeasureTheory.measure_eq_zero_iff_ae_notMem
-- 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_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), Eq.{u_3 + 1} (α := E) (∫ (x : X) in u ∩ k, f x ∂μ) 0
x : X
hx : x ∈ t → f x = 0
h'x : x ∈ t \ k
⊢ False

Tactic:
h'x.2 (hx h'x.1)

Premises used: And.right, 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
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
haux : StronglyMeasurable f
H : IntegrableOn f (s ∪ t) μ
k : Set X := f ⁻¹' {0}
hk : MeasurableSet k
h's : IntegrableOn f s μ
A : ∀ (u : Set X), Eq.{u_3 + 1} (α := E) (∫ (x : X) in u ∩ k, f x ∂μ) 0
h :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X |
        Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ x ∈ t → f x = 0) x} x →
          Membership.mem (γ := Set X) {x : X | (fun (a : X) ↦ a ∉ t \ k) x} x}
      a
h₁ : ∀ (a : X), (a ∈ t → f a = 0) → a ∉ t \ k
h₂ : ∀ (x : X) (hx : x ∈ t → f x = 0) (h'x : x ∈ t \ k), False
⊢ ∀ᵐ (a : X) ∂μ, a ∉ t \ k

Tactic:
filter_upwards [ae_imp_of_ae_restrict ht_eq] with x hx h'x using h'x.2 (hx h'x.1)

Premises used: 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
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
apply : (fun (x : X) ↦ 0) =ᶠ[ae (μ.restrict t)] f
⊢ IntegrableOn f t μ

Tactic:
apply integrableOn_zero.congr_fun_ae

Premises used: MeasureTheory.IntegrableOn.congr_fun_ae, MeasureTheory.integrableOn_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
s t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
symm : f =ᶠ[ae (μ.restrict t)] fun (x : X) ↦ 0
⊢ (fun (x : X) ↦ 0) =ᶠ[ae (μ.restrict t)] f

Tactic:
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 t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
⊢ f =ᶠ[ae (μ.restrict t)] fun (x : X) ↦ 0

Tactic:
ht_eq

Premises used: Filter.EventuallyEq
-- 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_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
⊢ f =ᶠ[ae (μ.restrict t)] fun (x : X) ↦ 0

Tactic:
exact ht_eq
-- 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_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
⊢ IntegrableOn f t μ

Tactic:
have ht : IntegrableOn f t μ := by apply integrableOn_zero.congr_fun_ae; symm; exact ht_eq
-- 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_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
ht : IntegrableOn f t μ
pos : ∀ (H : IntegrableOn f (s ∪ t) μ), Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
neg : ∀ (H : ¬IntegrableOn f (s ∪ t) μ), Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)

Tactic:
by_cases H : IntegrableOn f (s ∪ t) μ

Premises used: MeasureTheory.IntegrableOn, Union.union
-- 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_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
ht : IntegrableOn f t μ
H : ¬IntegrableOn f (s ∪ t) μ
neg : ¬Integrable f (μ.restrict s)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)

Tactic:
rw [integral_undef H, 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 t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ.restrict t, f x = 0
ht : IntegrableOn f t μ
H : ¬IntegrableOn f (s ∪ t) μ
⊢ ¬Integrable f (μ.restrict s)

Tactic:
simpa [integrableOn_union, ht] using H

Premises used: MeasureTheory.integrableOn_union
-- 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_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 ∪ t, f' x ∂μ)

Tactic:
integral_congr_ae H.1.ae_eq_mk

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, 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
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 ⋯
integral_union_eq_left_of_ae_aux : ∀ᵐ (x : X) ∂μ.restrict t, AEStronglyMeasurable.mk f ⋯ x = 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f' x ∂μ) (∫ (x : X) in s, f' x ∂μ)

Tactic:
apply
        integral_union_eq_left_of_ae_aux _ H.1.stronglyMeasurable_mk (H.congr_fun_ae H.1.ae_eq_mk)

Premises used: MeasureTheory.integral_union_eq_left_of_ae_aux, MeasureTheory.IntegrableOn.congr_fun_ae, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, 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
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 ⋯
h : ∀ (x : X) (hx : f x = 0) (h'x : f x = AEStronglyMeasurable.mk f ⋯ x), AEStronglyMeasurable.mk f ⋯ x = 0
⊢ ∀ᵐ (x : X) ∂μ.restrict t, AEStronglyMeasurable.mk f ⋯ x = 0

Tactic:
filter_upwards [ht_eq,
        ae_mono (Measure.restrict_mono subset_union_right le_rfl) H.1.ae_eq_mk] with x hx h'x

Premises used: le_rfl, MeasureTheory.Measure.restrict_mono, Set.subset_union_right, MeasureTheory.ae_mono, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, 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
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 ⋯
x : X
hx : f x = 0
h'x : f x = AEStronglyMeasurable.mk f ⋯ x
h : f x = 0
h₁ h₂ : Eq.{u_3 + 1} (α := E) 0 0
⊢ AEStronglyMeasurable.mk f ⋯ x = 0

Tactic:
rw [← h'x, hx]
-- 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_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, f' x ∂μ) (∫ (x : X) in s, f x ∂μ)

Tactic:
integral_congr_ae
        (ae_mono (Measure.restrict_mono subset_union_left le_rfl) H.1.ae_eq_mk.symm)

Premises used: le_rfl, MeasureTheory.integral_congr_ae, MeasureTheory.Measure.restrict_mono, MeasureTheory.ae_mono, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, Set.subset_union_left, And.left, Filter.EventuallyEq.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 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 ⋯
x : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f' x ∂μ) (∫ (x : X) in s, f' 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)

Premises used: le_rfl, MeasureTheory.integral_congr_ae, MeasureTheory.Measure.restrict_mono, MeasureTheory.ae_mono, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, Set.subset_union_left, And.left, Filter.EventuallyEq.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
s t : Set X
μ : Measure X
f : X → E
ht : NullMeasurableSet t μ
ht_eq : ∀ x ∈ t, f x = 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)

Tactic:
integral_union_eq_left_of_ae ((ae_restrict_iff'₀ ht).2 (Eventually.of_forall ht_eq))

Premises used: Iff.mpr, Filter.Eventually.of_forall, MeasureTheory.ae_restrict_iff'₀, MeasureTheory.integral_union_eq_left_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
s t : Set X
μ : Measure X
f : X → E
ht : MeasurableSet t
ht_eq : ∀ x ∈ t, f x = 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s ∪ t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)

Tactic:
integral_union_eq_left_of_forall₀ ht.nullMeasurableSet ht_eq

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.integral_union_eq_left_of_forall₀
-- 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
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}
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- 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
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}
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ MeasurableSet k

Tactic:
haux.measurable (measurableSet_singleton _)

Premises used: MeasurableSingletonClass.measurableSet_singleton, MeasureTheory.StronglyMeasurable.measurable
-- 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
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}
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ MeasurableSet k

Tactic:
exact haux.measurable (measurableSet_singleton _)

Premises used: MeasurableSingletonClass.measurableSet_singleton, MeasureTheory.StronglyMeasurable.measurable
-- 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
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

Tactic:
have hk : MeasurableSet k := by borelize E; exact haux.measurable (measurableSet_singleton _)
-- 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
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
rw rw₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in t, f 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:
rw [integral_inter_add_diff hk h'aux]

Premises used: MeasureTheory.integral_inter_add_diff
-- 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
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
rw : ∀ (x : X) (hx : x ∈ t ∩ k), f x = 0
⊢ 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:
rw [setIntegral_eq_zero_of_forall_eq_zero fun x hx => ?_, zero_add]

Premises used: zero_add, MeasureTheory.setIntegral_eq_zero_of_forall_eq_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
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 ∩ k
⊢ f x = 0

Tactic:
hx.2

Premises used: Set.Mem, setOf, And.right, Set.preimage, Set.singleton
-- 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
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 ∩ k
⊢ f x = 0

Tactic:
exact hx.2

Premises used: And.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
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
hst : t \ k =ᶠ[ae μ] s \ k
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t \ k, f x ∂μ) (∫ (x : X) in s \ k, f x ∂μ)

Tactic:
apply setIntegral_congr_set

Premises used: MeasureTheory.setIntegral_congr_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
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
h : ∀ (x : X) (hx : x ∈ t \ s → f x = 0), (t \ k) x = (s \ k) x
⊢ t \ k =ᶠ[ae μ] s \ k

Tactic:
filter_upwards [h't] with x hx
-- 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
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 ∉ k → (x ∈ t ↔ x ∈ s)
⊢ (x ∈ t \ k) = (x ∈ s \ k)

Tactic:
simp only [eq_iff_iff, and_congr_left_iff, mem_diff]

Premises used: Set.mem_diff, and_congr_left_iff, eq_iff_iff