mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
inst✝¹ : CompleteSpace E
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
inst✝ : Countable ι
f : ι → α → E
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf' : ∑' (i : ι), ∫⁻ (a : α), ‖f i a‖ₑ ∂μ ≠ ∞
⊢ (setToFun μ T hT fun a ↦ ∑' (i : ι), f i a) = ∑' (i : ι), setToFun μ T hT (f i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F✝ : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F✝
inst✝² : NormedSpace ℝ F✝
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F✝
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst✝¹ : l.IsCountablyGenerated
F : ι → α → E
inst✝ : IsFiniteMeasure μ
f : α → E
h_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) μ
h_bound : ∃ C, ∀ᶠ (n : ι) in l, ∀ᵐ (ω : α) ∂μ, ‖F n ω‖ ≤ C
h_lim : ∀ᵐ (ω : α) ∂μ, Tendsto (fun n ↦ F n ω) l (𝓝 (f ω))
⊢ Tendsto (fun n ↦ setToFun μ T hT (F n)) l (𝓝 (setToFun μ T hT f))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
hR : Nonempty R
inhabited_h : Inhabited R
⊢ ⨅ (_ : ∅ \ botSet ⊆ Ioc default default), ofReal (↑f default - ↑f default) ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
inst✝¹ : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
β : Type u_7
mβ : MeasurableSpace β
inst✝ : SFinite μ
f : β → α → E
hf : StronglyMeasurable (Function.uncurry f)
⊢ MeasurableSet {x | Integrable (f x) μ}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
⊢ f.length ∅ = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
β : Type u_7
mβ : MeasurableSpace β
inst✝ : SFinite μ
hT : DominatedFinMeasAdditive μ T C
h'T : ∀ (s : Set (β × α)), MeasurableSet s → StronglyMeasurable fun x ↦ T (Prod.mk x ⁻¹' s)
f : β → α → E
hf : StronglyMeasurable (Function.uncurry f)
hF : CompleteSpace F
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range (Function.uncurry f) ∪ {0})
⊢ 0 ∈ range (Function.uncurry f) ∪ {0}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
⊢ ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ =
    ∑ u ∈ t.powerset with u.Nonempty, (-1) ^ (#u + 1) • ∫ (x : X) in ⋂ i ∈ u, s i, f x ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
a b : R
⊢ f.length (Ioc a b) = ofReal (↑f b - ↑f a)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_5
m : MeasurableSpace X
μ : Measure X
s : Set X
hs : μ s ≠ ∞
⊢ ENNReal.ofReal (∫ (x : X) in s, 1 ∂μ) = ENNReal.ofReal (∫ (x : X) in s, ‖1‖ ∂μ)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_5
m : MeasurableSpace X
μ : Measure X
s : Set X
hs : μ s ≠ ∞
⊢ ENNReal.ofReal (∫ (x : X) in s, ‖1‖ ∂μ) = ∫⁻ (x : X) in s, 1 ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_5
m : MeasurableSpace X
μ : Measure X
s : Set X
⊢ ∫ (x : X) in s, 1 ∂μ = μ.real s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
s₁ s₂ : Set R
h : s₁ ⊆ s₂
hR : Nonempty R
a b : R
⊢ s₂ \ botSet ⊆ Ioc a b → s₁ \ botSet ⊆ Ioc a b

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
s₁ s₂ : Set R
h : s₁ ⊆ s₂
⊢ f.length s₁ ≤ f.length s₂

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝¹ : LinearOrder R
inst✝ : TopologicalSpace R
f : StieltjesFunction R
s : Set R
⊢ f.length (s \ botSet) = f.length s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
mX : MeasurableSpace X
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, μ (s i) ≠ ∞
⊢ μ.real (⋃ i ∈ t, s i) = ∑ u ∈ t.powerset with u.Nonempty, (-1) ^ (#u + 1) * μ.real (⋂ i ∈ u, s i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a b : R
c d : ℕ → R
ss : Icc a b ⊆ ⋃ i, Iotop (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : R),
    Icc a b ⊆ ⋃ i ∈ ↑s, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))
⊢ Icc ?m.78 ?m.79 ⊆ ⋃ i ∈ univ, Iotop (c i) (d i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
β : Type u_7
mβ : MeasurableSpace β
inst✝ : SFinite μ
hT : DominatedFinMeasAdditive μ T C
h'T : ∀ (s : Set (β × α)), MeasurableSet s → StronglyMeasurable fun x ↦ T (Prod.mk x ⁻¹' s)
f : β → α → E
hf : StronglyMeasurable (Function.uncurry f)
hF : CompleteSpace F
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range (Function.uncurry f) ∪ {0})
s : ℕ → SimpleFunc (β × α) E := SimpleFunc.approxOn (Function.uncurry f) ⋯ (range (Function.uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → β → SimpleFunc α E := fun n x ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → β → F := fun n ↦ {x | Integrable (f x) μ}.indicator fun x ↦ SimpleFunc.setToSimpleFunc T (s' n x)
n : ℕ
⊢ ∀ (x : β), {x ∈ (s' n x).range | x ≠ 0} ⊆ (s n).range

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a b : R
c d : ℕ → R
ss : Icc a b ⊆ ⋃ i, Iotop (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : R),
    Icc a b ⊆ ⋃ i ∈ ↑s, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : s.Finite
hs : Icc a b ⊆ ⋃ i ∈ s, Iotop (c i) (d i)
⊢ ⋃ i ∈ ↑hf.toFinset, Iotop (c i) (d i) = ⋃ i ∈ s, Iotop (c i) (d i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f g : X → E
s : Set X
μ : Measure X
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : MeasurableSet s
hf : IntegrableOn f s μ
hg : IntegrableOn g sᶜ μ
⊢ ∫ (x : X), s.piecewise f g x ∂μ = ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in sᶜ, g x ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
β : Type u_7
mβ : MeasurableSpace β
inst✝ : SFinite μ
hT : DominatedFinMeasAdditive μ T C
h'T : ∀ (s : Set (β × α)), MeasurableSet s → StronglyMeasurable fun x ↦ T (Prod.mk x ⁻¹' s)
f : β → α → E
hf : StronglyMeasurable (Function.uncurry f)
hF : CompleteSpace F
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range (Function.uncurry f) ∪ {0})
s : ℕ → SimpleFunc (β × α) E := SimpleFunc.approxOn (Function.uncurry f) ⋯ (range (Function.uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → β → SimpleFunc α E := fun n x ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → β → F := fun n ↦ {x | Integrable (f x) μ}.indicator fun x ↦ SimpleFunc.setToSimpleFunc T (s' n x)
n : ℕ
⊢ StronglyMeasurable (f' n)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a b : R
c d : ℕ → R
ss : Icc a b ⊆ ⋃ i, Iotop (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : R),
    Icc a b ⊆ ⋃ i ∈ ↑s, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))
s : Set ℕ
left✝ : s ⊆ univ
hf : s.Finite
hs : Icc a b ⊆ ⋃ i ∈ s, Iotop (c i) (d i)
e : ⋃ i ∈ ↑hf.toFinset, Iotop (c i) (d i) = ⋃ i ∈ s, Iotop (c i) (d i)
⊢ Icc a b ⊆ ⋃ i ∈ ↑hf.toFinset, Iotop (c i) (d i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
β : Type u_7
mβ : MeasurableSpace β
inst✝ : SFinite μ
hT : DominatedFinMeasAdditive μ T C
h'T : ∀ (s : Set (β × α)), MeasurableSet s → StronglyMeasurable fun x ↦ T (Prod.mk x ⁻¹' s)
f : β → α → E
hf : StronglyMeasurable (Function.uncurry f)
hF : CompleteSpace F
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range (Function.uncurry f) ∪ {0})
s : ℕ → SimpleFunc (β × α) E := SimpleFunc.approxOn (Function.uncurry f) ⋯ (range (Function.uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → β → SimpleFunc α E := fun n x ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → β → F := fun n ↦ {x | Integrable (f x) μ}.indicator fun x ↦ SimpleFunc.setToSimpleFunc T (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
x : β
hfx : Integrable (f x) μ
n : ℕ
⊢ Integrable (⇑(s' n x)) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a b : R
c d : ℕ → R
ss : Icc a b ⊆ ⋃ i, Iotop (c i) (d i)
this :
  ∀ (s : Finset ℕ) (b : R),
    Icc a b ⊆ ⋃ i ∈ ↑s, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ s, ofReal (↑f (d i) - ↑f (c i))
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), ofReal (↑f (d i) - ↑f (c i))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a : R
c d : ℕ → R
s✝ s : Finset ℕ
IH :
  ∀ t ⊂ s,
    ∀ (b : R), Icc a b ⊆ ⋃ i ∈ ↑t, Iotop (c i) (d i) → ofReal (↑f b - ↑f a) ≤ ∑ i ∈ t, ofReal (↑f (d i) - ↑f (c i))
b : R
cv : Icc a b ⊆ ⋃ i ∈ ↑s, Iotop (c i) (d i)
ab : a ≤ b
⊢ ∃ i ∈ s, b ∈ Iotop (c i) (d i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
β : Type u_7
mβ : MeasurableSpace β
inst✝ : SFinite μ
hT : DominatedFinMeasAdditive μ T C
h'T : ∀ (s : Set (β × α)), MeasurableSet s → StronglyMeasurable fun x ↦ T (Prod.mk x ⁻¹' s)
f : β → α → E
hf : StronglyMeasurable (Function.uncurry f)
hF : CompleteSpace F
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : SeparableSpace ↑(range (Function.uncurry f) ∪ {0})
s : ℕ → SimpleFunc (β × α) E := SimpleFunc.approxOn (Function.uncurry f) ⋯ (range (Function.uncurry f) ∪ {0}) 0 ⋯
s' : ℕ → β → SimpleFunc α E := fun n x ↦ (s n).comp (Prod.mk x) ⋯
f' : ℕ → β → F := fun n ↦ {x | Integrable (f x) μ}.indicator fun x ↦ SimpleFunc.setToSimpleFunc T (s' n x)
hf' : ∀ (n : ℕ), StronglyMeasurable (f' n)
⊢ Tendsto f' atTop (𝓝 fun x ↦ setToFun μ T hT (f x))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
β : Type u_7
mβ : MeasurableSpace β
inst✝ : SFinite μ
hT : DominatedFinMeasAdditive μ T C
h'T : ∀ (s : Set (β × α)), MeasurableSet s → StronglyMeasurable fun x ↦ T (Prod.mk x ⁻¹' s)
f : β → α → E
hf : StronglyMeasurable (Function.uncurry f)
⊢ StronglyMeasurable fun x ↦ setToFun μ T hT (f x)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), NullMeasurableSet (s i) μ
h_mono : Monotone s
hfi : IntegrableOn f (⋃ n, s n) μ
⊢ Tendsto (fun i ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋃ n, s n, f x ∂μ))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝³ : LinearOrder R
inst✝² : TopologicalSpace R
f : StieltjesFunction R
inst✝¹ : OrderTopology R
inst✝ : CompactIccSpace R
a b : R
c d : ℕ → R
ss : Icc a b ⊆ ⋃ i, Iotop (c i) (d i)
⊢ ofReal (↑f b - ↑f a) ≤ ∑' (i : ℕ), ofReal (↑f (d i) - ↑f (c i))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
hab : b ≤ a
⊢ ofReal (↑f b - ↑f a) = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
⊢ 0 < ↑δ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
⊢ ContinuousWithinAt (fun r ↦ ↑f r - ↑f a) (Ioi a) a

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
A : ContinuousWithinAt (fun r ↦ ↑f r - ↑f a) (Ioi a) a
⊢ ↑f a - ↑f a < ↑δ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.SetToL1

Goal state before:
pp: α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst✝¹ : TopologicalSpace X
inst✝ : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x ↦ fs x a) s
⊢ ContinuousOn (fun x ↦ setToFun μ T hT (fs x)) s

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
⊢ ∃ a', ↑f a' - ↑f a < ↑δ ∧ a < a'

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this✝ : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
this :
  Tendsto (fun x ↦ ∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in s i₀ \ s x, f x ∂μ) atTop
    (𝓝 (∫ (x : X) in s i₀, f x ∂μ - ∫ (x : X) in ⋃ i, s i₀ \ s i, f x ∂μ))
⊢ Tendsto (fun i ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋂ n, s n, f x ∂μ))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
⊢ ∀ (K₁ K₂ : Compacts G), ↑K₁ ⊆ ↑K₂ → 0 ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
⊢ ∀ (K₁ K₂ : Compacts G), Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → 0 = 0 + 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
⊢ ∀ (K₁ K₂ : Compacts G), 0 ≤ 0 + 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
⊢ Function.Injective fun μ s ↦ ↑(μ.toFun s)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K₁ K₂ : Compacts G
h : ↑K₁ ⊆ ↑K₂
⊢ μ K₁ ≤ μ K₂

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K₁ K₂ : Compacts G
h : Disjoint ↑K₁ ↑K₂
h₁ : IsClosed ↑K₁
h₂ : IsClosed ↑K₂
⊢ μ (K₁ ⊔ K₂) = μ K₁ + μ K₂

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K₁ K₂ : Compacts G
⊢ μ (K₁ ⊔ K₂) ≤ μ K₁ + μ K₂

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
μ : Content G
⊢ μ ⊥ = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hne : atTop.NeBot
this : IsDirectedOrder ι
i₀ : ι
hi₀ : IntegrableOn f (s i₀) μ
⊢ ∀ (i : ι), MeasurableSet (s i₀ \ s i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
μ : Content G
K : Compacts G
hK : ↑K ⊆ ↑⊥
⊢ K = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
μ : Content G
⊢ μ.innerContent ⊥ = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝¹ : Preorder ι
inst✝ : atTop.IsCountablyGenerated
s : ι → Set X
hsm : ∀ (i : ι), MeasurableSet (s i)
h_anti : Antitone s
hfi : ∃ i, IntegrableOn f (s i) μ
⊢ Tendsto (fun i ↦ ∫ (x : X) in s i, f x ∂μ) atTop (𝓝 (∫ (x : X) in ⋂ n, s n, f x ∂μ))

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : X → E
μ : Measure X
ι : Type u_5
inst✝ : Countable ι
s : ι → Set X
hm : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
hfi : IntegrableOn f (⋃ i, s i) μ
⊢ HasSum (fun n ↦ ∫ (x : X) in s n, f x ∂μ) (∫ (x : X) in ⋃ n, s n, f x ∂μ)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝ : TopologicalSpace G
μ : Content G
U : Opens G
hU : μ.innerContent U ≠ ∞
ε : ℝ≥0
hε : ε ≠ 0
⊢ ∃ K, ↑K ⊆ ↑U ∧ μ.innerContent U ≤ μ K + ↑ε

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
⊢ ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
hf : AEStronglyMeasurable f (μ.restrict t)
⊢ ∫ (x : X) in t, AEStronglyMeasurable.mk f hf x ∂μ = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Content

Goal state before:
pp: G : Type w
inst✝¹ : TopologicalSpace G
μ : Content G
inst✝ : R1Space G
U : ℕ → Opens G
h3 : ∀ (t : Finset ℕ) (K : ℕ → Compacts G), μ (t.sup K) ≤ ∑ i ∈ t, μ (K i)
K : Compacts G
hK : ↑K ⊆ ↑(⨆ i, U i)
⊢ ↑K ⊆ ⋃ i, ↑(U i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Measure.Stieltjes

Goal state before:
pp: R : Type u_1
inst✝⁴ : LinearOrder R
inst✝³ : TopologicalSpace R
f : StieltjesFunction R
inst✝² : OrderTopology R
inst✝¹ : CompactIccSpace R
inst✝ : DenselyOrdered R
a b : R
hab : a < b
s : ℕ → Set R
hs : Ioc a b ⊆ ⋃ i, s i
ε : ℝ≥0
εpos : 0 < ε
h : ∑' (i : ℕ), f.length (s i) < ∞
δ : ℝ≥0 := ε / 2
δpos : 0 < ↑δ
ε' : ℕ → ℝ≥0
ε'0 : ∀ (i : ℕ), 0 < ε' i
hε : ∑' (i : ℕ), ↑(ε' i) < ↑δ
a' : R
ha' : ↑f a' - ↑f a < ↑δ
aa' : a < a'
this : Nonempty R
i : ℕ
p q' : R
spq : s i \ botSet ⊆ Ioc p q'
hq' : ofReal (↑f q' - ↑f p) < f.length (s i) + ↑(ε' i)
⊢ Icc a' b ∩ s i ⊆ Ioc p q'

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
ht_eq : ∀ᵐ (x : X) ∂μ, x ∈ t → f x = 0
⊢ ∫ (x : X) in t, f x ∂μ = 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → E
t : Set X
μ : Measure X
hU : ∫ (x : X) in t, f x ∂μ ≠ 0
⊢ ∃ x ∈ t, f x ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.Bochner.Set

Goal state before:
pp: X : Type u_1
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : 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:
by

Goal state after: