mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → β
a : α
⊢ (𝓝 (f a) ⊓ map f (𝓝[≤] a)).NeBot

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
f : α → β
a : α
⊢ MapClusterPt (leftLim f a) (𝓝[≤] a) f

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
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
⊢ ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
⊢ 𝓝[≤] a = 𝓝[<] a ⊔ pure a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
this : 𝓝[≤] a = 𝓝[<] a ⊔ pure a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
⊢ ∃ u < a, Ioo u a ⊆ {x | f x ∈ s}

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
hst : s =ᵐ[μ] t
⊢ ∫ (x : X) in s, f x ∂μ = ∫ (x : X) in t, 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
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 ∂μ = ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in t, f x ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
⊢ ContinuousWithinAt (leftLim f) (Iic a) a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
b : α
hb : b ∈ Iio a
s : Set β
s_mem : s ∈ 𝓝 (leftLim f a)
s_closed : IsClosed[inst✝³] s
⊢ ∃ u < a, Ioo u a ⊆ {x | f x ∈ s}

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 : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
hts : t ⊆ s
⊢ ∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ - ∫ (x : X) in t, f x ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
a : α
h : Tendsto f (𝓝[<] a) (𝓝 (leftLim f a))
h' : (𝓝[<] a).NeBot
⊢ leftLim (rightLim f) a = leftLim f a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : T3Space β
inst✝ : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
hα : Nonempty α
s : Set β
s_mem : s ∈ 𝓝 b
s_closed : IsClosed[inst✝⁴] s
⊢ ∃ a, ∀ (b : α), a ≤ b → MapClusterPt (g b) (𝓝 b) f ∧ f b ∈ s

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 : NullMeasurableSet t μ
hfs : IntegrableOn f s μ
⊢ ∫ (x : X) in s ∩ t, f x ∂μ + ∫ (x : X) in s \ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : T3Space β
inst✝ : NoTopOrder α
f g : α → β
b : β
h : Tendsto f atTop (𝓝 b)
h' : ∀ᶠ (x : α) in atTop, MapClusterPt (g x) (𝓝 x) f
⊢ Tendsto g atTop (𝓝 b)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : NoTopOrder α
inst✝ : T3Space β
f : α → β
b : β
h : Tendsto f atTop (𝓝 b)
⊢ Tendsto (leftLim f) atTop (𝓝 b)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : T3Space β
f : α → β
b : β
h : Tendsto f atTop (𝓝 b)
⊢ Tendsto (rightLim f) atTop (𝓝 b)

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
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun n ↦ fs n a) l (𝓝 (f a))
⊢ Tendsto (fun n ↦ setToFun μ T hT (fs n)) l (𝓝 (setToFun μ T hT f))

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
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ bound n a
bound_integrable : Integrable (fun a ↦ ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n ↦ F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
⊢ ∀ (n : ι), bound n ≤ᵐ[μ] fun a ↦ ∑' (n : ι), bound n a

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
⊢ leftLim f x ≤ f y

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
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ bound n a
bound_integrable : Integrable (fun a ↦ ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n ↦ F n a) (f a)
hb_nonneg : ∀ᵐ (a : α) ∂μ, ∀ (n : ι), 0 ≤ bound n a
hb_le_tsum : ∀ (n : ι), bound n ≤ᵐ[μ] fun a ↦ ∑' (n : ι), bound n a
⊢ ∀ (n : ι), Integrable (F n) μ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
⊢ f x ≤ leftLim f y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
⊢ Monotone (leftLim f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
⊢ rightLim f x ≤ leftLim f y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
⊢ Tendsto f (𝓝[<] x) (𝓝[≤] leftLim f x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
⊢ leftLim f x = f x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Order.LeftRightLim

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
⊢ ContinuousAt f x ↔ leftLim f x = rightLim 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 : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
inst✝ : Countable ι
F : ι → α → E
f : α → E
bound : ι → α → ℝ
hF_meas : ∀ (n : ι), AEStronglyMeasurable (F n) μ
h_bound : ∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a
bound_summable : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ bound n a
bound_integrable : Integrable (fun a ↦ ∑' (n : ι), bound n a) μ
h_lim : ∀ᵐ (a : α) ∂μ, HasSum (fun n ↦ F n a) (f a)
⊢ HasSum (fun n ↦ setToFun μ T hT (F n)) (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
a b : R
⊢ Iotop a b ⊆ Ioc a b

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : LinearOrder R
a b : R
⊢ Ioo a b ⊆ Iotop 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
inst✝ : OrderTopology R
a b : R
h : IsTop b
x : R
hx : x ∈ Ioi a
⊢ x ∈ 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
inst✝ : OrderTopology R
a b : R
⊢ IsOpen[inst✝¹] (Iotop a b)

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝ : LinearOrder R
a b : R
⊢ Ioc a b \ 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
x y : R
h : x < y
⊢ y ∉ botSet

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 g : StieltjesFunction R
h : ∀ (x : R), ↑f x = ↑g x
⊢ f = g

Tactic:
by

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

Goal state before:
pp: R : Type u_1
inst✝² : LinearOrder R
inst✝¹ : TopologicalSpace R
inst✝ : OrderTopology R
f : StieltjesFunction R
x : R
⊢ rightLim (↑f) x = ↑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
inst✝² : OrderTopology R
inst✝¹ : DenselyOrdered R
inst✝ : NoMaxOrder R
f : StieltjesFunction R
x : R
this : rightLim (↑f) x = ⨅ r, ↑f ↑r
⊢ ⨅ r, ↑f ↑r = ↑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
inst✝² : OrderTopology R
inst✝¹ : DenselyOrdered R
inst✝ : NoMaxOrder R
f : StieltjesFunction R
x : R
⊢ ⨅ r, ↑f ↑r = ↑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
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
h's : (↑t).Pairwise (Disjoint on s)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
⊢ ∫ (x : X) in ⋃ i ∈ t, s i, f x ∂μ = ∑ i ∈ t, ∫ (x : X) in s i, f x ∂μ

Tactic:
by

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

Goal state before:
pp: f : StieltjesFunction ℝ
x : ℝ
⊢ ⨅ r, ↑f ↑↑r = ↑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✝ : Fintype ι
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), IntegrableOn f (s i) μ
⊢ ∫ (x : X) in ⋃ i, s i, f x ∂μ = ∑ i, ∫ (x : X) in 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
c : ℝ
x✝¹ x✝ : R
⊢ x✝¹ ≤ x✝ → (fun x ↦ c) x✝¹ ≤ (fun x ↦ c) 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
⊢ ∫ (x : X) in ∅, f x ∂μ = 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 : ℝ
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‖ₑ ∂μ ≠ ∞
hF : CompleteSpace F
hf'' : ∀ (i : ι), AEMeasurable (fun x ↦ ‖f i x‖ₑ) μ
⊢ ∀ᵐ (a : α) ∂μ, Summable fun n ↦ ↑‖f n 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
⊢ ∫ (x : X) in univ, f x ∂μ = ∫ (x : X), 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
s : Set X
μ : Measure X
hs : ∀ᵐ (x : X) ∂μ, x ∈ s
f : X → E
⊢ ∫ (x : X), f x ∂μ = ∫ (x : X) in s, 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
s : Set X
μ : Measure X
hs : NullMeasurableSet s μ
hfi : Integrable f μ
⊢ ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in sᶜ, f x ∂μ = ∫ (x : X), 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
s : Set X
μ : Measure X
hs : NullMeasurableSet s μ
hfi : Integrable f μ
⊢ ∫ (x : X) in sᶜ, f x ∂μ = ∫ (x : X), f x ∂μ - ∫ (x : X) in s, 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
s : Set X
μ : Measure X
hs : MeasurableSet s
hfi : IntegrableOn f s μ
⊢ ∫ (x : X) in s, f x ∂μ + ∫ (x : X) in sᶜ, 0 ∂μ = ∫ (x : X) in s, 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
s : Set X
μ : Measure X
hs : MeasurableSet s
⊢ ∫ (x : X), s.indicator f x ∂μ = ∫ (x : X) in s, 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
s : Set X
μ : Measure X
hs : NullMeasurableSet s μ
⊢ ∫ (x : X), s.indicator f x ∂μ = ∫ (x : X) in s, f x ∂μ

Tactic:
by

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
E : Type u_3
mX : MeasurableSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure X
mY : MeasurableSpace Y
ν : Measure Y
f : X → Y → E
s : Set X
hs : MeasurableSet s
⊢ ∫ (x : X), ∫ (y : Y), s.indicator (fun x ↦ f x y) x ∂ν ∂μ = ∫ (x : X) in s, ∫ (y : Y), f x y ∂ν ∂μ

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 : ℝ
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‖ₑ ∂μ ≠ ∞
hF : CompleteSpace F
hf'' : ∀ (i : ι), AEMeasurable (fun x ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ ↑‖f n a‖₊
⊢ ∫⁻ (a : α), ∑' (n : ι), ‖f n 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
s t : Set X
μ : Measure X
ht : MeasurableSet t
⊢ ∫ (x : X) in s, t.indicator f x ∂μ = ∫ (x : X) in s ∩ t, 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
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
u : Finset ι
hu : u ∈ {x ∈ t.powerset | x.Nonempty}
⊢ MeasurableSet (⋂ i ∈ u, s 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
μ : Measure X
ι : Type u_5
t : Finset ι
s : ι → Set X
hs : ∀ i ∈ t, MeasurableSet (s i)
hf : ∀ i ∈ t, IntegrableOn f (s i) μ
A : ∀ u ∈ {x ∈ t.powerset | x.Nonempty}, MeasurableSet (⋂ i ∈ u, s i)
⊢ ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X) in ⋂ i ∈ x, s i, (-1) ^ (#x + 1) • f a ∂μ =
    ∑ x ∈ t.powerset with x.Nonempty, ∫ (a : X), (⋂ i ∈ x, s i).indicator (fun a ↦ (-1) ^ (#x + 1) • f a) 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 : ℝ
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‖ₑ ∂μ ≠ ∞
hF : CompleteSpace F
hf'' : ∀ (i : ι), AEMeasurable (fun x ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ ↑‖f n a‖₊
this : ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ∞
⊢ (fun a ↦ ‖∑' (n : ι), ↑‖f n a‖₊‖ₑ) =ᵐ[μ] fun a ↦ ∑' (n : ι), ‖f n a‖ₑ

Tactic:
← NNReal.coe_tsum,

Goal state after:
α : 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‖ₑ ∂μ ≠ ∞
hF : CompleteSpace F
hf'' : ∀ (i : ι), AEMeasurable (fun x ↦ ‖f i x‖ₑ) μ
hhh : ∀ᵐ (a : α) ∂μ, Summable fun n ↦ ↑‖f n a‖₊
this : ∫⁻ (a : α), ∑' (n : ι), ‖f n a‖ₑ ∂μ < ∞
⊢ (fun a ↦ ‖↑(∑' (a_1 : ι), ‖f a_1 a‖₊)‖ₑ) =ᵐ[μ] fun a ↦ ∑' (n : ι), ‖f n a‖ₑ
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
f : R → ℝ
hf : Monotone f
⊢ ∀ (x : R), ContinuousWithinAt (rightLim f) (Ici x) 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
inst✝ : OrderTopology R
f : StieltjesFunction R
⊢ {x | leftLim (↑f) x ≠ ↑f x}.Countable

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✝ : Nonempty R
s : Set R
⊢ f.length s = ⨅ a, ⨅ b, ⨅ (_ : s \ botSet ⊆ Ioc a b), ofReal (↑f b - ↑f 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✝ : IsEmpty R
s : Set R
⊢ f.length s = 0

Tactic:
by

Goal state after: