awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
⊢ norm (E := ↥(Lp E 1 μ) →L[ℝ] E) integralCLM ≤ 1

Tactic:
norm_setToL1_le (dominatedFinMeasAdditive_weightedSMul μ) zero_le_one

Premises used: MeasureTheory.L1.norm_setToL1_le, Set.Mem, MeasureTheory.L1.integralCLM', MeasureTheory.L1.integralCLM, zero_le_one, MeasureTheory.L1.SimpleFunc.integral, MeasureTheory.SimpleFunc.integral, MeasureTheory.L1.SimpleFunc.integralCLM', MeasureTheory.dominatedFinMeasAdditive_weightedSMul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
⊢ nnnorm (E := ↥(Lp E 1 μ) →L[ℝ] E) integralCLM ≤ 1

Tactic:
norm_Integral_le_one

Premises used: MeasureTheory.L1.norm_Integral_le_one
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ ‖integral f‖ = norm.{u_2} (E := E) ((integralCLM : (a : ↥(Lp E 1 μ)) → E) f : E)

Tactic:
simp only [integral]

Premises used: MeasureTheory.L1.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ ‖integral f‖₊ ≤ ‖f‖₊

Tactic:
norm_integral_le f

Premises used: MeasureTheory.L1.norm_integral_le
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
simp : Continuous (Y := E) fun (f : ↥(Lp E 1 μ)) ↦ (integralCLM : (a : ↥(Lp E 1 μ)) → E) f
⊢ Continuous (Y := E) fun (f : ↥(Lp E 1 μ)) ↦ integral f

Tactic:
simp only [integral]

Premises used: MeasureTheory.L1.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
⊢ Continuous (Y := E) fun (f : ↥(Lp E 1 μ)) ↦ (integralCLM : (a : ↥(Lp E 1 μ)) → E) f

Tactic:
L1.integralCLM.continuous

Premises used: MeasureTheory.L1.integralCLM, ContinuousLinearMap.continuous
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
⊢ Continuous (Y := E) fun (f : ↥(Lp E 1 μ)) ↦ (integralCLM : (a : ↥(Lp E 1 μ)) → E) f

Tactic:
exact L1.integralCLM.continuous

Premises used: MeasureTheory.L1.integralCLM, ContinuousLinearMap.continuous
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖

Tactic:
@isClosed_property _ _ _ ((↑) : (α →₁ₛ[μ] ℝ) → α →₁[μ] ℝ)
      (fun f : α →₁[μ] ℝ => integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖)
      (simpleFunc.denseRange one_ne_top) (isClosed_eq ?_ ?_) ?_ f

Premises used: MeasureTheory.Lp.simpleFunc.denseRange, isClosed_eq, isClosed_property, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
refine_1 : Continuous.{u_1, 0} (X := ↥(Lp ℝ 1 μ)) integral
refine_2 : Continuous (Y := ℝ) fun (x : ↥(Lp ℝ 1 μ)) ↦ ‖Lp.posPart x‖ - ‖Lp.negPart x‖
refine_3 :
  ∀ (a : ↥(simpleFunc ℝ 1 μ)), (fun (f : ↥(Lp ℝ 1 μ)) ↦ integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖) (↑a : ↥(Lp ℝ 1 μ))
⊢ integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖

Tactic:
refine @isClosed_property _ _ _ ((↑) : (α →₁ₛ[μ] ℝ) → α →₁[μ] ℝ)
      (fun f : α →₁[μ] ℝ => integral f = ‖Lp.posPart f‖ - ‖Lp.negPart f‖)
      (simpleFunc.denseRange one_ne_top) (isClosed_eq ?_ ?_) ?_ f

Premises used: MeasureTheory.Lp.simpleFunc.denseRange, isClosed_eq, isClosed_property, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
refine_1 : Continuous.{u_1, 0} (X := ↥(Lp ℝ 1 μ)) (Y := ℝ) (⇑integralCLM : (a : ↥(Lp ℝ 1 μ)) → ℝ)
⊢ Continuous.{u_1, 0} (X := ↥(Lp ℝ 1 μ)) integral

Tactic:
simp only [integral]

Premises used: MeasureTheory.L1.integral
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ Continuous.{u_1, 0} (X := ↥(Lp ℝ 1 μ)) (Y := ℝ) (⇑integralCLM : (a : ↥(Lp ℝ 1 μ)) → ℝ)

Tactic:
cont _

Premises used: ContinuousLinearMap.cont
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ Continuous.{u_1, 0} (X := ↥(Lp ℝ 1 μ)) (Y := ℝ) (⇑integralCLM : (a : ↥(Lp ℝ 1 μ)) → ℝ)

Tactic:
exact cont _

Premises used: ContinuousLinearMap.cont
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ Continuous (Y := ℝ) fun (x : ↥(Lp ℝ 1 μ)) ↦ ‖Lp.posPart x‖ - ‖Lp.negPart x‖

Tactic:
Continuous.sub (continuous_norm.comp Lp.continuous_posPart)
      (continuous_norm.comp Lp.continuous_negPart)

Premises used: Continuous.comp, MeasureTheory.Lp.continuous_negPart, Continuous.sub, continuous_norm, MeasureTheory.Lp.continuous_posPart
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
⊢ Continuous (Y := ℝ) fun (x : ↥(Lp ℝ 1 μ)) ↦ ‖Lp.posPart x‖ - ‖Lp.negPart x‖

Tactic:
refine Continuous.sub (continuous_norm.comp Lp.continuous_posPart)
      (continuous_norm.comp Lp.continuous_negPart)

Premises used: Continuous.comp, Continuous.sub, continuous_norm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
s : ↥(simpleFunc ℝ 1 μ)
refine_3 : SimpleFunc.integral s = ‖SimpleFunc.posPart s‖ - ‖SimpleFunc.negPart s‖
⊢ integral (↑s : ↥(Lp ℝ 1 μ)) = ‖Lp.posPart (↑s : ↥(Lp ℝ 1 μ))‖ - ‖Lp.negPart (↑s : ↥(Lp ℝ 1 μ))‖

Tactic:
norm_cast
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
s : ↥(simpleFunc ℝ 1 μ)
⊢ SimpleFunc.integral s = ‖SimpleFunc.posPart s‖ - ‖SimpleFunc.negPart s‖

Tactic:
SimpleFunc.integral_eq_norm_posPart_sub _

Premises used: MeasureTheory.L1.SimpleFunc.integral_eq_norm_posPart_sub
-- Module: Mathlib.MeasureTheory.Integral.Bochner.L1
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ↥(Lp ℝ 1 μ)
s : ↥(simpleFunc ℝ 1 μ)
⊢ SimpleFunc.integral s = ‖SimpleFunc.posPart s‖ - ‖SimpleFunc.negPart s‖

Tactic:
exact SimpleFunc.integral_eq_norm_posPart_sub _

Premises used: MeasureTheory.L1.SimpleFunc.integral_eq_norm_posPart_sub
-- 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 g : X → E
s : Set X
μ : Measure X
hs : NullMeasurableSet s μ
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x = g x
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)

Tactic:
integral_congr_ae ((ae_restrict_iff'₀ hs).2 h)

Premises used: Iff.mpr, MeasureTheory.integral_congr_ae, MeasureTheory.ae_restrict_iff'₀
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : X → E
s : Set X
μ : Measure X
hs : MeasurableSet s
h : ∀ᵐ (x : X) ∂μ, x ∈ s → f x = g x
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)

Tactic:
integral_congr_ae ((ae_restrict_iff' hs).2 h)

Premises used: Iff.mpr, MeasureTheory.integral_congr_ae, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f g : X → E
s : Set X
μ : Measure X
hs : NullMeasurableSet s μ
h : EqOn f g s
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)

Tactic:
setIntegral_congr_ae₀ hs <| Eventually.of_forall h

Premises used: Filter.Eventually.of_forall, MeasureTheory.setIntegral_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 g : X → E
s : Set X
μ : Measure X
hs : MeasurableSet s
h : EqOn f g s
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in s, g x ∂μ)

Tactic:
setIntegral_congr_ae hs <| Eventually.of_forall h

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

Tactic:
rw [Measure.restrict_congr_set hst]

Premises used: MeasureTheory.Measure.restrict_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
hst : AEDisjoint μ s t
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
⊢ ∫ (x : X) in s ∪ t, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in t, f x ∂μ)

