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
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
neg : ∀ (xs : x ∉ s), x ∈ t ↔ x ∈ s
⊢ x ∈ t ↔ x ∈ s

Tactic:
by_cases xs : x ∈ s
-- 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 : x ∉ k
xs : x ∈ s
⊢ x ∈ t ↔ x ∈ s

Tactic:
simp only [xs, hts xs]
-- 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 : x ∉ k
xs : x ∉ s
neg : x ∉ t
⊢ x ∈ t ↔ x ∈ s

Tactic:
simp only [xs, iff_false]

Premises used: iff_false
-- 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 : x ∉ k
xs : x ∉ s
xt : x ∈ t
⊢ False

Tactic:
h'x (hx ⟨xt, xs⟩)

Premises used: And.intro
-- 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 : x ∉ k
xs : x ∉ s
xt : x ∈ t
⊢ False

Tactic:
exact h'x (hx ⟨xt, xs⟩)

Premises used: And.intro
-- 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 ∈ s ∩ k, f x = 0

Tactic:
have : ∀ x ∈ s ∩ k, f x = 0 := 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
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 ∂μ)
rw₁ rw₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s \ k, f x ∂μ) (∫ (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 ∂μ)

Tactic:
rw [setIntegral_eq_zero_of_forall_eq_zero this, 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
rw rw₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, f 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:
rw [integral_inter_add_diff hk (h'aux.mono hts le_rfl)]

Premises used: le_rfl, MeasureTheory.integral_inter_add_diff, MeasureTheory.IntegrableOn.mono
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
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 ∂μ)
x₄ : HAdd.hAdd (α := E) (∫ (x : X) in s ∩ k, f x ∂μ) (∫ (x : X) in s \ k, 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 ∂μ)

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)]
-- 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 : 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 ∂μ)
neg : ∀ (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 ∂μ)

Tactic:
by_cases h : IntegrableOn f t μ

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 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 μ
⊢ ¬IntegrableOn f s μ

Tactic:
have : ¬IntegrableOn f s μ := fun H => h (H.of_ae_diff_eq_zero ht h't)
-- 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 : 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 ∂μ)
neg₁ neg₂ : Eq.{u_3 + 1} (α := E) 0 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)

Tactic:
rw [integral_undef h, integral_undef this]

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 : 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 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 : 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 ⋯
setIntegral_eq_of_subset_of_ae_diff_eq_zero_aux : ∀ᵐ (x : X) ∂μ, x ∈ t \ s → AEStronglyMeasurable.mk f ⋯ x = 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f' x ∂μ) (∫ (x : X) in s, f' x ∂μ)

Tactic:
apply
        setIntegral_eq_of_subset_of_ae_diff_eq_zero_aux hts _ h.1.stronglyMeasurable_mk
          (h.congr h.1.ae_eq_mk)

Premises used: MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_eq_zero_aux, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, And.left, MeasureTheory.Integrable.congr
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
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 ⋯
h₁ :
  ∀ (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
⊢ ∀ᵐ (x : X) ∂μ, x ∈ t \ s → AEStronglyMeasurable.mk f ⋯ x = 0

Tactic:
filter_upwards [h't, ae_imp_of_ae_restrict h.1.ae_eq_mk] with x hx h'x h''x

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, And.left, 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 : 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
h₂ h₃ : Eq.{u_3 + 1} (α := E) 0 0
⊢ AEStronglyMeasurable.mk f ⋯ x = 0

Tactic:
rw [← h'x h''x.1, hx h''x]

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
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 ⋯
h₁ : f' =ᶠ[ae (μ.restrict s)] f
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f' x ∂μ) (∫ (x : X) in s, f x ∂μ)

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
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 ⋯
h₁ : ∀ᵐ (x : X) ∂μ.restrict t, f' x = f x
⊢ f' =ᶠ[ae (μ.restrict s)] f

Tactic:
apply ae_restrict_of_ae_restrict_of_subset hts

Premises used: MeasureTheory.ae_restrict_of_ae_restrict_of_subset
-- 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 : 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) ∂μ.restrict t, f' x = f x

Tactic:
h.1.ae_eq_mk.symm

Premises used: Filter.EventuallyEq, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, 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 : 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) ∂μ.restrict t, f' x = f x

Tactic:
exact h.1.ae_eq_mk.symm

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, 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 : 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 : Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f' x ∂μ) (∫ (x : X) in s, f' x ∂μ)
x₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, 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 ∂μ)

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

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 : MeasurableSet t
hts : s ⊆ t
h't : ∀ x ∈ t \ s, f x = 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in t, f x ∂μ) (∫ (x : X) in s, f x ∂μ)

