awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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'.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
have hP : ∀ p ∈ (Q'.extendOfLE (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) (b := s) sorry).parts (a := s),
  MeasurableSet p
Tactic: apply preVariation.sum_le' (fun p => ‖μ p‖ₑ) hs
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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)
⊢ MeasurableSet p
have hP : ∀ (h : p ∈ Q'.parts (a := (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
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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
⊢ MeasurableSet p
have 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) sorry).parts (a := s)),
  MeasurableSet (s \ (filter MeasurableSet (Q.parts (a := P.sup id))).sup id)
Tactic: rcases Q'.mem_parts_or_eq_sdiff_of_mem_extendOfLE _ hp with h | rfl
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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 \ (filter MeasurableSet (Q.parts (a := P.sup id))).sup id)
have hP : MeasurableSet (s \ ⋃ x ∈ filter MeasurableSet (Q.parts (a := P.sup id)), x)
Tactic: simp only [sup_set_eq_biUnion, id_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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 ∈ P, ‖(↑μ : Set X → V) p‖ₑ : ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have p : LE.le (α := ℝ≥0∞)
  (∑ p ∈ (Q'.extendOfLE (a := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) (b := s) sorry).parts (a := s),
      ‖(↑μ : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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∞)
⊢ LE.le (α := ℝ≥0∞) (∑ p ∈ P, ‖(↑μ : Set X → V) p‖ₑ : ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
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)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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∞)
⊢ LE.le (α := ℝ≥0∞) (∑ p ∈ P, ‖(↑μ : Set X → V) p‖ₑ : ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have 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) sorry sorry;
  ∀ (defQ' : Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) sorry sorry),
    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)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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∞)
⊢ LE.le (α := ℝ≥0∞) (∑ p ∈ P, ‖(↑μ : Set X → V) p‖ₑ : ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have 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) sorry sorry;
  ∀ (defQ' : Q' = Q.ofSubset (a := P.sup id) (b := (filter MeasurableSet (Q.parts (a := P.sup id))).sup id) sorry sorry)
    (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∞)
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)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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
⊢ ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E
have pos : ∀ (hE : MeasurableSet E), ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E
Tactic: by_cases hE : MeasurableSet E
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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
⊢ ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E
have neg : ∀ (hE : ¬MeasurableSet E), ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E
Tactic: by_cases hE : MeasurableSet E
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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
have pos : ∀ (hE' : Subtype.mk (p := MeasurableSet) E hE = ⊥), ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E
Tactic: by_cases hE' : (⟨E, hE⟩ : Subtype MeasurableSet) = ⊥
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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
⊢ ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E
have neg : ∀ (hE' : ¬Subtype.mk (p := MeasurableSet) E hE = ⊥), ‖(↑μ : Set X → V) E‖ₑ ≤ (μ.variation : (a : Set X) → ℝ≥0∞) E
Tactic: by_cases hE' : (⟨E, hE⟩ : Subtype MeasurableSet) = ⊥
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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
have neg : ‖(↑μ : Set X → V) E‖ₑ ≤ preVariationFun (fun (x : Set X) ↦ ‖(↑μ : Set X → V) x‖ₑ) E
Tactic: simp only [variation_apply, preVariation, ennrealToMeasure_apply hE, ennrealPreVariation_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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‖ₑ ≤ preVariationFun (fun (x : Set X) ↦ ‖(↑μ : Set X → V) x‖ₑ) E
have p : ‖(↑μ : Set X → V) E‖ₑ = ∑ p ∈ (Finpartition.indiscrete hE').parts, ‖(↑μ : Set X → V) (↑p : Set X)‖ₑ
Tactic: calc
    ‖μ E‖ₑ = ∑ p ∈ (Finpartition.indiscrete hE').parts, ‖μ p‖ₑ := by simp
    _ ≤ preVariationFun (‖μ ·‖ₑ) E := by apply preVariation.sum_le
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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)‖ₑ
⊢ ‖(↑μ : Set X → V) E‖ₑ ≤ preVariationFun (fun (x : Set X) ↦ ‖(↑μ : Set X → V) x‖ₑ) E
have p₁ : ∑ p ∈ (Finpartition.indiscrete hE').parts, ‖(↑μ : Set X → V) (↑p : Set X)‖ₑ ≤
  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
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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) (variation.{u_1, u_2} (V := V) 0) 0
have simp : Eq.{u_1 + 1} (α := Measure X) (preVariation (fun (x : Set X) ↦ 0) sorry sorry) 0
Tactic: simp only [variation, coe_zero, Pi.zero_apply, enorm_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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
⊢ (↑μ : Set X → V) s = 0
have pos : ∀ (hsm : MeasurableSet s), (↑μ : Set X → V) s = 0
Tactic: by_cases hsm : MeasurableSet s
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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
⊢ (↑μ : Set X → V) s = 0
have neg : ∀ (hsm : ¬MeasurableSet s), (↑μ : Set X → V) s = 0
Tactic: by_cases hsm : MeasurableSet s
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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
have pos : ‖(↑μ : Set X → V) s‖ₑ ≤ 0
Tactic: suffices ‖μ s‖ₑ ≤ 0 by simp_all
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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
have pos : LE.le (α := ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: grw [enorm_measure_le_variation, ← ennrealVariation_apply _ hsm, hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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∞)
⊢ ‖(↑μ : Set X → V) s‖ₑ ≤ 0
have pos₁ : (↑μ.ennrealVariation : Set X → ℝ≥0∞) s ≤ 0
Tactic: grw [enorm_measure_le_variation, ← ennrealVariation_apply _ hsm, hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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
⊢ ‖(↑μ : Set X → V) s‖ₑ ≤ 0
have pos₂ : LE.le (α := ℝ≥0∞) 0 0
Tactic: grw [enorm_measure_le_variation, ← ennrealVariation_apply _ hsm, hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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
have 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∞)
Tactic: refine Measure.le_intro fun s hs _ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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
⊢ LE.le (α := ℝ≥0∞) ((μ.variation : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
have simp : ∀ (i : Finpartition (Subtype.mk (p := MeasurableSet) s sorry)),
  LE.le (α := ℝ≥0∞) (∑ x ∈ i.parts, ‖(↑μ : Set X → V) (↑x : Set X)‖ₑ : ℝ≥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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Variation.Basic (goal)
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∞) (i.parts.sup (Subtype.val (p := MeasurableSet))) : ℝ≥0∞)
have 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∞)
Tactic: rw [sup_set_eq_biUnion]