awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
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)
have neg : ∀ (ε' : ℝ≥0) (hε' : 0 < ε') (hsnetop : preVariationFun f (⋃ (i : ℕ), s i) < ∞),
  ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i) + (↑ε' : ℝ≥0∞)
Tactic: refine ENNReal.le_of_forall_pos_le_add fun ε' hε' hsnetop ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (hypothesis)
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)
⊢ ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i) + (↑ε' : ℝ≥0∞)
have hε : 0 < ε
Tactic: have hε : 0 < ε := by positivity
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (hypothesis)
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 ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i) + (↑ε' : ℝ≥0∞)
have hs'' : ∀ (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
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) ≠ ∞
⊢ ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i) + (↑ε' : ℝ≥0∞)
have neg : ∀ (P : (i : ℕ) → Finpartition (Subtype.mk (p := MeasurableSet) (s i) sorry))
  (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∞)
Tactic: choose P hP using fun i ↦ exists_Finpartition_sum_ge f (hs i) (hε) (hs'' i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
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) + (↑ε : ℝ≥0∞)) =
    ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f (↑p : Set X) + (↑ε' : ℝ≥0∞)
have 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∞)
Tactic: rw [Finset.sum_add_distrib]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
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∞)
⊢ 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∞)
have 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∞)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
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) + (↑ε' : ℝ≥0∞) ≤
    preVariationFun f (⋃ (i : ℕ), s i) + (↑ε' : ℝ≥0∞)
have bc : ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f (↑p : Set X) ≤ preVariationFun f (⋃ (i : ℕ), s i)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
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, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i) + (↑ε' : ℝ≥0∞)
have 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∞)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
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∞)
⊢ ∑ i ∈ Finset.range n, preVariationFun f (s i) ≤ preVariationFun f (⋃ (i : ℕ), s i) + (↑ε' : ℝ≥0∞)
have calc₁ : ∑ i ∈ Finset.range n, ∑ p ∈ (P i).parts, f (↑p : Set X) + (↑ε' : ℝ≥0∞) ≤
  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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
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))
have refine : preVariationFun f (⋃ (i : ℕ), s i) ≤ ∑' (b : ℕ), preVariationFun f (s b)
Tactic: refine ENNReal.summable.hasSum_iff.mpr (le_antisymm (sum_le_preVariationFun_iUnion f hs hs') ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
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)
have refine : ∀ (b : ℝ≥0∞) (hb : b < preVariationFun f (⋃ (i : ℕ), s i)), ∃ (I : Finset ℕ), b < ∑ i ∈ I, preVariationFun f (s i)
Tactic: refine ENNReal.le_tsum_of_forall_lt_exists_sum fun b hb ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (hypothesis)
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 : Finset ℕ), b < ∑ i ∈ I, preVariationFun f (s i)
have hb₁ : ∃ (i : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) sorry)), b < ∑ p ∈ i.parts, f (↑p : Set X)
Tactic: simp only [preVariationFun, MeasurableSet.iUnion hs, reduceDIte, lt_iSup_iff] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
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)
⊢ ∃ (I : Finset ℕ), b < ∑ i ∈ I, preVariationFun f (s i)
have obtain : ∀ (Q : Finpartition (Subtype.mk (p := MeasurableSet) (⋃ (i : ℕ), s i) sorry)) (hQ : b < ∑ p ∈ Q.parts, f (↑p : Set X)),
  ∃ (I : Finset ℕ), b < ∑ i ∈ I, preVariationFun f (s i)
Tactic: obtain ⟨Q, hQ⟩ := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
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 ⋯
⊢ LE.le (α := ℝ≥0∞) (∑ q ∈ Q.parts, f (↑q : Set X)) (∑ q ∈ Q.parts, ∑' (i : ℕ), f ((↑q : Set X) ⊓ (↑(s' i) : Set X)))
have apply : ∀ (q : Subtype (α := Set X) MeasurableSet) (hq : q ∈ Q.parts),
  f (↑q : Set X) ≤ ∑' (i : ℕ), f ((↑q : Set X) ⊓ (↑(s' i) : Set X))
Tactic: apply Finset.sum_le_sum fun q hq => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
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
have rw : (↑q : Set X) = (↑q : Set X) ∩ ⋃ (i : ℕ), s i
Tactic: rw [← Set.inter_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (hypothesis)
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
⊢ f (↑q : Set X) ≤ ∑' (i : ℕ), f ((↑q : Set X) ⊓ (↑(s' i) : Set X))
have hq_eq : (↑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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (hypothesis)
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) ⋯
⊢ f (↑q : Set X) ≤ ∑' (i : ℕ), f ((↑q : Set X) ⊓ (↑(s' i) : Set X))
have ht_disj : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
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∞) (∑' (i : ℕ), ∑ q ∈ Q.parts, f ((↑q : Set X) ⊓ (↑(s' i) : Set X)))
    (∑' (i : ℕ), ∑ p ∈ (P i).parts, f (↑p : Set X))
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
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∞) (fun (i : ℕ) ↦ ∑ q ∈ Q.parts, f ((↑q : Set X) ⊓ (↑(s' i) : Set X))) fun (i : ℕ) ↦
    ∑ p ∈ (P i).parts, f (↑p : Set X)
have e_f : ∀ (i : ℕ), Eq (α := ℝ≥0∞) (∑ q ∈ Q.parts, f ((↑q : Set X) ⊓ (↑(s' i) : Set X))) (∑ p ∈ (P i).parts, f (↑p : Set X))
Tactic: funext i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
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 ⋯
⊢ LE.le (α := ℝ≥0∞) (∑ q ∈ Q.parts, f (↑q : Set X)) (∑' (i : ℕ), ∑ p ∈ (P i).parts, f (↑p : Set X))
have calc : LE.le (α := ℝ≥0∞) (∑ q ∈ Q.parts, f (↑q : Set X)) (∑ q ∈ Q.parts, ∑' (i : ℕ), f ((↑q : Set X) ⊓ (↑(s' i) : Set X)))
Tactic: calc ∑ q ∈ Q.parts, f q
      _ ≤ ∑ q ∈ Q.parts, ∑' i, f (q ⊓ s' i) := by
          apply Finset.sum_le_sum fun q hq => ?_
          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
          let t (i : ℕ) : Subtype MeasurableSet := ⟨q.val ∩ s i, q.2.inter (hs i)⟩
          have ht_disj : Pairwise (Disjoint on (Subtype.val ∘ t)) :=
            fun i j hij => (hs' hij).mono Set.inter_subset_right Set.inter_subset_right
          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
      _ = ∑' i, ∑ q ∈ Q.parts, f (q ⊓ s' i) :=
          (Summable.tsum_finsetSum (fun _ _ ↦ ENNReal.summable)).symm
      _ = ∑' i, ∑ p ∈ (P i).parts, f p := by
          congr 1; funext i
          exact (Q.sum_restrict _ (fun p => f p) hf').symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
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 ⋯
calc :
  LE.le (α := ℝ≥0∞) (∑ q ∈ Q.parts, f (↑q : Set X)) (∑ q ∈ Q.parts, ∑' (i : ℕ), f ((↑q : Set X) ⊓ (↑(s' i) : Set X)))
⊢ LE.le (α := ℝ≥0∞) (∑ q ∈ Q.parts, f (↑q : Set X)) (∑' (i : ℕ), ∑ p ∈ (P i).parts, f (↑p : Set X))
have calc₁ : Eq (α := ℝ≥0∞) (∑' (i : ℕ), ∑ q ∈ Q.parts, f ((↑q : Set X) ⊓ (↑(s' i) : Set X)))
  (∑' (i : ℕ), ∑ p ∈ (P i).parts, f (↑p : Set X))
Tactic: calc ∑ q ∈ Q.parts, f q
      _ ≤ ∑ q ∈ Q.parts, ∑' i, f (q ⊓ s' i) := by
          apply Finset.sum_le_sum fun q hq => ?_
          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
          let t (i : ℕ) : Subtype MeasurableSet := ⟨q.val ∩ s i, q.2.inter (hs i)⟩
          have ht_disj : Pairwise (Disjoint on (Subtype.val ∘ t)) :=
            fun i j hij => (hs' hij).mono Set.inter_subset_right Set.inter_subset_right
          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
      _ = ∑' i, ∑ q ∈ Q.parts, f (q ⊓ s' i) :=
          (Summable.tsum_finsetSum (fun _ _ ↦ ENNReal.summable)).symm
      _ = ∑' i, ∑ p ∈ (P i).parts, f p := by
          congr 1; funext i
          exact (Q.sum_restrict _ (fun p => f p) hf').symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (hypothesis)
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 : Finset ℕ), b < ∑ i ∈ I, preVariationFun f (s i)
have splitting : LE.le (α := ℝ≥0∞) (∑ q ∈ Q.parts, f (↑q : Set X)) (∑' (i : ℕ), ∑ p ∈ (P i).parts, f (↑p : Set X))
Tactic: have splitting : ∑ q ∈ Q.parts, f q ≤ ∑' i, ∑ p ∈ (P i).parts, f p := by
    calc ∑ q ∈ Q.parts, f q
      _ ≤ ∑ q ∈ Q.parts, ∑' i, f (q ⊓ s' i) := by
          apply Finset.sum_le_sum fun q hq => ?_
          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
          let t (i : ℕ) : Subtype MeasurableSet := ⟨q.val ∩ s i, q.2.inter (hs i)⟩
          have ht_disj : Pairwise (Disjoint on (Subtype.val ∘ t)) :=
            fun i j hij => (hs' hij).mono Set.inter_subset_right Set.inter_subset_right
          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
      _ = ∑' i, ∑ q ∈ Q.parts, f (q ⊓ s' i) :=
          (Summable.tsum_finsetSum (fun _ _ ↦ ENNReal.summable)).symm
      _ = ∑' i, ∑ p ∈ (P i).parts, f p := by
          congr 1; funext i
          exact (Q.sum_restrict _ (fun p => f p) hf').symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
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 ⋯
splitting : LE.le (α := ℝ≥0∞) (∑ q ∈ Q.parts, f (↑q : Set X)) (∑' (i : ℕ), ∑ p ∈ (P i).parts, f (↑p : Set X))
⊢ ∃ (I : Finset ℕ), b < ∑ i ∈ I, preVariationFun f (s i)
have obtain : ∀ (n : ℕ) (hn : b < ∑ a ∈ Finset.range n, ∑ p ∈ (P a).parts, f (↑p : Set X)),
  ∃ (I : Finset ℕ), b < ∑ i ∈ I, preVariationFun f (s i)
Tactic: obtain ⟨n, hn⟩ := lt_iSup_iff.mp <| ENNReal.tsum_eq_iSup_nat ▸ lt_of_lt_of_le hQ splitting
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (hypothesis)
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 ⋯
splitting : LE.le (α := ℝ≥0∞) (∑ q ∈ Q.parts, f (↑q : Set X)) (∑' (i : ℕ), ∑ p ∈ (P i).parts, f (↑p : Set X))
n : ℕ
hn : b < ∑ a ∈ Finset.range n, ∑ p ∈ (P a).parts, f (↑p : Set X)
⊢ ∃ (I : Finset ℕ), b < ∑ i ∈ I, preVariationFun f (s i)
have bound : ∀ (i : ℕ), ∑ p ∈ (P i).parts, f (↑p : Set X) ≤ preVariationFun f (s i)
Tactic: have bound (i : ℕ) : ∑ p ∈ (P i).parts, f p ≤ preVariationFun f (s i) := sum_le f (hs i) (P i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
⊢ Eq.{u_1 + 1} (α := VectorMeasure X ℝ≥0∞) (ennrealPreVariation 0 ⋯ ⋯) 0
have h : ∀ (i : Set X), MeasurableSet i → (↑(ennrealPreVariation 0 sorry sorry) : Set X → ℝ≥0∞) i = (↑0 : Set X → ℝ≥0∞) i
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.PreVariation (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
⊢ Eq.{u_1 + 1} (α := Measure X) (preVariation 0 ⋯ ⋯) 0
have h : ∀ (s : Set X),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) (((preVariation 0 sorry sorry : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
      (((0 : Measure X) : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ProbabilityMeasure (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
ν : ProbabilityMeasure Ω
s : Set Ω
⊢ (↑((ν : (a : Set Ω) → ℝ≥0) s) : ℝ≥0∞) = ((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s
have rw : (↑((ν.toFiniteMeasure : (a : Set Ω) → ℝ≥0) s) : ℝ≥0∞) = ((↑ν : Measure Ω) : (a : Set Ω) → ℝ≥0∞) s
Tactic: rw [← coeFn_comp_toFiniteMeasure_eq_coeFn, FiniteMeasure.ennreal_coeFn_eq_coeFn_toMeasure,
    toMeasure_comp_toFiniteMeasure_eq_toMeasure]