Tactic:
setIntegral_eq_of_subset_of_ae_diff_eq_zero ht.nullMeasurableSet hts
    (Eventually.of_forall fun x hx => h't x hx)

Premises used: MeasurableSet.nullMeasurableSet, Filter.Eventually.of_forall, MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_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 : Set X
μ : Measure X
h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0
symm : Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X), f x ∂μ)

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 : Set X
μ : Measure X
h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0
nth_rw : Eq.{u_3 + 1} (α := E) (∫ (x : X) in univ, f x ∂μ) (∫ (x : X) in s, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), f x ∂μ) (∫ (x : X) in s, f x ∂μ)

Tactic:
nth_rw 1 [← setIntegral_univ]

Premises used: 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
h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0
apply : ∀ᵐ (x : X) ∂μ, x ∈ univ \ s → f x = 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in univ, f x ∂μ) (∫ (x : X) in s, f x ∂μ)

Tactic:
apply setIntegral_eq_of_subset_of_ae_diff_eq_zero nullMeasurableSet_univ (subset_univ _)

Premises used: Set.subset_univ, MeasureTheory.nullMeasurableSet_univ, MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_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 : Set X
μ : Measure X
h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0
x : X
hx : x ∉ s → f x = 0
h'x : x ∈ univ \ s
⊢ f x = 0

Tactic:
hx h'x.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 : Set X
μ : Measure X
h : ∀ᵐ (x : X) ∂μ, x ∉ s → f x = 0
h₁ :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X |
        Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ x ∉ s → f x = 0) x} x →
          Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ x ∈ univ \ s → f x = 0) x} x}
      a
h₂ h₃ : ∀ (x : X) (hx : x ∉ s → f x = 0) (h'x : x ∈ univ \ s), f x = 0
⊢ ∀ᵐ (x : X) ∂μ, x ∈ univ \ s → f x = 0

Tactic:
filter_upwards [h] with x hx h'x using hx h'x.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 : Set X
μ : Measure X
h : ∀ x ∉ s, f x = 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X), f x ∂μ)

Tactic:
setIntegral_eq_integral_of_ae_compl_eq_zero (Eventually.of_forall h)

Premises used: Filter.Eventually.of_forall, MeasureTheory.setIntegral_eq_integral_of_ae_compl_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
μ : Measure X
inst_2 : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
simp_rw : Eq.{u_1 + 1} (α := Set X) {x : X | f x < 0 ∨ f x = 0} ({x : X | f x < 0} ∪ {x : X | f x = 0})
⊢ Eq.{u_1 + 1} (α := Set X) {x : X | f x ≤ 0} ({x : X | f x < 0} ∪ {x : X | f x = 0})

Tactic:
simp_rw [le_iff_lt_or_eq, setOf_or]

Premises used: le_iff_lt_or_eq, Set.setOf_or
-- 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
μ : Measure X
inst_2 : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
⊢ Eq.{u_1 + 1} (α := Set X) {x : X | f x ≤ 0} ({x : X | f x < 0} ∪ {x : X | f x = 0})

Tactic:
have h_union : {x | f x ≤ 0} = {x | f x < 0} ∪ {x | f x = 0} := by
    simp_rw [le_iff_lt_or_eq, setOf_or]
-- 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
μ : Measure X
inst_2 : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
h_union : Eq.{u_1 + 1} (α := Set X) {x : X | f x ≤ 0} ({x : X | f x < 0} ∪ {x : X | f x = 0})
rw :
  Eq.{u_3 + 1} (α := E) (∫ (x : X) in {x : X | f x < 0}, f x ∂μ)
    (∫ (x : X) in {x : X | f x < 0} ∪ {x : X | f x = 0}, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in {x : X | f x < 0}, f x ∂μ) (∫ (x : X) in {x : X | f x ≤ 0}, f x ∂μ)

