mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
h'α : Nonempty α
m : AddContent E {s | ∃ u v, u ≤ v ∧ s = Ioc u v} := AddContent.onIoc (Function.rightLim f)
A : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, ‖m s‖ₑ ≤ hf.measureAux s
B : hα = generateFrom {s | ∃ u v, u ≤ v ∧ s = Ioc u v}
m' : VectorMeasure α E
hm' : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, m' s = m s
h'm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ hf.measureAux s
u v : α
huv : u ≤ v
⊢ m' (Ioc u v) = Function.rightLim f v - Function.rightLim f u

pp: case inr.refine_2
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
h'α : Nonempty α
m : AddContent E {s | ∃ u v, u ≤ v ∧ s = Ioc u v} := AddContent.onIoc (Function.rightLim f)
A : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, ‖m s‖ₑ ≤ hf.measureAux s
B : hα = generateFrom {s | ∃ u v, u ≤ v ∧ s = Ioc u v}
m' : VectorMeasure α E
hm' : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, m' s = m s
h'm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ hf.measureAux s
⊢ m' botSet = 0

Tactic:
·

Goal state after:
case inr.refine_1
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
h'α : Nonempty α
m : AddContent E {s | ∃ u v, u ≤ v ∧ s = Ioc u v} := AddContent.onIoc (Function.rightLim f)
A : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, ‖m s‖ₑ ≤ hf.measureAux s
B : hα = generateFrom {s | ∃ u v, u ≤ v ∧ s = Ioc u v}
m' : VectorMeasure α E
hm' : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, m' s = m s
h'm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ hf.measureAux s
u v : α
huv : u ≤ v
⊢ m' (Ioc u v) = Function.rightLim f v - Function.rightLim f u
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case insert.hfs
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
s : ι → Set X
a✝ : ι
s✝ : Finset ι
hat : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, MeasurableSet (s i)) →
    (↑s✝).Pairwise (Disjoint on s) →
      (∀ i ∈ s✝, μ.IntegrableOn f (s i)) →
        ∫ᵛ (x : X) in ⋃ i ∈ s✝, s i, f x ∂[B; μ] = ∑ i ∈ s✝, ∫ᵛ (x : X) in s i, f x ∂[B; μ]
hs : MeasurableSet (s a✝) ∧ ∀ x ∈ s✝, MeasurableSet (s x)
hf : μ.IntegrableOn f (s a✝) ∧ ∀ x ∈ s✝, μ.IntegrableOn f (s x)
h's : (↑s✝).Pairwise (Disjoint on s) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Disjoint on s) a✝ b ∧ (Disjoint on s) b a✝
⊢ μ.IntegrableOn f (s a✝)

pp: case insert.hft
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
s : ι → Set X
a✝ : ι
s✝ : Finset ι
hat : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, MeasurableSet (s i)) →
    (↑s✝).Pairwise (Disjoint on s) →
      (∀ i ∈ s✝, μ.IntegrableOn f (s i)) →
        ∫ᵛ (x : X) in ⋃ i ∈ s✝, s i, f x ∂[B; μ] = ∑ i ∈ s✝, ∫ᵛ (x : X) in s i, f x ∂[B; μ]
hs : MeasurableSet (s a✝) ∧ ∀ x ∈ s✝, MeasurableSet (s x)
hf : μ.IntegrableOn f (s a✝) ∧ ∀ x ∈ s✝, μ.IntegrableOn f (s x)
h's : (↑s✝).Pairwise (Disjoint on s) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Disjoint on s) a✝ b ∧ (Disjoint on s) b a✝
⊢ μ.IntegrableOn f (⋃ x ∈ s✝, s x)

Tactic:
·

Goal state after:
case insert.hfs
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
s : ι → Set X
a✝ : ι
s✝ : Finset ι
hat : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, MeasurableSet (s i)) →
    (↑s✝).Pairwise (Disjoint on s) →
      (∀ i ∈ s✝, μ.IntegrableOn f (s i)) →
        ∫ᵛ (x : X) in ⋃ i ∈ s✝, s i, f x ∂[B; μ] = ∑ i ∈ s✝, ∫ᵛ (x : X) in s i, f x ∂[B; μ]
hs : MeasurableSet (s a✝) ∧ ∀ x ∈ s✝, MeasurableSet (s x)
hf : μ.IntegrableOn f (s a✝) ∧ ∀ x ∈ s✝, μ.IntegrableOn f (s x)
h's : (↑s✝).Pairwise (Disjoint on s) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Disjoint on s) a✝ b ∧ (Disjoint on s) b a✝
⊢ μ.IntegrableOn f (s a✝)
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
h'α : Nonempty α
m : AddContent E {s | ∃ u v, u ≤ v ∧ s = Ioc u v} := AddContent.onIoc (Function.rightLim f)
A : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, ‖m s‖ₑ ≤ hf.measureAux s
B : hα = generateFrom {s | ∃ u v, u ≤ v ∧ s = Ioc u v}
m' : VectorMeasure α E
hm' : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, m' s = m s
h'm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ hf.measureAux s
u v : α
huv : u ≤ v
⊢ m (Ioc u v) = Function.rightLim f v - Function.rightLim f u

