awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
s : Set X
hs : (↑μ.ennrealVariation : Set X → ℝ≥0∞) s = 0
hsm : MeasurableSet s
pos : LE.le (α := ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
pos₁ : (↑μ.ennrealVariation : Set X → ℝ≥0∞) s ≤ 0
pos₂ pos₃ : LE.le (α := ℝ≥0∞) 0 0
⊢ ‖(↑μ : Set X → V) s‖ₑ ≤ 0

Tactic:
grw [enorm_measure_le_variation, ← ennrealVariation_apply _ hsm, hs]

Premises used: MeasureTheory.VectorMeasure.enorm_measure_le_variation, MeasureTheory.VectorMeasure.ennrealVariation_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
s : Set X
hs : (↑μ.ennrealVariation : Set X → ℝ≥0∞) s = 0
hsm : ¬MeasurableSet s
⊢ (↑μ : Set X → V) s = 0

Tactic:
μ.not_measurable' hsm

Premises used: MeasureTheory.VectorMeasure.not_measurable'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
s : Set X
hs : (↑μ.ennrealVariation : Set X → ℝ≥0∞) s = 0
hsm : ¬MeasurableSet s
⊢ (↑μ : Set X → V) s = 0

Tactic:
exact μ.not_measurable' hsm

Premises used: MeasureTheory.VectorMeasure.not_measurable'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
m : Measure X
h : ∀ (E : Set X), MeasurableSet E → ‖(↑μ : Set X → V) E‖ₑ ≤ (m : (a : Set X) → ℝ≥0∞) E
⊢ μ.variation ≤ m

Tactic:
Measure.le_intro fun s hs _ => ?_

Premises used: MeasureTheory.Measure.le_intro
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
m : Measure X
h : ∀ (E : Set X), MeasurableSet E → ‖(↑μ : Set X → V) E‖ₑ ≤ (m : (a : Set X) → ℝ≥0∞) E
refine :
  ∀ (s : Set X) (hs : MeasurableSet s),
    s.Nonempty → LE.le (α := ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ.variation ≤ m

Tactic:
refine Measure.le_intro fun s hs _ => ?_

Premises used: MeasureTheory.Measure.le_intro
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
m : Measure X
h : ∀ (E : Set X), MeasurableSet E → ‖(↑μ : Set X → V) E‖ₑ ≤ (m : (a : Set X) → ℝ≥0∞) E
s : Set X
hs : MeasurableSet s
h_1 : s.Nonempty
simp :
  ∀ (i : Finpartition (Subtype.mk (p := MeasurableSet) s ⋯)),
    LE.le (α := ℝ≥0∞) (∑ x ∈ i.parts, ‖(↑μ : Set X → V) (↑x : Set X)‖ₑ : ℝ≥0∞) ((m : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [variation_apply, preVariation, ennrealToMeasure_apply hs, ennrealPreVariation_apply,
    preVariationFun, hs, dite_true, iSup_le_iff]

Premises used: MeasureTheory.VectorMeasure.ennrealToMeasure_apply, MeasureTheory.preVariationFun, MeasureTheory.preVariation, iSup_le_iff, dite_true, MeasureTheory.ennrealPreVariation_apply, MeasureTheory.VectorMeasure.variation_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
m : Measure X
h : ∀ (E : Set X), MeasurableSet E → ‖(↑μ : Set X → V) E‖ₑ ≤ (m : (a : Set X) → ℝ≥0∞) E
s : Set X
hs : MeasurableSet s
h_1 : s.Nonempty
i : Finpartition (Subtype.mk (p := MeasurableSet) s ⋯)
⊢ LE.le (α := ℝ≥0∞) (∑ x ∈ i.parts, ‖(↑μ : Set X → V) (↑x : Set X)‖ₑ)
    (∑ x ∈ i.parts, (m : (a : Set X) → ℝ≥0∞) (↑x : Set X))

Tactic:
Finset.sum_le_sum (fun s hs => h s s.property)

Premises used: Finset.sum_le_sum, Subtype.val, Subtype.property
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
m : Measure X
h : ∀ (E : Set X), MeasurableSet E → ‖(↑μ : Set X → V) E‖ₑ ≤ (m : (a : Set X) → ℝ≥0∞) E
s : Set X
hs : MeasurableSet s
h_1 : s.Nonempty
i : Finpartition (Subtype.mk (p := MeasurableSet) s ⋯)
rw :
  Eq (α := ℝ≥0∞) (∑ x ∈ i.parts, (m : (a : Set X) → ℝ≥0∞) (↑x : Set X) : ℝ≥0∞)
    ((m : (a : Set X) → ℝ≥0∞) (⋃ x ∈ i.parts, (↑x : Set X)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑ x ∈ i.parts, (m : (a : Set X) → ℝ≥0∞) (↑x : Set X) : ℝ≥0∞)
    ((m : (a : Set X) → ℝ≥0∞) (i.parts.sup (Subtype.val (p := MeasurableSet))) : ℝ≥0∞)

Tactic:
rw [sup_set_eq_biUnion]

Premises used: Finset.sup_set_eq_biUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
m : Measure X
h : ∀ (E : Set X), MeasurableSet E → ‖(↑μ : Set X → V) E‖ₑ ≤ (m : (a : Set X) → ℝ≥0∞) E
s : Set X
hs : MeasurableSet s
h_1 : s.Nonempty
i : Finpartition (Subtype.mk (p := MeasurableSet) s ⋯)
⊢ Eq (α := ℝ≥0∞) (∑ x ∈ i.parts, (m : (a : Set X) → ℝ≥0∞) (↑x : Set X) : ℝ≥0∞)
    ((m : (a : Set X) → ℝ≥0∞) (⋃ x ∈ i.parts, (↑x : Set X)) : ℝ≥0∞)

Tactic:
(MeasureTheory.measure_biUnion_finset ?_ fun b _ => b.property).symm

Premises used: MeasureTheory.measure_biUnion_finset, Eq.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
m : Measure X
h : ∀ (E : Set X), MeasurableSet E → ‖(↑μ : Set X → V) E‖ₑ ≤ (m : (a : Set X) → ℝ≥0∞) E
s : Set X
hs : MeasurableSet s
h_1 : s.Nonempty
i : Finpartition (Subtype.mk (p := MeasurableSet) s ⋯)
refine : (↑i.parts : Set (Subtype MeasurableSet)).PairwiseDisjoint (Subtype.val (p := MeasurableSet))
⊢ Eq (α := ℝ≥0∞) (∑ x ∈ i.parts, (m : (a : Set X) → ℝ≥0∞) (↑x : Set X) : ℝ≥0∞)
    ((m : (a : Set X) → ℝ≥0∞) (⋃ x ∈ i.parts, (↑x : Set X)) : ℝ≥0∞)

Tactic:
refine (MeasureTheory.measure_biUnion_finset ?_ fun b _ => b.property).symm

Premises used: MeasureTheory.measure_biUnion_finset, Eq.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
m : Measure X
h : ∀ (E : Set X), MeasurableSet E → ‖(↑μ : Set X → V) E‖ₑ ≤ (m : (a : Set X) → ℝ≥0∞) E
s : Set X
hs : MeasurableSet s
h_1 : s.Nonempty
i : Finpartition (Subtype.mk (p := MeasurableSet) s ⋯)
a : Subtype (α := Set X) MeasurableSet
ha : a ∈ (↑i.parts : Set (Subtype MeasurableSet))
b : Subtype (α := Set X) MeasurableSet
hb : b ∈ (↑i.parts : Set (Subtype MeasurableSet))
hab : a ≠ b
⊢ Function.onFun Disjoint (Subtype.val (p := MeasurableSet)) a b

Tactic:
simpa [disjoint_iff, Subtype.ext_iff] using i.disjoint ha hb hab

Premises used: Finpartition.disjoint, disjoint_iff, Subtype.ext_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
m : Measure X
h : ∀ (E : Set X), MeasurableSet E → ‖(↑μ : Set X → V) E‖ₑ ≤ (m : (a : Set X) → ℝ≥0∞) E
s : Set X
hs : MeasurableSet s
h_1 : s.Nonempty
i : Finpartition (Subtype.mk (p := MeasurableSet) s ⋯)
rw :
  LE.le (α := ℝ≥0∞) ((m : (a : Set X) → ℝ≥0∞) (⋃ x ∈ i.parts, (↑x : Set X)) : ℝ≥0∞) ((m : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set X) → ℝ≥0∞) (i.parts.sup (Subtype.val (p := MeasurableSet))) : ℝ≥0∞)
    ((m : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [sup_set_eq_biUnion]

Premises used: Finset.sup_set_eq_biUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
m : Measure X
h : ∀ (E : Set X), MeasurableSet E → ‖(↑μ : Set X → V) E‖ₑ ≤ (m : (a : Set X) → ℝ≥0∞) E
s : Set X
hs : MeasurableSet s
h_1 : s.Nonempty
i : Finpartition (Subtype.mk (p := MeasurableSet) s ⋯)
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set X) → ℝ≥0∞) (⋃ x ∈ i.parts, (↑x : Set X)) : ℝ≥0∞) ((m : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
measure_mono <| Set.iUnion₂_subset fun _ hp => Subtype.coe_le_coe.mpr (i.le hp)

Premises used: Iff.mpr, Set.iUnion₂_subset, Subtype.coe_le_coe, MeasureTheory.measure_mono, Finpartition.le
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
m : Measure X
h : ∀ (E : Set X), MeasurableSet E → ‖(↑μ : Set X → V) E‖ₑ ≤ (m : (a : Set X) → ℝ≥0∞) E
s : Set X
hs : MeasurableSet s
h_1 : s.Nonempty
i : Finpartition (Subtype.mk (p := MeasurableSet) s ⋯)
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set X) → ℝ≥0∞) (⋃ x ∈ i.parts, (↑x : Set X)) : ℝ≥0∞) ((m : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact measure_mono <| Set.iUnion₂_subset fun _ hp => Subtype.coe_le_coe.mpr (i.le hp)

Premises used: Iff.mpr, Set.iUnion₂_subset, Subtype.coe_le_coe, MeasureTheory.measure_mono, Finpartition.le
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ : VectorMeasure X V
m : Measure X
h : ∀ (E : Set X), MeasurableSet E → ‖(↑μ : Set X → V) E‖ₑ ≤ (m : (a : Set X) → ℝ≥0∞) E
s : Set X
hs : MeasurableSet s
h_1 : s.Nonempty
i : Finpartition (Subtype.mk (p := MeasurableSet) s ⋯)
x :
  Eq (α := ℝ≥0∞) (∑ x ∈ i.parts, (m : (a : Set X) → ℝ≥0∞) (↑x : Set X) : ℝ≥0∞)
    ((m : (a : Set X) → ℝ≥0∞) (i.parts.sup (Subtype.val (p := MeasurableSet))) : ℝ≥0∞)
x₁ :
  LE.le (α := ℝ≥0∞) ((m : (a : Set X) → ℝ≥0∞) (i.parts.sup (Subtype.val (p := MeasurableSet))) : ℝ≥0∞)
    ((m : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑ x ∈ i.parts, ‖(↑μ : Set X → V) (↑x : Set X)‖ₑ : ℝ≥0∞) ((m : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
calc
    ∑ x ∈ i.parts, ‖μ x‖ₑ ≤ ∑ x ∈ i.parts, m x := Finset.sum_le_sum (fun s hs => h s s.property)
    _ = m (i.parts.sup Subtype.val) := by
      rw [sup_set_eq_biUnion]
      refine (MeasureTheory.measure_biUnion_finset ?_ fun b _ => b.property).symm
      intro a ha b hb hab
      simpa [disjoint_iff, Subtype.ext_iff] using i.disjoint ha hb hab
    _ ≤ m s := by
      rw [sup_set_eq_biUnion]
      exact measure_mono <| Set.iUnion₂_subset fun _ hp => Subtype.coe_le_coe.mpr (i.le hp)

Premises used: Finpartition.parts, Finset.sup, Subtype.val, DFunLike.coe
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ ν : VectorMeasure X V
inst_3 : ContinuousAdd V
⊢ (μ + ν).variation ≤ μ.variation + ν.variation

Tactic:
variation_le_of_forall_enorm_le fun E _ => ?_

Premises used: MeasureTheory.VectorMeasure.variation_le_of_forall_enorm_le
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ ν : VectorMeasure X V
inst_3 : ContinuousAdd V
refine :
  ∀ (E : Set X), MeasurableSet E → ‖(↑(μ + ν) : Set X → V) E‖ₑ ≤ (μ.variation + ν.variation : (a : Set X) → ℝ≥0∞) E
⊢ (μ + ν).variation ≤ μ.variation + ν.variation

Tactic:
refine variation_le_of_forall_enorm_le fun E _ => ?_

Premises used: MeasureTheory.VectorMeasure.variation_le_of_forall_enorm_le
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ ν : VectorMeasure X V
inst_3 : ContinuousAdd V
E : Set X
h : MeasurableSet E
⊢ ‖(↑μ : Set X → V) E + (↑ν : Set X → V) E‖ₑ ≤ ‖(↑μ : Set X → V) E‖ₑ + ‖(↑ν : Set X → V) E‖ₑ

Tactic:
enorm_add_le _ _

Premises used: enorm_add_le
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ ν : VectorMeasure X V
inst_3 : ContinuousAdd V
E : Set X
h : MeasurableSet E
h₁ : ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E
h₂ : ‖(↑ν : Set X → V) E‖ₑ ≤ (ν.variation : (a : Set X) → ℝ≥0∞) E
⊢ ‖(↑μ : Set X → V) E‖ₑ + ‖(↑ν : Set X → V) E‖ₑ ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞)
      ((ν.variation : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ ν : VectorMeasure X V
inst_3 : ContinuousAdd V
E : Set X
h : MeasurableSet E
⊢ ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E

Tactic:
enorm_measure_le_variation _ E

Premises used: MeasureTheory.VectorMeasure.enorm_measure_le_variation
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ ν : VectorMeasure X V
inst_3 : ContinuousAdd V
E : Set X
h : MeasurableSet E
⊢ ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E

Tactic:
exact enorm_measure_le_variation _ E

Premises used: MeasureTheory.VectorMeasure.enorm_measure_le_variation
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ ν : VectorMeasure X V
inst_3 : ContinuousAdd V
E : Set X
h : MeasurableSet E
⊢ ‖(↑ν : Set X → V) E‖ₑ ≤ (ν.variation : (a : Set X) → ℝ≥0∞) E

Tactic:
enorm_measure_le_variation _ E

Premises used: MeasureTheory.VectorMeasure.enorm_measure_le_variation
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ ν : VectorMeasure X V
inst_3 : ContinuousAdd V
E : Set X
h : MeasurableSet E
⊢ ‖(↑ν : Set X → V) E‖ₑ ≤ (ν.variation : (a : Set X) → ℝ≥0∞) E

Tactic:
exact enorm_measure_le_variation _ E

Premises used: MeasureTheory.VectorMeasure.enorm_measure_le_variation
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
μ ν : VectorMeasure X V
inst_3 : ContinuousAdd V
E : Set X
h : MeasurableSet E
_ :
  ‖(↑μ : Set X → V) E‖ₑ + ‖(↑ν : Set X → V) E‖ₑ ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞)
      ((ν.variation : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞)
⊢ ‖(↑(μ + ν) : Set X → V) E‖ₑ ≤ (μ.variation + ν.variation : (a : Set X) → ℝ≥0∞) E

Tactic:
calc
    _ ≤ ‖μ E‖ₑ + ‖ν E‖ₑ := enorm_add_le _ _
    _ ≤ μ.variation E + ν.variation E := by
      gcongr <;> exact enorm_measure_le_variation _ E

Premises used: MeasureTheory.VectorMeasure.variation, MeasureTheory.VectorMeasure.measureOf', enorm_add_le, DFunLike.coe
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
inst_3 : ContinuousAdd V
ι : Type u_3
μ : ι → VectorMeasure X V
⊢ LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ ∅, μ i)) (∑ i ∈ ∅, (μ i).variation)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
inst_3 : ContinuousAdd V
ι : Type u_3
μ : ι → VectorMeasure X V
i : ι
s : Finset ι
his : i ∉ s
ih : LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ s, μ i)) (∑ i ∈ s, (μ i).variation)
⊢ LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ insert i s, μ i))
    (∑ i ∈ insert i s, (μ i).variation)

Tactic:
simpa [Finset.sum_insert his] using
      variation_add_le.trans (add_le_add_right ih ((μ i).variation))

Premises used: MeasureTheory.VectorMeasure.variation, MeasureTheory.VectorMeasure.variation_add_le, add_le_add_right, LE.le.trans, Finset.sum_insert
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
inst_3 : ContinuousAdd V
ι : Type u_3
s : Finset ι
μ : ι → VectorMeasure X V
empty : LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ ∅, μ i)) (∑ i ∈ ∅, (μ i).variation)
insert :
  ∀ (i : ι) (s : Finset ι) (his : i ∉ s)
    (ih : LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ s, μ i)) (∑ i ∈ s, (μ i).variation)),
    LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ Insert.insert i s, μ i))
      (∑ i ∈ Insert.insert i s, (μ i).variation)
⊢ LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ s, μ i)) (∑ i ∈ s, (μ i).variation)

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert i s his ih =>
    simpa [Finset.sum_insert his] using
      variation_add_le.trans (add_le_add_right ih ((μ i).variation))

Premises used: MeasureTheory.VectorMeasure.empty, Insert.insert
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : TopologicalSpace V
inst_1 : ENormedAddCommMonoid V
inst_2 : T2Space V
inst_3 : ContinuousAdd V
ι : Type u_3
s : Finset ι
μ : ι → VectorMeasure X V
empty : LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ ∅, μ i)) (∑ i ∈ ∅, (μ i).variation)
insert :
  ∀ (i : ι) (s : Finset ι) (his : i ∉ s)
    (ih : LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ s, μ i)) (∑ i ∈ s, (μ i).variation)),
    LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ Insert.insert i s, μ i))
      (∑ i ∈ Insert.insert i s, (μ i).variation)
⊢ LE.le.{u_1} (α := Measure X) (variation.{u_1, u_2} (V := V) (∑ i ∈ s, μ i)) (∑ i ∈ s, (μ i).variation)

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert i s his ih =>
    simpa [Finset.sum_insert his] using
      variation_add_le.trans (add_le_add_right ih ((μ i).variation))

Premises used: MeasureTheory.VectorMeasure.empty, Insert.insert
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : NormedAddCommGroup V
μ : VectorMeasure X V
E : Set X
hE : Ne (α := ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E
⊢ ‖(↑μ : Set X → V) E‖ ≤ μ.variation.real E

Tactic:
rw [measureReal_def, ← toReal_enorm, ENNReal.toReal_le_toReal (enorm_ne_top) hE]

Premises used: toReal_enorm, MeasureTheory.measureReal_def, ENNReal.toReal_le_toReal, enorm_ne_top
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : NormedAddCommGroup V
μ : VectorMeasure X V
E : Set X
hE : Ne (α := ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E

Tactic:
enorm_measure_le_variation μ E

Premises used: MeasureTheory.VectorMeasure.enorm_measure_le_variation
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : NormedAddCommGroup V
μ : VectorMeasure X V
E : Set X
hE : Ne (α := ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E

Tactic:
exact enorm_measure_le_variation μ E

Premises used: MeasureTheory.VectorMeasure.enorm_measure_le_variation
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : NormedAddCommGroup V
μ : VectorMeasure X V
⊢ (-μ).variation = μ.variation

Tactic:
simp [variation]

Premises used: MeasureTheory.VectorMeasure.variation
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
Goal:
X : Type u_1
V : Type u_2
mX : MeasurableSpace X
inst : NormedAddCommGroup V
μ ν : VectorMeasure X V
grw : (μ + -ν).variation ≤ μ.variation + ν.variation
grw₁ : μ.variation + (-ν).variation ≤ μ.variation + ν.variation
grw₂ grw₃ : μ.variation + ν.variation ≤ μ.variation + ν.variation
⊢ (μ - ν).variation ≤ μ.variation + ν.variation

Tactic:
grw [sub_eq_add_neg, variation_add_le, variation_neg]

Premises used: MeasureTheory.VectorMeasure.variation_neg, sub_eq_add_neg, MeasureTheory.VectorMeasure.variation_add_le
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Defs
Goal:
X : Type u_1
inst : MeasurableSpace X
V : Type u_2
inst_1 : TopologicalSpace V
inst_2 : ENormedAddCommMonoid V
inst_3 : T2Space V
μ : VectorMeasure X V
s : ℕ → { t : Set X // MeasurableSet t }
hs : Pairwise (Function.onFun Disjoint (Subtype.val (p := fun (t : Set X) ↦ MeasurableSet t) ∘ s))
⊢ ∀ (i : ℕ), MeasurableSet (↑(s i) : Set X)

Tactic:
have hmeas : ∀ i, MeasurableSet (s i).val := fun i => (s i).prop
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Defs
Goal:
X : Type u_1
inst : MeasurableSpace X
V : Type u_2
inst_1 : TopologicalSpace V
inst_2 : ENormedAddCommMonoid V
inst_3 : T2Space V
μ : VectorMeasure X V
s : ℕ → { t : Set X // MeasurableSet t }
hs : Pairwise (Function.onFun Disjoint (Subtype.val (p := fun (t : Set X) ↦ MeasurableSet t) ∘ s))
hmeas : ∀ (i : ℕ), MeasurableSet (↑(s i) : Set X)
⊢ LE.le (α := ℝ≥0∞) ((fun (x : Set X) ↦ ‖(↑μ : Set X → V) x‖ₑ) (⋃ (i : ℕ), (↑(s i) : Set X)))
    (∑' (i : ℕ), (fun (x : Set X) ↦ ‖(↑μ : Set X → V) x‖ₑ) (↑(s i) : Set X))

Tactic:
simpa [VectorMeasure.of_disjoint_iUnion hmeas hs] using enorm_tsum_le_tsum_enorm

Premises used: MeasureTheory.VectorMeasure.of_disjoint_iUnion, enorm_tsum_le_tsum_enorm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Variation.Defs
Goal:
X : Type u_1
inst : MeasurableSpace X
V : Type u_2
inst_1 : TopologicalSpace V
inst_2 : ENormedAddCommMonoid V
inst_3 : T2Space V
μ : VectorMeasure X V
⊢ Eq (α := ℝ≥0∞) ((fun (x : Set X) ↦ ‖(↑μ : Set X → V) x‖ₑ) ∅) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ_1 : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : Integrable f μ
⊢ Eq.{u_2 + 1} (α := E) (if MeasurableSet.{u_1} (α := α) ∅ then ∫ (x : α) in ∅, f x ∂μ else 0) 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.WithDensity
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ_1 : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
f : α → E
hf : Integrable f μ
s : ℕ → Set α
hs₁ : ∀ (i : ℕ), MeasurableSet (s i)
hs₂ : Pairwise (Function.onFun Disjoint s)
⊢ HasSum.{u_2, 0} (α := E) (fun (n : ℕ) ↦ ∫ (x : α) in s n, f x ∂μ) (∫ (x : α) in ⋃ (n : ℕ), s n, f x ∂μ)

Tactic:
hasSum_integral_iUnion hs₁ hs₂ hf.integrableOn

Premises used: MeasureTheory.hasSum_integral_iUnion, MeasureTheory.Integrable.integrableOn