Tactic:
rw [h_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
μ : Measure X
inst_2 : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
h_union : Eq.{u_1 + 1} (α := Set X) {x : X | f x ≤ 0} ({x : X | f x < 0} ∪ {x : X | f x = 0})
⊢ NullMeasurableSet {x : X | f x = 0} μ

Tactic:
have B : NullMeasurableSet {x | f x = 0} μ :=
    hf.nullMeasurableSet_eq_fun aestronglyMeasurable_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
μ : Measure X
inst_2 : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
h_union : Eq.{u_1 + 1} (α := Set X) {x : X | f x ≤ 0} ({x : X | f x < 0} ∪ {x : X | f x = 0})
B : NullMeasurableSet {x : X | f x = 0} μ
symm :
  Eq.{u_3 + 1} (α := E) (∫ (x : X) in {x : X | f x < 0} ∪ {x : X | f x = 0}, f x ∂μ)
    (∫ (x : X) in {x : X | f x < 0}, f x ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in {x : X | f x < 0}, f x ∂μ)
    (∫ (x : X) in {x : X | f x < 0} ∪ {x : X | f x = 0}, f x ∂μ)

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
μ : Measure X
inst_2 : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
h_union : Eq.{u_1 + 1} (α := Set X) {x : X | f x ≤ 0} ({x : X | f x < 0} ∪ {x : X | f x = 0})
B : NullMeasurableSet {x : X | f x = 0} μ
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in {x : X | f x < 0} ∪ {x : X | f x = 0}, f x ∂μ)
    (∫ (x : X) in {x : X | f x < 0}, f x ∂μ)

Tactic:
integral_union_eq_left_of_ae ?_

Premises used: 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
μ : Measure X
inst_2 : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
h_union : Eq.{u_1 + 1} (α := Set X) {x : X | f x ≤ 0} ({x : X | f x < 0} ∪ {x : X | f x = 0})
B : NullMeasurableSet {x : X | f x = 0} μ
refine : ∀ᵐ (x : X) ∂μ.restrict {x : X | f x = 0}, f x = 0
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in {x : X | f x < 0} ∪ {x : X | f x = 0}, f x ∂μ)
    (∫ (x : X) in {x : X | f x < 0}, f x ∂μ)

Tactic:
refine integral_union_eq_left_of_ae ?_

Premises used: 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
μ : Measure X
inst_2 : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
h_union : Eq.{u_1 + 1} (α := Set X) {x : X | f x ≤ 0} ({x : X | f x < 0} ∪ {x : X | f x = 0})
B : NullMeasurableSet {x : X | f x = 0} μ
x : X
hx : f x = 0
⊢ f x = 0

Tactic:
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
μ : Measure X
inst_2 : PartialOrder E
f : X → E
hf : AEStronglyMeasurable f μ
h_union : Eq.{u_1 + 1} (α := Set X) {x : X | f x ≤ 0} ({x : X | f x < 0} ∪ {x : X | f x = 0})
B : NullMeasurableSet {x : X | f x = 0} μ
h :
  ∀ (a : X),
    Membership.mem (γ := Set X)
      {x : X |
        Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ Membership.mem (γ := Set X) {x : X | f x = 0} x) x} x →
          Membership.mem (γ := Set X) {x : X | (fun (x : X) ↦ f x = 0) x} x}
      a
h₁ h₂ : ∀ (x : X) (hx : f x = 0), f x = 0
⊢ ∀ᵐ (x : X) ∂μ.restrict {x : X | f x = 0}, f x = 0

Tactic:
filter_upwards [ae_restrict_mem₀ B] with x hx using hx

Premises used: MeasureTheory.ae_restrict_mem₀
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
rw rw₁ :
  HAdd.hAdd (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, ‖f x‖ ∂μ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ) =
    HAdd.hAdd (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, ‖f x‖ ∂μ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ)
⊢ ∫ (x : X), ‖f x‖ ∂μ =
    HAdd.hAdd (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, ‖f x‖ ∂μ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ)

Tactic:
rw [← integral_add_compl₀ h_meas hfi.norm]

Premises used: MeasureTheory.integral_add_compl₀, MeasureTheory.Integrable.norm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
e_a : Eq (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, ‖f x‖ ∂μ) (∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ)
⊢ HAdd.hAdd (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, ‖f x‖ ∂μ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ) =
    HAdd.hAdd (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ) (∫ (x : X) in {x : X | 0 ≤ f x}ᶜ, ‖f x‖ ∂μ)

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
mX : MeasurableSpace X
μ : Measure X
f : X → ℝ
hfi : Integrable f μ
h_meas : NullMeasurableSet {x : X | 0 ≤ f x} μ
⊢ Eq (α := ℝ) (∫ (x : X) in {x : X | 0 ≤ f x}, ‖f x‖ ∂μ) (∫ (x : X) in {x : X | 0 ≤ f x}, f x ∂μ)

Tactic:
setIntegral_congr_fun₀ h_meas fun x hx => ?_

Premises used: MeasureTheory.setIntegral_congr_fun₀