awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : (↑ε' : ℝ≥0∞) ≤ preVariationFun f s
this_1 : ε' ≤ ε
hw : preVariationFun f s ≠ 0
this : 0 < ε'
a : ℝ≥0∞ := preVariationFun f s - (↑ε' : ℝ≥0∞)
ha : a < preVariationFun f s
inl :
  ∀ (P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)) (hP : a < ∑ p ∈ P.parts, f (↑p : Set X)),
    ∃ (P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)),
      preVariationFun f s ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)
⊢ ∃ (P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)),
    preVariationFun f s ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)

Tactic:
obtain ⟨P, hP⟩ := exists_Finpartition_sum_gt f hs ha

Premises used: MeasureTheory.preVariation.exists_Finpartition_sum_gt
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : (↑ε' : ℝ≥0∞) ≤ preVariationFun f s
this_1 : ε' ≤ ε
hw : preVariationFun f s ≠ 0
this : 0 < ε'
a : ℝ≥0∞ := preVariationFun f s - (↑ε' : ℝ≥0∞)
ha : a < preVariationFun f s
P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)
hP : a < ∑ p ∈ P.parts, f (↑p : Set X)
h₁ : preVariationFun f s ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)
⊢ ∃ (P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)),
    preVariationFun f s ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)

Tactic:
use P
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : (↑ε' : ℝ≥0∞) ≤ preVariationFun f s
this_1 : ε' ≤ ε
hw : preVariationFun f s ≠ 0
this : 0 < ε'
a : ℝ≥0∞ := preVariationFun f s - (↑ε' : ℝ≥0∞)
ha : a < preVariationFun f s
P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)
hP : a < ∑ p ∈ P.parts, f (↑p : Set X)
⊢ preVariationFun f s = a + (↑ε' : ℝ≥0∞)

Tactic:
(tsub_add_cancel_of_le hε').symm

Premises used: tsub_add_cancel_of_le, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : (↑ε' : ℝ≥0∞) ≤ preVariationFun f s
this_1 : ε' ≤ ε
hw : preVariationFun f s ≠ 0
this : 0 < ε'
a : ℝ≥0∞ := preVariationFun f s - (↑ε' : ℝ≥0∞)
ha : a < preVariationFun f s
P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)
hP : a < ∑ p ∈ P.parts, f (↑p : Set X)
⊢ a + (↑ε' : ℝ≥0∞) ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε' : ℝ≥0∞)

Tactic:
(ENNReal.add_le_add_iff_right coe_ne_top).mpr (le_of_lt hP)

Premises used: Iff.mpr, ENNReal.add_le_add_iff_right, le_of_lt, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : (↑ε' : ℝ≥0∞) ≤ preVariationFun f s
this_1 : ε' ≤ ε
hw : preVariationFun f s ≠ 0
this : 0 < ε'
a : ℝ≥0∞ := preVariationFun f s - (↑ε' : ℝ≥0∞)
ha : a < preVariationFun f s
P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)
hP : a < ∑ p ∈ P.parts, f (↑p : Set X)
⊢ a + (↑ε' : ℝ≥0∞) ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε' : ℝ≥0∞)

Tactic:
exact (ENNReal.add_le_add_iff_right coe_ne_top).mpr (le_of_lt hP)

Premises used: Iff.mpr, ENNReal.add_le_add_iff_right, le_of_lt, ENNReal.coe_ne_top
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : (↑ε' : ℝ≥0∞) ≤ preVariationFun f s
this_1 : ε' ≤ ε
hw : preVariationFun f s ≠ 0
this : 0 < ε'
a : ℝ≥0∞ := preVariationFun f s - (↑ε' : ℝ≥0∞)
ha : a < preVariationFun f s
P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)
hP : a < ∑ p ∈ P.parts, f (↑p : Set X)
⊢ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε' : ℝ≥0∞) ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : (↑ε' : ℝ≥0∞) ≤ preVariationFun f s
this_1 : ε' ≤ ε
hw : preVariationFun f s ≠ 0
this : 0 < ε'
a : ℝ≥0∞ := preVariationFun f s - (↑ε' : ℝ≥0∞)
ha : a < preVariationFun f s
P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)
hP : a < ∑ p ∈ P.parts, f (↑p : Set X)
calc : a + (↑ε' : ℝ≥0∞) ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε' : ℝ≥0∞)
calc₁ : ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε' : ℝ≥0∞) ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)
⊢ preVariationFun f s ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)

Tactic:
calc preVariationFun f s
      _ = a + ε' := (tsub_add_cancel_of_le hε').symm
      _ ≤ ∑ p ∈ P.parts, f p + ε' := by
        exact (ENNReal.add_le_add_iff_right coe_ne_top).mpr (le_of_lt hP)
      _ ≤ ∑ p ∈ P.parts, f p + ε := by gcongr

Premises used: tsub_add_cancel_of_le, Finpartition.parts, MeasureTheory.preVariationFun, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : Set X
hs : MeasurableSet s
ε : ℝ≥0
hε : 0 < ε
h : preVariationFun f s ≠ ∞
ε' : ℝ≥0 := min ε (preVariationFun f s).toNNReal
hε' : (↑ε' : ℝ≥0∞) ≤ preVariationFun f s
this : ε' ≤ ε
hw : preVariationFun f s = 0
⊢ ∃ (P : Finpartition (Subtype.mk (p := MeasurableSet) s hs)),
    preVariationFun f s ≤ ∑ p ∈ P.parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)

Tactic:
simp [*]
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition (Subtype.mk (p := MeasurableSet) (s i) ⋯)
n : ℕ
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
i : ℕ
h : i ∈ (↑(Finset.range n) : Set ℕ)
j : ℕ
h_1 : j ∈ (↑(Finset.range n) : Set ℕ)
hij : i ≠ j
simp : (↑(s' i ⊓ s' j) : Set X) = (↑⊥ : Set X)
⊢ (Disjoint on s') i j

Tactic:
simp only [Function.onFun, disjoint_iff, Subtype.ext_iff]

Premises used: Function.onFun, disjoint_iff, Subtype.ext_iff
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition (Subtype.mk (p := MeasurableSet) (s i) ⋯)
n : ℕ
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
i : ℕ
h : i ∈ (↑(Finset.range n) : Set ℕ)
j : ℕ
h_1 : j ∈ (↑(Finset.range n) : Set ℕ)
hij : i ≠ j
⊢ (↑(s' i ⊓ s' j) : Set X) = (↑⊥ : Set X)

Tactic:
Set.disjoint_iff_inter_eq_empty.mp (hs' hij)

Premises used: Set.disjoint_iff_inter_eq_empty, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition (Subtype.mk (p := MeasurableSet) (s i) ⋯)
n : ℕ
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
i : ℕ
h : i ∈ (↑(Finset.range n) : Set ℕ)
j : ℕ
h_1 : j ∈ (↑(Finset.range n) : Set ℕ)
hij : i ≠ j
⊢ (↑(s' i ⊓ s' j) : Set X) = (↑⊥ : Set X)

Tactic:
exact Set.disjoint_iff_inter_eq_empty.mp (hs' hij)

Premises used: Set.disjoint_iff_inter_eq_empty, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition (Subtype.mk (p := MeasurableSet) (s i) ⋯)
n : ℕ
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
⊢ (↑(Finset.range n) : Set ℕ).PairwiseDisjoint s'

Tactic:
have hs_disj : Set.PairwiseDisjoint (Finset.range n : Set ℕ) s' := fun i _ j _ hij => by
    simp only [Function.onFun, disjoint_iff, Subtype.ext_iff]
    exact Set.disjoint_iff_inter_eq_empty.mp (hs' hij)
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition (Subtype.mk (p := MeasurableSet) (s i) ⋯)
n : ℕ
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
hs_disj : (↑(Finset.range n) : Set ℕ).PairwiseDisjoint s'
Q : Finpartition (α := Subtype (α := Set X) MeasurableSet)
  ((Finset.range n).sup fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯) :=
  Finpartition.combine P ⋯
⊢ ∀ ⦃x y : Set X⦄, MeasurableSet x → MeasurableSet y → MeasurableSet (x ⊔ y)

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition (Subtype.mk (p := MeasurableSet) (s i) ⋯)
n : ℕ
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
hs_disj : (↑(Finset.range n) : Set ℕ).PairwiseDisjoint s'
Q : Finpartition (α := Subtype (α := Set X) MeasurableSet)
  ((Finset.range n).sup fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯) :=
  Finpartition.combine P ⋯
rw : ⋃ x ∈ Finset.range n, (↑(s' x) : Set X) ≤ (↑(Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯) : Set X)
⊢ (Finset.range n).sup s' ≤ Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯

Tactic:
rw [← Subtype.coe_le_coe, Finset.sup_coe (Psup := by measurability), Finset.sup_set_eq_biUnion]

Premises used: Finset.sup_coe, Finset.sup_set_eq_biUnion, Subtype.coe_le_coe
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition (Subtype.mk (p := MeasurableSet) (s i) ⋯)
n : ℕ
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
hs_disj : (↑(Finset.range n) : Set ℕ).PairwiseDisjoint s'
Q : Finpartition (α := Subtype (α := Set X) MeasurableSet)
  ((Finset.range n).sup fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯) :=
  Finpartition.combine P ⋯
⊢ ⋃ x ∈ Finset.range n, (↑(s' x) : Set X) ≤ (↑(Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯) : Set X)

Tactic:
Set.iUnion₂_subset fun i _ => Set.subset_iUnion s i

Premises used: Set.iUnion₂_subset, Set.subset_iUnion
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition (Subtype.mk (p := MeasurableSet) (s i) ⋯)
n : ℕ
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
hs_disj : (↑(Finset.range n) : Set ℕ).PairwiseDisjoint s'
Q : Finpartition (α := Subtype (α := Set X) MeasurableSet)
  ((Finset.range n).sup fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯) :=
  Finpartition.combine P ⋯
⊢ ⋃ x ∈ Finset.range n, (↑(s' x) : Set X) ≤ (↑(Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯) : Set X)

Tactic:
exact Set.iUnion₂_subset fun i _ => Set.subset_iUnion s i

Premises used: Set.iUnion₂_subset, Set.subset_iUnion
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition (Subtype.mk (p := MeasurableSet) (s i) ⋯)
n : ℕ
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
hs_disj : (↑(Finset.range n) : Set ℕ).PairwiseDisjoint s'
Q : Finpartition (α := Subtype (α := Set X) MeasurableSet)
  ((Finset.range n).sup fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯) :=
  Finpartition.combine P ⋯
⊢ (Finset.range n).sup s' ≤ Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯

Tactic:
have hQ_le : (Finset.range n).sup s' ≤ ⟨⋃ i, s i, MeasurableSet.iUnion hs⟩ := by
    rw [← Subtype.coe_le_coe, Finset.sup_coe (Psup := by measurability), Finset.sup_set_eq_biUnion]
    exact Set.iUnion₂_subset fun i _ => Set.subset_iUnion s i
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition (Subtype.mk (p := MeasurableSet) (s i) ⋯)
n : ℕ
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
hs_disj : (↑(Finset.range n) : Set ℕ).PairwiseDisjoint s'
Q : Finpartition (α := Subtype (α := Set X) MeasurableSet)
  ((Finset.range n).sup fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯) :=
  Finpartition.combine P ⋯
hQ_le : (Finset.range n).sup s' ≤ Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯
R : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯) := Q.extendOfLE hQ_le
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f (↑p : Set X)) (∑ p ∈ Q.parts, f (↑p : Set X))

Tactic:
(Finpartition.sum_combine P hs_disj.supIndep (fun p => f p)).symm

Premises used: Eq.symm, Subtype.val, Finpartition.sum_combine, Set.PairwiseDisjoint.supIndep
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition (Subtype.mk (p := MeasurableSet) (s i) ⋯)
n : ℕ
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
hs_disj : (↑(Finset.range n) : Set ℕ).PairwiseDisjoint s'
Q : Finpartition (α := Subtype (α := Set X) MeasurableSet)
  ((Finset.range n).sup fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯) :=
  Finpartition.combine P ⋯
hQ_le : (Finset.range n).sup s' ≤ Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯
R : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯) := Q.extendOfLE hQ_le
⊢ LE.le (α := ℝ≥0∞) (∑ p ∈ Q.parts, f (↑p : Set X)) (∑ p ∈ R.parts, f (↑p : Set X))

Tactic:
Finset.sum_le_sum_of_subset (Q.parts_subset_extendOfLE hQ_le)

Premises used: Finpartition.parts_subset_extendOfLE, Finset.sum_le_sum_of_subset
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition (Subtype.mk (p := MeasurableSet) (s i) ⋯)
n : ℕ
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
hs_disj : (↑(Finset.range n) : Set ℕ).PairwiseDisjoint s'
Q : Finpartition (α := Subtype (α := Set X) MeasurableSet)
  ((Finset.range n).sup fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯) :=
  Finpartition.combine P ⋯
hQ_le : (Finset.range n).sup s' ≤ Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯
R : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯) := Q.extendOfLE hQ_le
⊢ ∑ p ∈ R.parts, f (↑p : Set X) ≤ preVariationFun f (⋃ (i : ℕ), s i)

Tactic:
sum_le f (MeasurableSet.iUnion hs) R

Premises used: MeasureTheory.preVariation.sum_le, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
P : (i : ℕ) → Finpartition (Subtype.mk (p := MeasurableSet) (s i) ⋯)
n : ℕ
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
hs_disj : (↑(Finset.range n) : Set ℕ).PairwiseDisjoint s'
Q : Finpartition (α := Subtype (α := Set X) MeasurableSet)
  ((Finset.range n).sup fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯) :=
  Finpartition.combine P ⋯
hQ_le : (Finset.range n).sup s' ≤ Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯
R : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯) := Q.extendOfLE hQ_le
⊢ ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f (↑p : Set X) ≤ preVariationFun f (⋃ (i : ℕ), s i)

Tactic:
calc ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f p
    _ = ∑ p ∈ Q.parts, f p := (Finpartition.sum_combine P hs_disj.supIndep (fun p => f p)).symm
    _ ≤ ∑ p ∈ R.parts, f p := Finset.sum_le_sum_of_subset (Q.parts_subset_extendOfLE hQ_le)
    _ ≤ preVariationFun f (⋃ i, s i) := sum_le f (MeasurableSet.iUnion hs) R

Premises used: Finpartition.parts_subset_extendOfLE, Finpartition.parts, Finset.sum_le_sum_of_subset, Finset.range, MeasureTheory.preVariation.sum_le, MeasureTheory.preVariationFun, MeasurableSet.iUnion, Eq.symm, Subtype.val, Set.iUnion, Finpartition.sum_combine, Set.PairwiseDisjoint.supIndep
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
⊢ ∑' (i : ℕ), preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i)

Tactic:
ENNReal.tsum_le_of_sum_range_le fun n ↦ ?_

Premises used: ENNReal.tsum_le_of_sum_range_le
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
refine : ∀ (n : ℕ), ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i)
⊢ ∑' (i : ℕ), preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i)

Tactic:
refine ENNReal.tsum_le_of_sum_range_le fun n ↦ ?_

Premises used: ENNReal.tsum_le_of_sum_range_le
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
pos : ∀ (hn : n = 0), ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i)
neg : ∀ (hn : ¬n = 0), ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i)
⊢ ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i)

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
hn : n = 0
⊢ ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i)

Tactic:
simp [hn]
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
hn : ¬n = 0
⊢ ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i)