Tactic:
simp only [Measure.restrict_union₀ hst ht, integral_add_measure hfs hft]

Premises used: MeasureTheory.integral_add_measure, MeasureTheory.Measure.restrict_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
hst : Disjoint s t
ht : MeasurableSet t
hfs : IntegrableOn f s μ
hft : IntegrableOn f t μ
⊢ ∫ (x : X) in s ∪ t, f x ∂μ = HAdd.hAdd (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in t, f x ∂μ)

Tactic:
setIntegral_union₀ hst.aedisjoint ht.nullMeasurableSet hfs hft

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.setIntegral_union₀, Disjoint.aedisjoint
-- 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 μ
hfs : IntegrableOn f s μ
hts : t ⊆ s
hst : AEDisjoint μ (s \ t) t
ht₁ : NullMeasurableSet t μ
hfs₁ : IntegrableOn f (s \ t) μ
hft : IntegrableOn f t μ
⊢ ∫ (x : X) in s \ t, f x ∂μ = HSub.hSub (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in t, f x ∂μ)

Tactic:
rw [eq_sub_iff_add_eq, ← setIntegral_union₀, diff_union_of_subset hts]

Premises used: eq_sub_iff_add_eq, MeasureTheory.setIntegral_union₀, Set.diff_union_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 μ
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ AEDisjoint μ (s \ t) t

Tactic:
disjoint_sdiff_self_left.aedisjoint

Premises used: Disjoint.aedisjoint, disjoint_sdiff_self_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 μ
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ NullMeasurableSet t μ

Tactic:
ht
-- 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 μ
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ IntegrableOn f (s \ t) μ

Tactic:
hfs.mono_set diff_subset

Premises used: Set.diff_subset, MeasureTheory.IntegrableOn.mono_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 : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ IntegrableOn f t μ

Tactic:
hfs.mono_set hts

Premises used: MeasureTheory.IntegrableOn.mono_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 : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ AEDisjoint μ (s \ t) t

Tactic:
exacts [disjoint_sdiff_self_left.aedisjoint, ht, hfs.mono_set diff_subset, hfs.mono_set hts]

Premises used: Set.diff_subset, MeasureTheory.IntegrableOn.mono_set, Disjoint.aedisjoint, disjoint_sdiff_self_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
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ ∫ (x : X) in s \ t, f x ∂μ = HSub.hSub (α := E) (∫ (x : X) in s, f x ∂μ) (∫ (x : X) in t, f x ∂μ)

Tactic:
setIntegral_diff₀ ht.nullMeasurableSet hfs hts

Premises used: MeasureTheory.setIntegral_diff₀, MeasurableSet.nullMeasurableSet
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
s t : Set X
μ : Measure X
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
hμ : Integrable f (μ.restrict (s ∩ t))
hν : Integrable f (μ.restrict (s \ t))
⊢ HAdd.hAdd (α := E) (∫ (x : X) in s ∩ t, f x ∂μ) (∫ (x : X) in s \ t, f x ∂μ) = ∫ (x : X) in s, f x ∂μ

Tactic:
rw [← Measure.restrict_inter_add_diff₀ s ht, integral_add_measure]

Premises used: MeasureTheory.integral_add_measure, MeasureTheory.Measure.restrict_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
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
⊢ Integrable f (μ.restrict (s ∩ t))

Tactic:
Integrable.mono_measure hfs (Measure.restrict_mono inter_subset_left le_rfl)

Premises used: MeasureTheory.Integrable.mono_measure, le_rfl, MeasureTheory.Measure.restrict_mono, Set.inter_subset_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 μ
hfs : IntegrableOn f s μ
⊢ Integrable f (μ.restrict (s ∩ t))

