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 : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet (Q.parts (a := P.sup id))).sup id) :=
  Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
defQ' : Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
hQ' : ∀ t ∈ Q'.parts (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id), t ⊆ s
⊢ ‖(↑μ : Set X → V) ⊥‖ₑ = 0

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
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet (Q.parts (a := P.sup id))).sup id) :=
  Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
defQ' : Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
hQ' : ∀ t ∈ Q'.parts (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id), t ⊆ s
⊢ ∀ p ∈ Q.parts (a := P.sup id), p ∉ filter MeasurableSet (Q.parts (a := P.sup id)) → ‖(↑μ : Set X → V) p‖ₑ = 0

Tactic:
simp_all
-- 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 : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet (Q.parts (a := P.sup id))).sup id) :=
  Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
defQ' : Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
hQ' : ∀ t ∈ Q'.parts (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id), t ⊆ s
⊢ LE.le (α := ℝ≥0∞)
    (∑ p ∈ Q'.parts (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id), ‖(↑μ : Set X → V) p‖ₑ)
    (∑ p ∈ (Q'.extendOfLE (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) (b := s) ⋯).parts (a := s),
      ‖(↑μ : Set X → V) p‖ₑ)

Tactic:
sum_le_sum_of_subset (Q'.parts_subset_extendOfLE (Finset.sup_le hQ'))

Premises used: Finpartition.parts_subset_extendOfLE, Finset.sup_le, Finset.sum_le_sum_of_subset
-- 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 : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet (Q.parts (a := P.sup id))).sup id) :=
  Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
defQ' : Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
hQ' : ∀ t ∈ Q'.parts (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id), t ⊆ s
simp :
  ∑ p ∈ (Q'.extendOfLE (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) (b := s) ⋯).parts (a := s),
      ‖(↑μ : Set X → V) p‖ₑ ≤
    preVariationFun (fun (p : Set X) ↦ ‖(↑μ : Set X → V) p‖ₑ) s
⊢ LE.le (α := ℝ≥0∞)
    (∑ p ∈ (Q'.extendOfLE (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) (b := s) ⋯).parts (a := s),
        ‖(↑μ : Set X → V) p‖ₑ :
      ℝ≥0∞)
    ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [variation_apply, preVariation_apply, ennrealToMeasure_apply hs,
        ennrealPreVariation_apply]

Premises used: MeasureTheory.VectorMeasure.ennrealToMeasure_apply, MeasureTheory.preVariation_apply, 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
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet (Q.parts (a := P.sup id))).sup id) :=
  Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
defQ' : Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
hQ' : ∀ t ∈ Q'.parts (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id), t ⊆ s
hP :
  ∀ p ∈ (Q'.extendOfLE (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) (b := s) ⋯).parts (a := s),
    MeasurableSet p
⊢ ∑ p ∈ (Q'.extendOfLE (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) (b := s) ⋯).parts (a := s),
      ‖(↑μ : Set X → V) p‖ₑ ≤
    preVariationFun (fun (p : Set X) ↦ ‖(↑μ : Set X → V) p‖ₑ) s

Tactic:
apply preVariation.sum_le' (fun p => ‖μ p‖ₑ) hs

Premises used: MeasureTheory.VectorMeasure.measureOf', ENorm.enorm, MeasureTheory.preVariation.sum_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
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet (Q.parts (a := P.sup id))).sup id) :=
  Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
defQ' : Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
hQ' : ∀ t ∈ Q'.parts (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id), t ⊆ s
p : Set X
hp : p ∈ (Q'.extendOfLE (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) (b := s) ⋯).parts (a := s)
hP : ∀ (h : p ∈ Q'.parts (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id)), MeasurableSet p
hP₃ :
  ∀
    (hp :
      s \ (filter MeasurableSet (Q.parts (a := P.sup id))).sup id ∈
        (Q'.extendOfLE (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) (b := s) ⋯).parts (a := s)),
    MeasurableSet (s \ (filter MeasurableSet (Q.parts (a := P.sup id))).sup id)
⊢ MeasurableSet p

Tactic:
rcases Q'.mem_parts_or_eq_sdiff_of_mem_extendOfLE _ hp with h | rfl

Premises used: Finpartition.mem_parts_or_eq_sdiff_of_mem_extendOfLE, rfl
-- 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 : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet (Q.parts (a := P.sup id))).sup id) :=
  Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
defQ' : Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
hQ' : ∀ t ∈ Q'.parts (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id), t ⊆ s
p : Set X
hp : p ∈ (Q'.extendOfLE (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) (b := s) ⋯).parts (a := s)
h : p ∈ Q'.parts (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id)
⊢ MeasurableSet p

Tactic:
simp_all
-- 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 : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet (Q.parts (a := P.sup id))).sup id) :=
  Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
defQ' : Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
hQ' : ∀ t ∈ Q'.parts (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id), t ⊆ s
hp :
  s \ (filter MeasurableSet (Q.parts (a := P.sup id))).sup id ∈
    (Q'.extendOfLE (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) (b := s) ⋯).parts (a := s)
hP : MeasurableSet (s \ ⋃ x ∈ filter MeasurableSet (Q.parts (a := P.sup id)), x)
⊢ MeasurableSet (s \ (filter MeasurableSet (Q.parts (a := P.sup id))).sup id)

Tactic:
simp only [sup_set_eq_biUnion, id_eq]

Premises used: Finset.sup_set_eq_biUnion, id_eq
-- 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 : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet (Q.parts (a := P.sup id))).sup id) :=
  Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
defQ' : Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
hQ' : ∀ t ∈ Q'.parts (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id), t ⊆ s
hp :
  s \ (filter MeasurableSet (Q.parts (a := P.sup id))).sup id ∈
    (Q'.extendOfLE (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) (b := s) ⋯).parts (a := s)
⊢ ∀ b ∈ (↑(filter MeasurableSet (Q.parts (a := P.sup id))) : Set (Set X)), MeasurableSet b

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
μ : VectorMeasure X V
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet (Q.parts (a := P.sup id))).sup id) :=
  Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
defQ' : Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
hQ' : ∀ t ∈ Q'.parts (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id), t ⊆ s
hp :
  s \ (filter MeasurableSet (Q.parts (a := P.sup id))).sup id ∈
    (Q'.extendOfLE (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) (b := s) ⋯).parts (a := s)
⊢ MeasurableSet (s \ ⋃ x ∈ filter MeasurableSet (Q.parts (a := P.sup id)), x)

Tactic:
exact hs.diff <| .biUnion (Finset.countable_toSet _) (by simp)

Premises used: MeasurableSet.diff
-- 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 : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
Q : Finpartition (P.sup id) := Finpartition.ofPairwiseDisjoint P hP₂
defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂
Q' : Finpartition ((filter MeasurableSet (Q.parts (a := P.sup id))).sup id) :=
  Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
defQ' : Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯
hQ' : ∀ t ∈ Q'.parts (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id), t ⊆ s
p :
  LE.le (α := ℝ≥0∞)
    (∑ p ∈ (Q'.extendOfLE (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) (b := s) ⋯).parts (a := s),
        ‖(↑μ : Set X → V) p‖ₑ :
      ℝ≥0∞)
    ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑ p ∈ P, ‖(↑μ : Set X → V) p‖ₑ : ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
calc
    ∑ p ∈ P, ‖μ p‖ₑ = ∑ p ∈ Q.parts, ‖μ p‖ₑ :=
      (Finpartition.sum_ofPairwiseDisjoint_eq_sum hP₂ (by simp)).symm
    _ = ∑ p ∈ Q'.parts, ‖μ p‖ₑ := (Q.sum_ofSubset_eq_sum _ _ _ (by simp_all)).symm
    _ ≤ ∑ p ∈ (Q'.extendOfLE (Finset.sup_le hQ')).parts, ‖μ p‖ₑ :=
      sum_le_sum_of_subset (Q'.parts_subset_extendOfLE (Finset.sup_le hQ'))
    _ ≤ μ.variation s := by
      simp only [variation_apply, preVariation_apply, ennrealToMeasure_apply hs,
        ennrealPreVariation_apply]
      apply preVariation.sum_le' (fun p => ‖μ p‖ₑ) hs
      intro p hp
      rcases Q'.mem_parts_or_eq_sdiff_of_mem_extendOfLE _ hp with h | rfl
      · simp_all
      simp only [sup_set_eq_biUnion, id_eq]
      exact hs.diff <| .biUnion (Finset.countable_toSet _) (by simp)

Premises used: MeasureTheory.VectorMeasure.variation, Finpartition.parts_subset_extendOfLE, Finpartition.extendOfLE, Finset.sup_le, Finpartition.parts, Finpartition.sum_ofPairwiseDisjoint_eq_sum, Finset.sum_le_sum_of_subset, Finpartition.sum_ofSubset_eq_sum, Eq.symm, 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
s : Set X
hs : MeasurableSet s
P : Finset (Set X)
hP₁ : ∀ t ∈ P, t ⊆ s
hP₂ : (↑P : Set (Set X)).PairwiseDisjoint id
set set₁ : LE.le (α := ℝ≥0∞) (∑ p ∈ P, ‖(↑μ : Set X → V) p‖ₑ : ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
set₂ :
  let Q := Finpartition.ofPairwiseDisjoint P hP₂;
  ∀ (defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂),
    LE.le (α := ℝ≥0∞) (∑ p ∈ P, ‖(↑μ : Set X → V) p‖ₑ : ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
set₃ :
  let Q := Finpartition.ofPairwiseDisjoint P hP₂;
  ∀ (defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂),
    let Q' : Finpartition ((filter MeasurableSet (Q.parts (a := P.sup id))).sup id) :=
      Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯;
    ∀ (defQ' : Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯),
      LE.le (α := ℝ≥0∞) (∑ p ∈ P, ‖(↑μ : Set X → V) p‖ₑ : ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
set₄ :
  let Q := Finpartition.ofPairwiseDisjoint P hP₂;
  ∀ (defQ : Q = Finpartition.ofPairwiseDisjoint P hP₂),
    let Q' : Finpartition ((filter MeasurableSet (Q.parts (a := P.sup id))).sup id) :=
      Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯;
    ∀ (defQ' : Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) ⋯ ⋯)
      (hQ' : ∀ t ∈ Q'.parts (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id), t ⊆ s),
      LE.le (α := ℝ≥0∞) (∑ p ∈ P, ‖(↑μ : Set X → V) p‖ₑ : ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑ p ∈ P, ‖(↑μ : Set X → V) p‖ₑ : ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
classical
  set Q := Finpartition.ofPairwiseDisjoint P hP₂ with defQ
  set Q' := Q.ofSubset (filter_subset MeasurableSet Q.parts) rfl with defQ'
  have hQ' : ∀ t ∈ Q'.parts, t ⊆ s := by simp [Q', Q]; grind
  calc
    ∑ p ∈ P, ‖μ p‖ₑ = ∑ p ∈ Q.parts, ‖μ p‖ₑ :=
      (Finpartition.sum_ofPairwiseDisjoint_eq_sum hP₂ (by simp)).symm
    _ = ∑ p ∈ Q'.parts, ‖μ p‖ₑ := (Q.sum_ofSubset_eq_sum _ _ _ (by simp_all)).symm
    _ ≤ ∑ p ∈ (Q'.extendOfLE (Finset.sup_le hQ')).parts, ‖μ p‖ₑ :=
      sum_le_sum_of_subset (Q'.parts_subset_extendOfLE (Finset.sup_le hQ'))
    _ ≤ μ.variation s := by
      simp only [variation_apply, preVariation_apply, ennrealToMeasure_apply hs,
        ennrealPreVariation_apply]
      apply preVariation.sum_le' (fun p => ‖μ p‖ₑ) hs
      intro p hp
      rcases Q'.mem_parts_or_eq_sdiff_of_mem_extendOfLE _ hp with h | rfl
      · simp_all
      simp only [sup_set_eq_biUnion, id_eq]
      exact hs.diff <| .biUnion (Finset.countable_toSet _) (by simp)

Premises used: MeasureTheory.VectorMeasure.variation, Finpartition.ofPairwiseDisjoint, Finpartition.sum_ofPairwiseDisjoint_eq_sum, Eq.symm, 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
E : Set X
pos : ∀ (hE : MeasurableSet E), ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E
neg : ∀ (hE : ¬MeasurableSet E), ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E
⊢ ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E

Tactic:
by_cases hE : MeasurableSet E

Premises used: MeasurableSet
-- 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
E : Set X
hE : ¬MeasurableSet E
⊢ ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E

Tactic:
simp [μ.not_measurable' hE]

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
E : Set X
hE : MeasurableSet E
pos : ∀ (hE' : Subtype.mk (p := MeasurableSet) E hE = ⊥), ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E
neg : ∀ (hE' : ¬Subtype.mk (p := MeasurableSet) E hE = ⊥), ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E
⊢ ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E

Tactic:
by_cases hE' : (⟨E, hE⟩ : Subtype MeasurableSet) = ⊥

Premises used: Subtype.mk
-- 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
E : Set X
hE : MeasurableSet E
hE' : Subtype.mk (p := MeasurableSet) E hE = ⊥
⊢ ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E

Tactic:
simp_all
-- 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
E : Set X
hE : MeasurableSet E
hE' : ¬Subtype.mk (p := MeasurableSet) E hE = ⊥
neg : ‖(↑μ : Set X → V) E‖ₑ ≤ preVariationFun (fun (x : Set X) ↦ ‖(↑μ : Set X → V) x‖ₑ) E
⊢ ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E

Tactic:
simp only [variation_apply, preVariation, ennrealToMeasure_apply hE, ennrealPreVariation_apply]

Premises used: MeasureTheory.VectorMeasure.ennrealToMeasure_apply, MeasureTheory.preVariation, 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
E : Set X
hE : MeasurableSet E
hE' : ¬Subtype.mk (p := MeasurableSet) E hE = ⊥
⊢ ‖(↑μ : Set X → V) E‖ₑ = ∑ p ∈ (Finpartition.indiscrete hE').parts, ‖(↑μ : Set X → V) (↑p : Set X)‖ₑ

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
μ : VectorMeasure X V
E : Set X
hE : MeasurableSet E
hE' : ¬Subtype.mk (p := MeasurableSet) E hE = ⊥
⊢ ∑ p ∈ (Finpartition.indiscrete hE').parts, ‖(↑μ : Set X → V) (↑p : Set X)‖ₑ ≤
    preVariationFun (fun (x : Set X) ↦ ‖(↑μ : Set X → V) x‖ₑ) E

Tactic:
apply preVariation.sum_le

Premises used: MeasureTheory.preVariation.sum_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
E : Set X
hE : MeasurableSet E
hE' : ¬Subtype.mk (p := MeasurableSet) E hE = ⊥
p : ‖(↑μ : Set X → V) E‖ₑ = ∑ p ∈ (Finpartition.indiscrete hE').parts, ‖(↑μ : Set X → V) (↑p : Set X)‖ₑ
p₁ :
  ∑ p ∈ (Finpartition.indiscrete hE').parts, ‖(↑μ : Set X → V) (↑p : Set X)‖ₑ ≤
    preVariationFun (fun (x : Set X) ↦ ‖(↑μ : Set X → V) x‖ₑ) E
⊢ ‖(↑μ : Set X → V) E‖ₑ ≤ preVariationFun (fun (x : Set X) ↦ ‖(↑μ : Set X → V) x‖ₑ) E

Tactic:
calc
    ‖μ E‖ₑ = ∑ p ∈ (Finpartition.indiscrete hE').parts, ‖μ p‖ₑ := by simp
    _ ≤ preVariationFun (‖μ ·‖ₑ) E := by apply preVariation.sum_le

Premises used: MeasureTheory.VectorMeasure.measureOf', Finpartition.parts, ENorm.enorm, MeasureTheory.preVariationFun, Finpartition.indiscrete
-- 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
simp : Eq.{u_1 + 1} (α := Measure X) (preVariation (fun (x : Set X) ↦ 0) ⋯ ⋯) 0
⊢ Eq.{u_1 + 1} (α := Measure X) (variation.{u_1, u_2} (V := V) 0) 0

Tactic:
simp only [variation, coe_zero, Pi.zero_apply, enorm_zero]

Premises used: MeasureTheory.VectorMeasure.variation, MeasureTheory.VectorMeasure.coe_zero, Pi.zero_apply, enorm_zero
-- 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
⊢ Eq.{u_1 + 1} (α := Measure X) (preVariation (fun (x : Set X) ↦ 0) ⋯ ⋯) 0

Tactic:
preVariation_zero

Premises used: MeasureTheory.preVariation_zero
-- 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
⊢ Eq.{u_1 + 1} (α := Measure X) (preVariation (fun (x : Set X) ↦ 0) ⋯ ⋯) 0

Tactic:
exact preVariation_zero

Premises used: MeasureTheory.preVariation_zero
-- 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
pos : ∀ (hsm : MeasurableSet s), (↑μ : Set X → V) s = 0
neg : ∀ (hsm : ¬MeasurableSet s), (↑μ : Set X → V) s = 0
⊢ (↑μ : Set X → V) s = 0

Tactic:
by_cases hsm : MeasurableSet s

Premises used: MeasurableSet
-- 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
this : ‖(↑μ : Set X → V) s‖ₑ ≤ 0
⊢ (↑μ : Set X → V) s = 0

Tactic:
simp_all
-- 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 : ‖(↑μ : Set X → V) s‖ₑ ≤ 0
⊢ (↑μ : Set X → V) s = 0

Tactic:
suffices ‖μ s‖ₑ ≤ 0 by simp_all