awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m_1 : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst : AddCommMonoid L
inst_1 : TopologicalSpace L
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
⊢ (if MeasurableSet.{u_1} (α := α) ∅ then (↑v : Set α → M) ∅ else 0) = 0
have rw : (↑v : Set α → M) ∅ = 0
Tactic: rw [if_pos (@MeasurableSet.empty _ m), v.empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m_1 : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst : AddCommMonoid L
inst_1 : TopologicalSpace L
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
rw : (↑v : Set α → M) ∅ = 0
⊢ (if MeasurableSet.{u_1} (α := α) ∅ then (↑v : Set α → M) ∅ else 0) = 0
have rw₁ : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [if_pos (@MeasurableSet.empty _ m), v.empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m_1 : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst : AddCommMonoid L
inst_1 : TopologicalSpace L
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : ¬MeasurableSet i
⊢ (if MeasurableSet i then (↑v : Set α → M) i else 0) = 0
have rw : Eq.{u_4 + 1} (α := M) 0 0
Tactic: rw [if_neg hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m_1 : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst : AddCommMonoid L
inst_1 : TopologicalSpace L
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ HasSum (fun (i : ℕ) ↦ if MeasurableSet (f i) then (↑v : Set α → M) (f i) else 0)
    (if MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), f i) then (↑v : Set α → M) (⋃ (i : ℕ), f i) else 0)
have hf₁' : ∀ (k : ℕ), MeasurableSet (f k)
Tactic: have hf₁' : ∀ k, MeasurableSet[n] (f k) := fun k => hle _ (hf₁ k)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m_1 : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst : AddCommMonoid L
inst_1 : TopologicalSpace L
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
hf₁' : ∀ (k : ℕ), MeasurableSet (f k)
⊢ HasSum (fun (i : ℕ) ↦ if MeasurableSet (f i) then (↑v : Set α → M) (f i) else 0)
    (if MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), f i) then (↑v : Set α → M) (⋃ (i : ℕ), f i) else 0)
have h : Eq.{u_4 + 1} (α := ℕ → M) (fun (i : ℕ) ↦ if MeasurableSet (f i) then (↑v : Set α → M) (f i) else 0) fun (i : ℕ) ↦
  (↑v : Set α → M) (f i)
Tactic: convert! v.m_iUnion hf₁' hf₂ using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m_1 : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst : AddCommMonoid L
inst_1 : TopologicalSpace L
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
hf₁' : ∀ (k : ℕ), MeasurableSet (f k)
h :
  Eq.{u_4 + 1} (α := ℕ → M) (fun (i : ℕ) ↦ if MeasurableSet (f i) then (↑v : Set α → M) (f i) else 0) fun (i : ℕ) ↦
    (↑v : Set α → M) (f i)
⊢ HasSum (fun (i : ℕ) ↦ if MeasurableSet (f i) then (↑v : Set α → M) (f i) else 0)
    (if MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), f i) then (↑v : Set α → M) (⋃ (i : ℕ), f i) else 0)
have h₁ : (if MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), f i) then (↑v : Set α → M) (⋃ (i : ℕ), f i) else 0) =
  (↑v : Set α → M) (⋃ (i : ℕ), f i)
Tactic: convert! v.m_iUnion hf₁' hf₂ using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m_1 : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst : AddCommMonoid L
inst_1 : TopologicalSpace L
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
hf₁' : ∀ (k : ℕ), MeasurableSet (f k)
⊢ Eq.{u_4 + 1} (α := ℕ → M) (fun (i : ℕ) ↦ if MeasurableSet (f i) then (↑v : Set α → M) (f i) else 0) fun (i : ℕ) ↦
    (↑v : Set α → M) (f i)
have h : ∀ (n_1 : ℕ), (if MeasurableSet (f n_1) then (↑v : Set α → M) (f n_1) else 0) = (↑v : Set α → M) (f n_1)
Tactic: ext n
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m_1 : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst : AddCommMonoid L
inst_1 : TopologicalSpace L
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
m n_1 : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n_1
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
hf₁' : ∀ (k : ℕ), MeasurableSet (f k)
n : ℕ
⊢ (if MeasurableSet (f n) then (↑v : Set α → M) (f n) else 0) = (↑v : Set α → M) (f n)
have h : (↑v : Set α → M) (f n) = (↑v : Set α → M) (f n)
Tactic: rw [if_pos (hf₁ n)]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m_1 : MeasurableSpace α
L : Type u_3
M : Type u_4
N : Type u_5
inst : AddCommMonoid L
inst_1 : TopologicalSpace L
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
m n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
hf₁' : ∀ (k : ℕ), MeasurableSet (f k)
⊢ (if MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), f i) then (↑v : Set α → M) (⋃ (i : ℕ), f i) else 0) =
    (↑v : Set α → M) (⋃ (i : ℕ), f i)
have h : (↑v : Set α → M) (⋃ (i : ℕ), f i) = (↑v : Set α → M) (⋃ (i : ℕ), f i)
Tactic: rw [if_pos (@MeasurableSet.iUnion _ _ m _ _ hf₁)]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
⊢ v.trim ⋯ = v
have h : ∀ (i : Set α) (hi : MeasurableSet i), (↑(v.trim sorry) : Set α → M) i = (↑v : Set α → M) i
Tactic: ext i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
n : MeasurableSpace α
hle : m ≤ n
⊢ Eq (α := VectorMeasure α M) (trim 0 hle) 0
have h : ∀ (i : Set α) (hi : MeasurableSet i), Eq.{u_4 + 1} (α := M) ((↑(trim 0 hle) : Set α → M) i) ((↑0 : Set α → M) i)
Tactic: ext i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
⊢ (v.trim hle).restrict i = (v.restrict i).trim hle
have h : ∀ (j : Set α) (hj : MeasurableSet j),
  (↑((v.trim hle).restrict i) : Set α → M) j = (↑((v.restrict i).trim hle) : Set α → M) j
Tactic: ext j hj
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
⊢ (↑((v.trim hle).restrict i) : Set α → M) j = (↑((v.restrict i).trim hle) : Set α → M) j
have h : MeasurableSet (j ∩ i)
Tactic: rw [@restrict_apply _ m, trim_measurableSet_eq hle hj, restrict_apply, trim_measurableSet_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
h : MeasurableSet (j ∩ i)
⊢ (↑((v.trim hle).restrict i) : Set α → M) j = (↑((v.restrict i).trim hle) : Set α → M) j
have h₁ : MeasurableSet i
Tactic: rw [@restrict_apply _ m, trim_measurableSet_eq hle hj, restrict_apply, trim_measurableSet_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
n : MeasurableSpace α
v : VectorMeasure α M
hle : m ≤ n
i : Set α
hi : MeasurableSet i
j : Set α
hj : MeasurableSet j
h : MeasurableSet (j ∩ i)
h₁ : MeasurableSet i
⊢ (↑((v.trim hle).restrict i) : Set α → M) j = (↑((v.restrict i).trim hle) : Set α → M) j
have h₂ : MeasurableSet j
Tactic: rw [@restrict_apply _ m, trim_measurableSet_eq hle hj, restrict_apply, trim_measurableSet_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
⊢ Measure α
have refine_1 : s.toMeasureOfZeroLE' i hi₂ ∅ sorry = 0
Tactic: refine Measure.ofMeasurable (s.toMeasureOfZeroLE' i hi₂) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
refine_1 : s.toMeasureOfZeroLE' i hi₂ ∅ ⋯ = 0
⊢ Measure α
have refine_2 : ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
  Pairwise (Disjoint on f) →
    s.toMeasureOfZeroLE' i hi₂ (⋃ (i : ℕ), f i) sorry = ∑' (i_1 : ℕ), s.toMeasureOfZeroLE' i hi₂ (f i_1) sorry
Tactic: refine Measure.ofMeasurable (s.toMeasureOfZeroLE' i hi₂) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
⊢ s.toMeasureOfZeroLE' i hi₂ ∅ ⋯ = 0
have refine_1 : (↑(NNReal.mk 0 sorry) : ℝ≥0∞) = 0
Tactic: simp_rw [toMeasureOfZeroLE', s.restrict_apply hi₁ MeasurableSet.empty, Set.empty_inter i,
      s.empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ s.toMeasureOfZeroLE' i hi₂ (⋃ (i : ℕ), f i) ⋯ = ∑' (i_1 : ℕ), s.toMeasureOfZeroLE' i hi₂ (f i_1) ⋯
have h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
Tactic: have h₁ : ∀ n, MeasurableSet (i ∩ f n) := fun n => hi₁.inter (hf₁ n)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
⊢ s.toMeasureOfZeroLE' i hi₂ (⋃ (i : ℕ), f i) ⋯ = ∑' (i_1 : ℕ), s.toMeasureOfZeroLE' i hi₂ (f i_1) ⋯
have h₂ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ i ∩ f n)
Tactic: have h₂ : Pairwise (Disjoint on fun n : ℕ => i ∩ f n) := by
      intro n m hnm
      exact ((hf₂ hnm).inf_left' i).inf_right' i
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
h₂ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ i ∩ f n)
⊢ s.toMeasureOfZeroLE' i hi₂ (⋃ (i : ℕ), f i) ⋯ = ∑' (i_1 : ℕ), s.toMeasureOfZeroLE' i hi₂ (f i_1) ⋯
have refine_2 : (↑(NNReal.mk (∑' (i_1 : ℕ), (↑s : Set α → ℝ) (i ∩ f i_1)) sorry) : ℝ≥0∞) =
  ∑' (i_1 : ℕ), (↑(NNReal.mk ((↑(VectorMeasure.restrict s i) : Set α → ℝ) (f i_1)) sorry) : ℝ≥0∞)
Tactic: simp only [toMeasureOfZeroLE', s.restrict_apply hi₁ (MeasurableSet.iUnion hf₁), Set.inter_comm,
      Set.inter_iUnion, s.of_disjoint_iUnion h₁ h₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
h₂ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ i ∩ f n)
⊢ (↑(NNReal.mk (∑' (i_1 : ℕ), (↑s : Set α → ℝ) (i ∩ f i_1)) ⋯) : ℝ≥0∞) =
    ∑' (i_1 : ℕ), (↑(NNReal.mk ((↑(VectorMeasure.restrict s i) : Set α → ℝ) (f i_1)) ⋯) : ℝ≥0∞)
have h : ∀ (n : ℕ), 0 ≤ (↑s : Set α → ℝ) (i ∩ f n)
Tactic: have h : ∀ n, 0 ≤ s (i ∩ f n) := fun n =>
      s.nonneg_of_zero_le_restrict (s.zero_le_restrict_subset hi₁ Set.inter_subset_left hi₂)
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
h₂ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ i ∩ f n)
h : ∀ (n : ℕ), 0 ≤ (↑s : Set α → ℝ) (i ∩ f n)
⊢ (↑(NNReal.mk (∑' (i_1 : ℕ), (↑s : Set α → ℝ) (i ∩ f i_1)) ⋯) : ℝ≥0∞) =
    ∑' (i_1 : ℕ), (↑(NNReal.mk ((↑(VectorMeasure.restrict s i) : Set α → ℝ) (f i_1)) ⋯) : ℝ≥0∞)
have refine_2 : Eq (α := ℝ≥0∞) (∑' (a : ℕ), (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ f a)) sorry) : ℝ≥0∞))
  (∑' (i_1 : ℕ), (↑(NNReal.mk ((↑(VectorMeasure.restrict s i) : Set α → ℝ) (f i_1)) sorry) : ℝ≥0∞))
Tactic: rw [NNReal.coe_tsum_of_nonneg h, ENNReal.coe_tsum]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
h₂ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ i ∩ f n)
h : ∀ (n : ℕ), 0 ≤ (↑s : Set α → ℝ) (i ∩ f n)
refine_2 :
  Eq (α := ℝ≥0∞) (∑' (a : ℕ), (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ f a)) ⋯) : ℝ≥0∞))
    (∑' (i_1 : ℕ), (↑(NNReal.mk ((↑(VectorMeasure.restrict s i) : Set α → ℝ) (f i_1)) ⋯) : ℝ≥0∞))
⊢ (↑(NNReal.mk (∑' (i_1 : ℕ), (↑s : Set α → ℝ) (i ∩ f i_1)) ⋯) : ℝ≥0∞) =
    ∑' (i_1 : ℕ), (↑(NNReal.mk ((↑(VectorMeasure.restrict s i) : Set α → ℝ) (f i_1)) ⋯) : ℝ≥0∞)
have refine_2₁ : Summable (α := ℝ≥0) fun (n : ℕ) ↦ NNReal.mk ((↑s : Set α → ℝ) (i ∩ f n)) sorry
Tactic: rw [NNReal.coe_tsum_of_nonneg h, ENNReal.coe_tsum]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
h₂ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ i ∩ f n)
h : ∀ (n : ℕ), 0 ≤ (↑s : Set α → ℝ) (i ∩ f n)
⊢ Eq (α := ℝ≥0∞) (∑' (a : ℕ), (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ f a)) ⋯) : ℝ≥0∞))
    (∑' (i_1 : ℕ), (↑(NNReal.mk ((↑(VectorMeasure.restrict s i) : Set α → ℝ) (f i_1)) ⋯) : ℝ≥0∞))
have refine_2 : ∀ (n : ℕ),
  (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ f n)) sorry) : ℝ≥0∞) =
    (↑(NNReal.mk ((↑(VectorMeasure.restrict s i) : Set α → ℝ) (f n)) sorry) : ℝ≥0∞)
Tactic: refine tsum_congr fun n => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
h₁ : ∀ (n : ℕ), MeasurableSet (i ∩ f n)
h₂ : Pairwise (α := ℕ) (Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint fun (n : ℕ) ↦ i ∩ f n)
h : ∀ (n : ℕ), 0 ≤ (↑s : Set α → ℝ) (i ∩ f n)
n : ℕ
⊢ (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ f n)) ⋯) : ℝ≥0∞) =
    (↑(NNReal.mk ((↑(VectorMeasure.restrict s i) : Set α → ℝ) (f n)) ⋯) : ℝ≥0∞)
have refine_2 : (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ f n)) sorry) : ℝ≥0∞) = (↑(NNReal.mk ((↑s : Set α → ℝ) (f n ∩ i)) sorry) : ℝ≥0∞)
Tactic: simp_rw [s.restrict_apply hi₁ (hf₁ n), Set.inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : 0 ≤[i] s
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ (s.toMeasureOfZeroLE i hi₁ hi : (a : Set α) → ℝ≥0∞) j = (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ j)) ⋯) : ℝ≥0∞)
have simp_rw : (Measure.ofMeasurable (s.toMeasureOfZeroLE' i hi) sorry sorry : (a : Set α) → ℝ≥0∞) j =
  (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ j)) sorry) : ℝ≥0∞)
Tactic: simp_rw [toMeasureOfZeroLE, Measure.ofMeasurable_apply _ hj₁, toMeasureOfZeroLE',
    s.restrict_apply hi₁ hj₁, Set.inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : 0 ≤[i] s
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
simp_rw :
  (Measure.ofMeasurable (s.toMeasureOfZeroLE' i hi) ⋯ ⋯ : (a : Set α) → ℝ≥0∞) j =
    (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ j)) ⋯) : ℝ≥0∞)
⊢ (s.toMeasureOfZeroLE i hi₁ hi : (a : Set α) → ℝ≥0∞) j = (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ j)) ⋯) : ℝ≥0∞)
have simp_rw₁ : s.toMeasureOfZeroLE' i hi j hj₁ = (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ j)) sorry) : ℝ≥0∞)
Tactic: simp_rw [toMeasureOfZeroLE, Measure.ofMeasurable_apply _ hj₁, toMeasureOfZeroLE',
    s.restrict_apply hi₁ hj₁, Set.inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : 0 ≤[i] s
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
simp_rw :
  (Measure.ofMeasurable (s.toMeasureOfZeroLE' i hi) ⋯ ⋯ : (a : Set α) → ℝ≥0∞) j =
    (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ j)) ⋯) : ℝ≥0∞)
simp_rw₁ : s.toMeasureOfZeroLE' i hi j hj₁ = (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ j)) ⋯) : ℝ≥0∞)
⊢ (s.toMeasureOfZeroLE i hi₁ hi : (a : Set α) → ℝ≥0∞) j = (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ j)) ⋯) : ℝ≥0∞)
have simp_rw₂ : (↑(NNReal.mk ((↑(VectorMeasure.restrict s i) : Set α → ℝ) j) sorry) : ℝ≥0∞) =
  (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ j)) sorry) : ℝ≥0∞)
Tactic: simp_rw [toMeasureOfZeroLE, Measure.ofMeasurable_apply _ hj₁, toMeasureOfZeroLE',
    s.restrict_apply hi₁ hj₁, Set.inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : 0 ≤[i] s
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
simp_rw :
  (Measure.ofMeasurable (s.toMeasureOfZeroLE' i hi) ⋯ ⋯ : (a : Set α) → ℝ≥0∞) j =
    (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ j)) ⋯) : ℝ≥0∞)
simp_rw₁ : s.toMeasureOfZeroLE' i hi j hj₁ = (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ j)) ⋯) : ℝ≥0∞)
simp_rw₂ :
  (↑(NNReal.mk ((↑(VectorMeasure.restrict s i) : Set α → ℝ) j) ⋯) : ℝ≥0∞) =
    (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ j)) ⋯) : ℝ≥0∞)
⊢ (s.toMeasureOfZeroLE i hi₁ hi : (a : Set α) → ℝ≥0∞) j = (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ j)) ⋯) : ℝ≥0∞)
have simp_rw₃ : (↑(NNReal.mk ((↑s : Set α → ℝ) (j ∩ i)) sorry) : ℝ≥0∞) = (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ j)) sorry) : ℝ≥0∞)
Tactic: simp_rw [toMeasureOfZeroLE, Measure.ofMeasurable_apply _ hj₁, toMeasureOfZeroLE',
    s.restrict_apply hi₁ hj₁, Set.inter_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : 0 ≤[i] s
hi₁ : MeasurableSet i
⊢ LT.lt (α := ℝ≥0∞) ((s.toMeasureOfZeroLE i hi₁ hi : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ univ)) sorry) : ℝ≥0∞) < ∞
Tactic: rw [toMeasureOfZeroLE_apply s hi hi₁ MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : s ≤[i] 0
hi₁ : MeasurableSet i
⊢ LT.lt (α := ℝ≥0∞) ((s.toMeasureOfLEZero i hi₁ hi : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : (↑(NNReal.mk (-(↑s : Set α → ℝ) (i ∩ univ)) sorry) : ℝ≥0∞) < ∞
Tactic: rw [toMeasureOfLEZero_apply s hi hi₁ MeasurableSet.univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
hs : 0 ≤[univ] s
⊢ (s.toMeasureOfZeroLE univ ⋯ hs).toSignedMeasure = s
have h : ∀ (i : Set α) (hi : MeasurableSet i),
  (↑(s.toMeasureOfZeroLE univ sorry hs).toSignedMeasure : Set α → ℝ) i = (↑s : Set α → ℝ) i
Tactic: ext i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
hs : s ≤[univ] 0
⊢ (s.toMeasureOfLEZero univ ⋯ hs).toSignedMeasure = -s
have h : ∀ (i : Set α) (hi : MeasurableSet i),
  (↑(s.toMeasureOfLEZero univ sorry hs).toSignedMeasure : Set α → ℝ) i = (↑(-s) : Set α → ℝ) i
Tactic: ext i hi
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
⊢ 0 ≤ μ.toSignedMeasure
have rw : 0 ≤[univ] μ.toSignedMeasure
Tactic: rw [← le_restrict_univ_iff_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
⊢ 0 ≤[univ] μ.toSignedMeasure
have refine : ∀ (j : Set α) (hj₁ : MeasurableSet j), j ⊆ univ → (↑0 : Set α → ℝ) j ≤ (↑μ.toSignedMeasure : Set α → ℝ) j
Tactic: refine restrict_le_restrict_of_subset_le _ _ fun j hj₁ _ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
⊢ μ.toSignedMeasure.toMeasureOfZeroLE univ ⋯ ⋯ = μ
have refine : ∀ (i : Set α) (hi : MeasurableSet i),
  Eq (α := ℝ≥0∞) ((μ.toSignedMeasure.toMeasureOfZeroLE univ sorry sorry : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
Tactic: refine Measure.ext fun i hi => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
⊢ Eq (α := ℝ≥0∞) ((μ.toSignedMeasure.toMeasureOfZeroLE univ ⋯ ⋯ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
have lift : ∀ (m_1 : ℝ≥0) (hm : (↑m_1 : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) i),
  (μ.toSignedMeasure.toMeasureOfZeroLE univ sorry sorry : (a : Set α) → ℝ≥0∞) i = (↑m_1 : ℝ≥0∞)
Tactic: lift μ i to ℝ≥0 using (measure_lt_top _ _).ne with m hm
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
m : ℝ≥0
hm : (↑m : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) i
⊢ (μ.toSignedMeasure.toMeasureOfZeroLE univ ⋯ ⋯ : (a : Set α) → ℝ≥0∞) i = (↑m : ℝ≥0∞)
have rw : NNReal.mk ((↑μ.toSignedMeasure : Set α → ℝ) (univ ∩ i)) sorry = m
Tactic: rw [SignedMeasure.toMeasureOfZeroLE_apply _ _ _ hi, ENNReal.coe_inj]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
m : ℝ≥0
hm : (↑m : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) i
⊢ NNReal.mk ((↑μ.toSignedMeasure : Set α → ℝ) (univ ∩ i)) ⋯ = m
have e_x : (↑μ.toSignedMeasure : Set α → ℝ) (univ ∩ i) = (↑m : ℝ)
Tactic: congr