Tactic:
exact Integrable.mono_measure hfs (Measure.restrict_mono inter_subset_left le_rfl)

Premises used: MeasureTheory.Integrable.mono_measure, le_rfl, MeasureTheory.Measure.restrict_mono, Set.inter_subset_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 μ
hfs : IntegrableOn f s μ
⊢ Integrable f (μ.restrict (s \ t))

Tactic:
Integrable.mono_measure hfs (Measure.restrict_mono diff_subset le_rfl)

Premises used: MeasureTheory.Integrable.mono_measure, Set.diff_subset, le_rfl, MeasureTheory.Measure.restrict_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
ht : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
⊢ Integrable f (μ.restrict (s \ t))

Tactic:
exact Integrable.mono_measure hfs (Measure.restrict_mono diff_subset le_rfl)

Premises used: MeasureTheory.Integrable.mono_measure, Set.diff_subset, le_rfl, MeasureTheory.Measure.restrict_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
ht : MeasurableSet t
hfs : IntegrableOn f s μ
⊢ HAdd.hAdd (α := E) (∫ (x : X) in s ∩ t, f x ∂μ) (∫ (x : X) in s \ t, f x ∂μ) = ∫ (x : X) in s, f x ∂μ

Tactic:
integral_inter_add_diff₀ ht.nullMeasurableSet hfs

Premises used: MeasurableSet.nullMeasurableSet, 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
μ : Measure X
ι : Type u_5
s : ι → Set X
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:
simp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
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 : ∀ i ∈ Insert.insert a s_1, MeasurableSet (s i)
h's : (↑(Insert.insert a s_1) : Set ι).Pairwise (Disjoint on s)
hf : ∀ i ∈ Insert.insert a s_1, IntegrableOn f (s i) μ
insert :
  ∀ (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),
    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 ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X) in ⋃ i ∈ Insert.insert a s_1, s i, f x ∂μ)
    (∑ i ∈ Insert.insert a s_1, ∫ (x : X) in s i, f x ∂μ)

Tactic:
simp only [Finset.coe_insert, Finset.forall_mem_insert, Set.pairwise_insert,
      Finset.set_biUnion_insert] at hs hf h's ⊢

Premises used: Finset.forall_mem_insert, Set.pairwise_insert, Finset.coe_insert, Finset.set_biUnion_insert
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
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)
rw₁ : MeasurableSet.{u_1} (α := X) (⋃ 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 ∂μ)

Tactic:
rw [setIntegral_union _ _ hf.1 (integrableOn_finset_iUnion.2 hf.2)]

Premises used: MeasureTheory.setIntegral_union, Iff.mpr, MeasureTheory.integrableOn_finset_iUnion, 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
μ : 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 ∂μ)
insert₁ 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 ∂μ)
⊢ 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 ∂μ

Tactic:
rw [Finset.sum_insert hat, IH hs.2 h's.1 hf.2]

Premises used: And.right, And.left, Finset.sum_insert
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Set
Goal:
X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
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
simp : ∀ (i : ι) (i_1 : i ∈ s_1), Disjoint (s a) (s i)
⊢ Disjoint (s a) (⋃ i ∈ s_1, s i)

Tactic:
simp only [disjoint_iUnion_right]

Premises used: Set.disjoint_iUnion_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
μ : 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
⊢ ∀ (i : ι) (i_1 : i ∈ s_1), Disjoint (s a) (s i)

Tactic:
fun i hi => (h's.2 i hi (ne_of_mem_of_not_mem hi hat).symm).1

Premises used: Ne.symm, ne_of_mem_of_not_mem, 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
μ : 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
⊢ ∀ (i : ι) (i_1 : i ∈ s_1), Disjoint (s a) (s i)

Tactic:
exact fun i hi => (h's.2 i hi (ne_of_mem_of_not_mem hi hat).symm).1

Premises used: Ne.symm, ne_of_mem_of_not_mem, And.right, And.left