Tactic:
ENNReal.le_of_forall_pos_le_add fun ε' hε' hsnetop ↦ ?_

Premises used: ENNReal.le_of_forall_pos_le_add
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
hn : ¬n = 0
neg :
  ∀ (ε' : ℝ≥0) (hε' : 0 < ε') (hsnetop : preVariationFun f (⋃ (i : ℕ), s i) < ∞),
    ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i) + (↑ε' : ℝ≥0∞)
⊢ ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i)

Tactic:
refine ENNReal.le_of_forall_pos_le_add fun ε' hε' hsnetop ↦ ?_

Premises used: ENNReal.le_of_forall_pos_le_add
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
hn : ¬n = 0
ε' : ℝ≥0
hε' : 0 < ε'
hsnetop : preVariationFun f (⋃ (i : ℕ), s i) < ∞
ε : ℝ≥0 := ε' / (↑n : ℝ≥0)
⊢ 0 < ε

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
hn : ¬n = 0
ε' : ℝ≥0
hε' : 0 < ε'
hsnetop : preVariationFun f (⋃ (i : ℕ), s i) < ∞
ε : ℝ≥0 := ε' / (↑n : ℝ≥0)
⊢ 0 < ε

Tactic:
have hε : 0 < ε := by positivity
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
hn : ¬n = 0
ε' : ℝ≥0
hε' : 0 < ε'
hsnetop : preVariationFun f (⋃ (i : ℕ), s i) < ∞
ε : ℝ≥0 := ε' / (↑n : ℝ≥0)
hε : 0 < ε
⊢ ∀ (i : ℕ), preVariationFun f (s i) ≠ ∞