pp: case inr.refine_1.a
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
h'α : Nonempty α
m : AddContent E {s | ∃ u v, u ≤ v ∧ s = Ioc u v} := AddContent.onIoc (Function.rightLim f)
A : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, ‖m s‖ₑ ≤ hf.measureAux s
B : hα = generateFrom {s | ∃ u v, u ≤ v ∧ s = Ioc u v}
m' : VectorMeasure α E
hm' : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, m' s = m s
h'm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ hf.measureAux s
u v : α
huv : u ≤ v
⊢ Ioc u v ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}

Tactic:
·

Goal state after:
case inr.refine_1
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
h'α : Nonempty α
m : AddContent E {s | ∃ u v, u ≤ v ∧ s = Ioc u v} := AddContent.onIoc (Function.rightLim f)
A : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, ‖m s‖ₑ ≤ hf.measureAux s
B : hα = generateFrom {s | ∃ u v, u ≤ v ∧ s = Ioc u v}
m' : VectorMeasure α E
hm' : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, m' s = m s
h'm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ hf.measureAux s
u v : α
huv : u ≤ v
⊢ m (Ioc u v) = Function.rightLim f v - Function.rightLim f u
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case insert.hft
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
s : ι → Set X
a✝ : ι
s✝ : Finset ι
hat : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, MeasurableSet (s i)) →
    (↑s✝).Pairwise (Disjoint on s) →
      (∀ i ∈ s✝, μ.IntegrableOn f (s i)) →
        ∫ᵛ (x : X) in ⋃ i ∈ s✝, s i, f x ∂[B; μ] = ∑ i ∈ s✝, ∫ᵛ (x : X) in s i, f x ∂[B; μ]
hs : MeasurableSet (s a✝) ∧ ∀ x ∈ s✝, MeasurableSet (s x)
hf : μ.IntegrableOn f (s a✝) ∧ ∀ x ∈ s✝, μ.IntegrableOn f (s x)
h's : (↑s✝).Pairwise (Disjoint on s) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Disjoint on s) a✝ b ∧ (Disjoint on s) b a✝
⊢ μ.IntegrableOn f (⋃ x ∈ s✝, s x)

Tactic:
·

Goal state after:
case insert.hft
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
s : ι → Set X
a✝ : ι
s✝ : Finset ι
hat : a✝ ∉ s✝
IH :
  (∀ i ∈ s✝, MeasurableSet (s i)) →
    (↑s✝).Pairwise (Disjoint on s) →
      (∀ i ∈ s✝, μ.IntegrableOn f (s i)) →
        ∫ᵛ (x : X) in ⋃ i ∈ s✝, s i, f x ∂[B; μ] = ∑ i ∈ s✝, ∫ᵛ (x : X) in s i, f x ∂[B; μ]
hs : MeasurableSet (s a✝) ∧ ∀ x ∈ s✝, MeasurableSet (s x)
hf : μ.IntegrableOn f (s a✝) ∧ ∀ x ∈ s✝, μ.IntegrableOn f (s x)
h's : (↑s✝).Pairwise (Disjoint on s) ∧ ∀ b ∈ ↑s✝, a✝ ≠ b → (Disjoint on s) a✝ b ∧ (Disjoint on s) b a✝
⊢ μ.IntegrableOn f (⋃ x ∈ s✝, s x)
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: case inr.refine_1.a
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
h'α : Nonempty α
m : AddContent E {s | ∃ u v, u ≤ v ∧ s = Ioc u v} := AddContent.onIoc (Function.rightLim f)
A : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, ‖m s‖ₑ ≤ hf.measureAux s
B : hα = generateFrom {s | ∃ u v, u ≤ v ∧ s = Ioc u v}
m' : VectorMeasure α E
hm' : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, m' s = m s
h'm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ hf.measureAux s
u v : α
huv : u ≤ v
⊢ Ioc u v ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}

Tactic:
·

Goal state after:
case inr.refine_1.a
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
h'α : Nonempty α
m : AddContent E {s | ∃ u v, u ≤ v ∧ s = Ioc u v} := AddContent.onIoc (Function.rightLim f)
A : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, ‖m s‖ₑ ≤ hf.measureAux s
B : hα = generateFrom {s | ∃ u v, u ≤ v ∧ s = Ioc u v}
m' : VectorMeasure α E
hm' : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, m' s = m s
h'm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ hf.measureAux s
u v : α
huv : u ≤ v
⊢ Ioc u v ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case e'_2.e'_12
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
inst✝ : Fintype ι
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), μ.IntegrableOn f (s i)
x✝ : ι
⊢ s x✝ = ⋃ (_ : x✝ ∈ Finset.univ), s x✝

pp: case convert_5
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
inst✝ : Fintype ι
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), μ.IntegrableOn f (s i)
⊢ (↑Finset.univ).Pairwise (Disjoint on s)

Tactic:
·

Goal state after:
case e'_2.e'_12
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
inst✝ : Fintype ι
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), μ.IntegrableOn f (s i)
x✝ : ι
⊢ s x✝ = ⋃ (_ : x✝ ∈ Finset.univ), s x✝
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case convert_5
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
inst✝ : Fintype ι
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), μ.IntegrableOn f (s i)
⊢ (↑Finset.univ).Pairwise (Disjoint on s)

Tactic:
·

Goal state after:
case convert_5
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
ι : Type u_7
inst✝ : Fintype ι
s : ι → Set X
hs : ∀ (i : ι), MeasurableSet (s i)
h's : Pairwise (Disjoint on s)
hf : ∀ (i : ι), μ.IntegrableOn f (s i)
⊢ (↑Finset.univ).Pairwise (Disjoint on s)
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: case inr.refine_2
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
h'α : Nonempty α
m : AddContent E {s | ∃ u v, u ≤ v ∧ s = Ioc u v} := AddContent.onIoc (Function.rightLim f)
A : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, ‖m s‖ₑ ≤ hf.measureAux s
B : hα = generateFrom {s | ∃ u v, u ≤ v ∧ s = Ioc u v}
m' : VectorMeasure α E
hm' : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, m' s = m s
h'm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ hf.measureAux s
⊢ m' botSet = 0

Tactic:
·

Goal state after:
case inr.refine_2
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
hf : BoundedVariationOn f univ
h'α : Nonempty α
m : AddContent E {s | ∃ u v, u ≤ v ∧ s = Ioc u v} := AddContent.onIoc (Function.rightLim f)
A : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, ‖m s‖ₑ ≤ hf.measureAux s
B : hα = generateFrom {s | ∃ u v, u ≤ v ∧ s = Ioc u v}
m' : VectorMeasure α E
hm' : ∀ s ∈ {s | ∃ u v, u ≤ v ∧ s = Ioc u v}, m' s = m s
h'm' : ∀ (s : Set α), ‖m' s‖ₑ ≤ hf.measureAux s
⊢ m' botSet = 0
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: case h₁
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := ⋯
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := ⋯
s t : ↑C'
this : edist s t = edist ↑s ↑t
Is : ↑↑s ∩ ↑↑t ∪ ↑↑s \ ↑↑t = ↑↑s
It : ↑↑t ∩ ↑↑s ∪ ↑↑t \ ↑↑s = ↑↑t
⊢ ‖m (↑↑s \ ↑↑t)‖ₑ ≤ μ (↑↑s \ ↑↑t)

pp: case h₂
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := ⋯
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := ⋯
s t : ↑C'
this : edist s t = edist ↑s ↑t
Is : ↑↑s ∩ ↑↑t ∪ ↑↑s \ ↑↑t = ↑↑s
It : ↑↑t ∩ ↑↑s ∪ ↑↑t \ ↑↑s = ↑↑t
⊢ ‖m (↑↑t \ ↑↑s)‖ₑ ≤ μ (↑↑t \ ↑↑s)

Tactic:
·

Goal state after:
case h₁
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := ⋯
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := ⋯
s t : ↑C'
this : edist s t = edist ↑s ↑t
Is : ↑↑s ∩ ↑↑t ∪ ↑↑s \ ↑↑t = ↑↑s
It : ↑↑t ∩ ↑↑s ∪ ↑↑t \ ↑↑s = ↑↑t
⊢ ‖m (↑↑s \ ↑↑t)‖ₑ ≤ μ (↑↑s \ ↑↑t)
Module: Mathlib.MeasureTheory.VectorMeasure.AddContent

Goal state before:
pp: case h₂
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := ⋯
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := ⋯
s t : ↑C'
this : edist s t = edist ↑s ↑t
Is : ↑↑s ∩ ↑↑t ∪ ↑↑s \ ↑↑t = ↑↑s
It : ↑↑t ∩ ↑↑s ∪ ↑↑t \ ↑↑s = ↑↑t
⊢ ‖m (↑↑t \ ↑↑s)‖ₑ ≤ μ (↑↑t \ ↑↑s)

Tactic:
·

Goal state after:
case h₂
α : Type u_1
hα : MeasurableSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
C : Set (Set α)
m : AddContent E C
hC : IsSetRing C
hCmeas : ∀ s ∈ C, MeasurableSet s
hm : ∀ s ∈ C, ‖m s‖ₑ ≤ μ s
h'C : ∀ (t : Set α) (ε : ℝ≥0∞), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (s ∆ t) < ε
C' : Set (MeasuredSets μ) := ⋯
C'C : ∀ s ∈ C', ↑s ∈ C
C'_dense : Dense C'
m₀ : ↑C' → E := ⋯
s t : ↑C'
this : edist s t = edist ↑s ↑t
Is : ↑↑s ∩ ↑↑t ∪ ↑↑s \ ↑↑t = ↑↑s
It : ↑↑t ∩ ↑↑s ∪ ↑↑t \ ↑↑s = ↑↑t
⊢ ‖m (↑↑t \ ↑↑s)‖ₑ ≤ μ (↑↑t \ ↑↑s)
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
hfi : μ.Integrable f
⊢ ∫ᵛ (x : X) in sᶜ, f x ∂[B; μ] =
    ∫ᵛ (x : X) in s, f x ∂[B; μ] + ∫ᵛ (x : X) in sᶜ, f x ∂[B; μ] - ∫ᵛ (x : X) in s, f x ∂[B; μ]

Tactic:
add_sub_cancel_left

Goal state after:
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
hfi : μ.Integrable f
⊢ ∫ᵛ (x : X) in sᶜ, f x ∂[B; μ] = ∫ᵛ (x : X) in sᶜ, f x ∂[B; μ]
Module: Mathlib.MeasureTheory.VectorMeasure.SetIntegral

Goal state before:
pp: case neg
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
hfi : ¬μ.IntegrableOn f s
⊢ ∫ᵛ (x : X), s.indicator f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]

pp: case pos
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
hfi : μ.IntegrableOn f s
⊢ ∫ᵛ (x : X), s.indicator f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]

Tactic:
·

Goal state after:
case neg
X : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
mX : MeasurableSpace X
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedAddCommGroup G
μ : VectorMeasure X F
f : X → E
s : Set X
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace ℝ G
B : E →L[ℝ] F →L[ℝ] G
hs : MeasurableSet s
hfi : ¬μ.IntegrableOn f s
⊢ ∫ᵛ (x : X), s.indicator f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: case pos
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
h : a ≤ b
A : ⋯.choose (Ioc a b) = Function.rightLim f b - Function.rightLim f a
hx : ∃ x, IsBot x
⊢ (if hx : ∃ x, IsBot x then VectorMeasure.dirac hx.choose (Function.rightLim f hx.choose - f hx.choose) else 0)
      (Ioc a b) =
    0

pp: case neg
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
h : a ≤ b
A : ⋯.choose (Ioc a b) = Function.rightLim f b - Function.rightLim f a
hx : ¬∃ x, IsBot x
⊢ (if hx : ∃ x, IsBot x then VectorMeasure.dirac hx.choose (Function.rightLim f hx.choose - f hx.choose) else 0)
      (Ioc a b) =
    0

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
h : a ≤ b
A : ⋯.choose (Ioc a b) = Function.rightLim f b - Function.rightLim f a
hx : ∃ x, IsBot x
⊢ (if hx : ∃ x, IsBot x then VectorMeasure.dirac hx.choose (Function.rightLim f hx.choose - f hx.choose) else 0)
      (Ioc a b) =
    0
Module: Mathlib.MeasureTheory.VectorMeasure.BoundedVariation

Goal state before:
pp: case neg
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
h : a ≤ b
A : ⋯.choose (Ioc a b) = Function.rightLim f b - Function.rightLim f a
hx : ¬∃ x, IsBot x
⊢ (if hx : ∃ x, IsBot x then VectorMeasure.dirac hx.choose (Function.rightLim f hx.choose - f hx.choose) else 0)
      (Ioc a b) =
    0

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝⁸ : LinearOrder α
inst✝⁷ : DenselyOrdered α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : SecondCountableTopology α
inst✝³ : CompactIccSpace α
hα : MeasurableSpace α
inst✝² : BorelSpace α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : CompleteSpace E
f : α → E
a b : α
hf : BoundedVariationOn f univ
h : a ≤ b
A : ⋯.choose (Ioc a b) = Function.rightLim f b - Function.rightLim f a
hx : ¬∃ x, IsBot x
⊢ (if hx : ∃ x, IsBot x then VectorMeasure.dirac hx.choose (Function.rightLim f hx.choose - f hx.choose) else 0)
      (Ioc a b) =
    0