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 : ∀ (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∞)
norm_cast :
  ∑ x ∈ Finset.range n, ∑ p ∈ (P x).parts, f (↑p : Set X) + (↑(∑ a ∈ Finset.range n, ε) : ℝ≥0∞) =
    ∑ x ∈ Finset.range n, ∑ p ∈ (P x).parts, f (↑p : Set X) + (↑ε' : ℝ≥0∞)
⊢ 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∞)

Tactic:
norm_cast
-- 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∞)
⊢ (↑n : ℝ≥0) * ε = ε'

Tactic:
field
-- 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∞)
⊢ ∑ x ∈ Finset.range n, ∑ p ∈ (P x).parts, f (↑p : Set X) + (↑(∑ a ∈ Finset.range n, ε) : ℝ≥0∞) =
    ∑ x ∈ Finset.range n, ∑ p ∈ (P x).parts, f (↑p : Set X) + (↑ε' : ℝ≥0∞)

Tactic:
simp [show n * ε = ε' by field]
-- 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∞)
bc : ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f (↑p : Set X) ≤ preVariationFun f (⋃ (i : ℕ), s i)
⊢ ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f (↑p : Set X) + (↑ε' : ℝ≥0∞) ≤
    preVariationFun f (⋃ (i : ℕ), s i) + (↑ε' : ℝ≥0∞)

Tactic:
gcongr
-- 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∞)
⊢ ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f (↑p : Set X) ≤ preVariationFun f (⋃ (i : ℕ), s i)

Tactic:
sum_le_preVariationFun_iUnion' f hs hs' P n

Premises used: MeasureTheory.preVariation.sum_le_preVariationFun_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)
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∞)
⊢ ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f (↑p : Set X) ≤ preVariationFun f (⋃ (i : ℕ), s i)

Tactic:
exact sum_le_preVariationFun_iUnion' f hs hs' P n

Premises used: MeasureTheory.preVariation.sum_le_preVariationFun_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)
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∞)
calc :
  ∑ 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∞)
calc₁ :
  ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f (↑p : Set X) + (↑ε' : ℝ≥0∞) ≤
    preVariationFun f (⋃ (i : ℕ), s i) + (↑ε' : ℝ≥0∞)
⊢ ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i) + (↑ε' : ℝ≥0∞)

Tactic:
calc ∑ i ∈ Finset.range n, preVariationFun f (s i)
    _ ≤ ∑ i ∈ Finset.range n, (∑ p ∈ (P i).parts, f p + ε) := Finset.sum_le_sum fun i _ => hP i
    _ = ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f p + ε' := by
      rw [Finset.sum_add_distrib]; norm_cast
      simp [show n * ε = ε' by field]
    _ ≤ preVariationFun f (⋃ i, s i) + ε' := by
      gcongr; exact sum_le_preVariationFun_iUnion' f hs hs' P n

Premises used: Finset.range, MeasureTheory.preVariationFun, Finset.sum_le_sum, Set.iUnion
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
s : ℕ → { t : Set X // MeasurableSet t }
⊢ Pairwise (Disjoint on Subtype.val (p := fun (t : Set X) ↦ MeasurableSet t) ∘ s) →
    LE.le (α := ℝ≥0∞) (0 (⋃ (i : ℕ), (↑(s i) : Set X))) (∑' (i : ℕ), 0 (↑(s i) : Set X))

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
⊢ HasSum (fun (i : ℕ) ↦ preVariationFun f (s i)) (preVariationFun f (⋃ (i : ℕ), s i))

Tactic:
ENNReal.summable.hasSum_iff.mpr (le_antisymm (sum_le_preVariationFun_iUnion f hs hs') ?_)

Premises used: Iff.mpr, ENNReal.summable, le_antisymm, Summable.hasSum_iff, MeasureTheory.preVariation.sum_le_preVariationFun_iUnion
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
refine : preVariationFun f (⋃ (i : ℕ), s i) ≤ ∑' (b : ℕ), preVariationFun f (s b)
⊢ HasSum (fun (i : ℕ) ↦ preVariationFun f (s i)) (preVariationFun f (⋃ (i : ℕ), s i))

Tactic:
refine ENNReal.summable.hasSum_iff.mpr (le_antisymm (sum_le_preVariationFun_iUnion f hs hs') ?_)

Premises used: Iff.mpr, ENNReal.summable, le_antisymm, Summable.hasSum_iff, MeasureTheory.preVariation.sum_le_preVariationFun_iUnion
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
⊢ preVariationFun f (⋃ (i : ℕ), s i) ≤ ∑' (b : ℕ), preVariationFun f (s b)

Tactic:
ENNReal.le_tsum_of_forall_lt_exists_sum fun b hb ↦ ?_

Premises used: ENNReal.le_tsum_of_forall_lt_exists_sum
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
refine :
  ∀ (b : ℝ≥0∞) (hb : b < preVariationFun f (⋃ (i : ℕ), s i)), ∃ (I : Finset ℕ), b < ∑ i ∈ I, preVariationFun f (s i)
⊢ preVariationFun f (⋃ (i : ℕ), s i) ≤ ∑' (b : ℕ), preVariationFun f (s b)

Tactic:
refine ENNReal.le_tsum_of_forall_lt_exists_sum fun b hb ↦ ?_

Premises used: ENNReal.le_tsum_of_forall_lt_exists_sum
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
hb : b < preVariationFun f (⋃ (i : ℕ), s i)
⊢ ∃ (i : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)), b < ∑ p ∈ i.parts, f (↑p : Set X)

Tactic:
simp only [preVariationFun, MeasurableSet.iUnion hs, reduceDIte, lt_iSup_iff] at hb

Premises used: reduceDIte, MeasureTheory.preVariationFun, MeasurableSet.iUnion, lt_iSup_iff
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
hb : ∃ (i : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)), b < ∑ p ∈ i.parts, f (↑p : Set X)
obtain :
  ∀ (Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)) (hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)),
    ∃ (I : Finset ℕ), b < ∑ i ∈ I, preVariationFun f (s i)
⊢ ∃ (I : Finset ℕ), b < ∑ i ∈ I, preVariationFun f (s i)

Tactic:
obtain ⟨Q, hQ⟩ := hb
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
apply :
  ∀ (q : Subtype (α := Set X) MeasurableSet) (hq : q ∈ Q.parts),
    f (↑q : Set X) ≤ ∑' (i : ℕ), f ((↑q : Set X) ⊓ (↑(s' i) : Set X))
⊢ LE.le (α := ℝ≥0∞) (∑ q ∈ Q.parts, f (↑q : Set X)) (∑ q ∈ Q.parts, ∑' (i : ℕ), f ((↑q : Set X) ⊓ (↑(s' i) : Set X)))

Tactic:
apply Finset.sum_le_sum fun q hq => ?_

Premises used: Finset.sum_le_sum
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
q : Subtype (α := Set X) MeasurableSet
hq : q ∈ Q.parts
rw : (↑q : Set X) = (↑q : Set X) ∩ ⋃ (i : ℕ), s i
⊢ (↑q : Set X) = ⋃ (i : ℕ), (↑q : Set X) ∩ s i

Tactic:
rw [← Set.inter_iUnion]

Premises used: Set.inter_iUnion
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
q : Subtype (α := Set X) MeasurableSet
hq : q ∈ Q.parts
⊢ (↑q : Set X) = (↑q : Set X) ∩ ⋃ (i : ℕ), s i

Tactic:
(Set.inter_eq_left.mpr (Q.le hq)).symm

Premises used: Set.inter_eq_left, Iff.mpr, iSup, Finpartition.le, Eq.symm, Set.iUnion
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
q : Subtype (α := Set X) MeasurableSet
hq : q ∈ Q.parts
⊢ (↑q : Set X) = (↑q : Set X) ∩ ⋃ (i : ℕ), s i

Tactic:
exact (Set.inter_eq_left.mpr (Q.le hq)).symm

Premises used: Set.inter_eq_left, Iff.mpr, Finpartition.le, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
q : Subtype (α := Set X) MeasurableSet
hq : q ∈ Q.parts
⊢ (↑q : Set X) = ⋃ (i : ℕ), (↑q : Set X) ∩ s i

Tactic:
have hq_eq : q.val = ⋃ i, q.val ∩ s i := by
            rw [← Set.inter_iUnion]; exact (Set.inter_eq_left.mpr (Q.le hq)).symm
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
q : Subtype (α := Set X) MeasurableSet
hq : q ∈ Q.parts
hq_eq : (↑q : Set X) = ⋃ (i : ℕ), (↑q : Set X) ∩ s i
t : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) ((↑q : Set X) ∩ s i) ⋯
⊢ Pairwise (Disjoint on Subtype.val (p := MeasurableSet) ∘ t)

Tactic:
have ht_disj : Pairwise (Disjoint on (Subtype.val ∘ t)) :=
            fun i j hij => (hs' hij).mono Set.inter_subset_right Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
q : Subtype (α := Set X) MeasurableSet
hq : q ∈ Q.parts
hq_eq : (↑q : Set X) = ⋃ (i : ℕ), (↑q : Set X) ∩ s i
t : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) ((↑q : Set X) ∩ s i) ⋯
ht_disj : Pairwise (Disjoint on Subtype.val (p := MeasurableSet) ∘ t)
⊢ f (↑q : Set X) = f (⋃ (i : ℕ), (↑q : Set X) ∩ s i)

Tactic:
congrArg f hq_eq

Premises used: congrArg
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
q : Subtype (α := Set X) MeasurableSet
hq : q ∈ Q.parts
hq_eq : (↑q : Set X) = ⋃ (i : ℕ), (↑q : Set X) ∩ s i
t : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) ((↑q : Set X) ∩ s i) ⋯
ht_disj : Pairwise (Disjoint on Subtype.val (p := MeasurableSet) ∘ t)
⊢ f (⋃ (i : ℕ), (↑q : Set X) ∩ s i) = f (⋃ (i : ℕ), (↑(t i) : Set X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
q : Subtype (α := Set X) MeasurableSet
hq : q ∈ Q.parts
hq_eq : (↑q : Set X) = ⋃ (i : ℕ), (↑q : Set X) ∩ s i
t : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) ((↑q : Set X) ∩ s i) ⋯
ht_disj : Pairwise (Disjoint on Subtype.val (p := MeasurableSet) ∘ t)
⊢ f (⋃ (i : ℕ), (↑(t i) : Set X)) ≤ ∑' (i : ℕ), f (↑(t i) : Set X)

Tactic:
hf t ht_disj
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
q : Subtype (α := Set X) MeasurableSet
hq : q ∈ Q.parts
hq_eq : (↑q : Set X) = ⋃ (i : ℕ), (↑q : Set X) ∩ s i
t : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) ((↑q : Set X) ∩ s i) ⋯
ht_disj : Pairwise (Disjoint on Subtype.val (p := MeasurableSet) ∘ t)
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), f (↑(t i) : Set X)) (∑' (i : ℕ), f ((↑q : Set X) ⊓ (↑(s' i) : Set X)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
q : Subtype (α := Set X) MeasurableSet
hq : q ∈ Q.parts
hq_eq : (↑q : Set X) = ⋃ (i : ℕ), (↑q : Set X) ∩ s i
t : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) ((↑q : Set X) ∩ s i) ⋯
ht_disj : Pairwise (Disjoint on Subtype.val (p := MeasurableSet) ∘ t)
⊢ f (↑q : Set X) ≤ ∑' (i : ℕ), f ((↑q : Set X) ⊓ (↑(s' i) : Set X))

Tactic:
calc f q
            _ = f (⋃ i, q.val ∩ s i) := congrArg f hq_eq
            _ = f (⋃ i, (t i).val) := rfl
            _ ≤ ∑' i, f (t i) := hf t ht_disj
            _ = ∑' i, f (q ⊓ s' i) := rfl

Premises used: congrArg, Inter.inter, Subtype.val, Set.iUnion, rfl
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
⊢ Eq (α := ℝ≥0∞) (∑ q ∈ Q.parts, ∑' (i : ℕ), f ((↑q : Set X) ⊓ (↑(s' i) : Set X)))
    (∑' (i : ℕ), ∑ q ∈ Q.parts, f ((↑q : Set X) ⊓ (↑(s' i) : Set X)))

Tactic:
(Summable.tsum_finsetSum (fun _ _ ↦ ENNReal.summable)).symm

Premises used: ENNReal.summable, Eq.symm, Summable.tsum_finsetSum
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
e_f :
  Eq (α := ℕ → ℝ≥0∞) (fun (i : ℕ) ↦ ∑ q ∈ Q.parts, f ((↑q : Set X) ⊓ (↑(s' i) : Set X))) fun (i : ℕ) ↦
    ∑ p ∈ (P i).parts, f (↑p : Set X)
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), ∑ q ∈ Q.parts, f ((↑q : Set X) ⊓ (↑(s' i) : Set X)))
    (∑' (i : ℕ), ∑ p ∈ (P i).parts, f (↑p : Set X))

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
e_f :
  ∀ (i : ℕ), Eq (α := ℝ≥0∞) (∑ q ∈ Q.parts, f ((↑q : Set X) ⊓ (↑(s' i) : Set X))) (∑ p ∈ (P i).parts, f (↑p : Set X))
⊢ Eq (α := ℕ → ℝ≥0∞) (fun (i : ℕ) ↦ ∑ q ∈ Q.parts, f ((↑q : Set X) ⊓ (↑(s' i) : Set X))) fun (i : ℕ) ↦
    ∑ p ∈ (P i).parts, f (↑p : Set X)

Tactic:
funext i
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
i : ℕ
⊢ Eq (α := ℝ≥0∞) (∑ q ∈ Q.parts, f ((↑q : Set X) ⊓ (↑(s' i) : Set X))) (∑ p ∈ (P i).parts, f (↑p : Set X))

Tactic:
(Q.sum_restrict _ (fun p => f p) hf').symm

Premises used: Finpartition.sum_restrict, Eq.symm, Subtype.val
-- Module: Mathlib.MeasureTheory.Measure.PreVariation
Goal:
X : Type u_1
inst : MeasurableSpace X
f : Set X → ℝ≥0∞
hf : IsSigmaSubadditiveSetFun f
hf' : f ∅ = 0
s : ℕ → Set X
hs : ∀ (i : ℕ), MeasurableSet (s i)
hs' : Pairwise (Disjoint on s)
b : ℝ≥0∞
Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) ⋯)
hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)
s' : (i : ℕ) → Subtype (α := Set X) MeasurableSet := fun (i : ℕ) ↦ Subtype.mk (p := MeasurableSet) (s i) ⋯
P : (i : ℕ) → Finpartition (s' i) := fun (i : ℕ) ↦ Q.restrict ⋯
i : ℕ
⊢ Eq (α := ℝ≥0∞) (∑ q ∈ Q.parts, f ((↑q : Set X) ⊓ (↑(s' i) : Set X))) (∑ p ∈ (P i).parts, f (↑p : Set X))

Tactic:
exact (Q.sum_restrict _ (fun p => f p) hf').symm

Premises used: Finpartition.sum_restrict, Eq.symm, Subtype.val