Tactic:
have hs'' i : preVariationFun f (s i) ≠ ⊤ := lt_top_iff_ne_top.mp <|
    (mono f (MeasurableSet.iUnion hs) (Set.subset_iUnion s i)).trans_lt hsnetop
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
hn : ¬n = 0
ε' : ℝ≥0
hε' : 0 < ε'
hsnetop : preVariationFun f (⋃ (i : ℕ), s i) < ∞
ε : ℝ≥0 := ε' / (↑n : ℝ≥0)
hε : 0 < ε
hs'' : ∀ (i : ℕ), preVariationFun f (s i) ≠ ∞
neg :
  ∀ (P : (i : ℕ) → Finpartition (Subtype.mk (p := MeasurableSet) (s i) ⋯))
    (hP : ∀ (i : ℕ), preVariationFun f (s i) ≤ ∑ p ∈ (P i).parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)),
    ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i) + (↑ε' : ℝ≥0∞)
⊢ ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i) + (↑ε' : ℝ≥0∞)

Tactic:
choose P hP using fun i ↦ exists_Finpartition_sum_ge f (hs i) (hε) (hs'' i)

Premises used: MeasureTheory.preVariation.exists_Finpartition_sum_ge
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
hn : ¬n = 0
ε' : ℝ≥0
hε' : 0 < ε'
hsnetop : preVariationFun f (⋃ (i : ℕ), s i) < ∞
ε : ℝ≥0 := ε' / (↑n : ℝ≥0)
hε : 0 < ε
hs'' : ∀ (i : ℕ), preVariationFun f (s i) ≠ ∞
P : (i : ℕ) → Finpartition (Subtype.mk (p := MeasurableSet) (s i) ⋯)
hP : ∀ (i : ℕ), preVariationFun f (s i) ≤ ∑ p ∈ (P i).parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ Finset.range n, preVariationFun f (s i))
    (∑ i ∈ Finset.range n, (∑ p ∈ (P i).parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)))

Tactic:
Finset.sum_le_sum fun i _ => hP i

Premises used: Finset.sum_le_sum
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
n : ℕ
hn : ¬n = 0
ε' : ℝ≥0
hε' : 0 < ε'
hsnetop : preVariationFun f (⋃ (i : ℕ), s i) < ∞
ε : ℝ≥0 := ε' / (↑n : ℝ≥0)
hε : 0 < ε
hs'' : ∀ (i : ℕ), preVariationFun f (s i) ≠ ∞
P : (i : ℕ) → Finpartition (Subtype.mk (p := MeasurableSet) (s i) ⋯)
hP : ∀ (i : ℕ), preVariationFun f (s i) ≤ ∑ p ∈ (P i).parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)
rw :
  HAdd.hAdd (α := ℝ≥0∞) (∑ x ∈ Finset.range n, ∑ p ∈ (P x).parts, f (↑p : Set X)) (∑ x ∈ Finset.range n, (↑ε : ℝ≥0∞)) =
    ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f (↑p : Set X) + (↑ε' : ℝ≥0∞)
⊢ ∑ i ∈ Finset.range n, (∑ p ∈ (P i).parts, f (↑p : Set X) + (↑ε : ℝ≥0∞)) =
    ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f (↑p : Set X) + (↑ε' : ℝ≥0∞)

Tactic:
rw [Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib