awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
h : (μ + ν).real i = (↑(μ.toSignedMeasure + ν.toSignedMeasure) : Set α → ℝ) i
h₁ : μ.real i + ν.real i = (↑(μ.toSignedMeasure + ν.toSignedMeasure) : Set α → ℝ) i
⊢ (↑(μ + ν).toSignedMeasure : Set α → ℝ) i = (↑(μ.toSignedMeasure + ν.toSignedMeasure) : Set α → ℝ) i
have h₂ : μ.real i + ν.real i = (↑μ.toSignedMeasure : Set α → ℝ) i + (↑ν.toSignedMeasure : Set α → ℝ) i
Tactic: rw [toSignedMeasure_apply_measurable hi, measureReal_add_apply,
    VectorMeasure.add_apply, toSignedMeasure_apply_measurable hi,
    toSignedMeasure_apply_measurable hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
h : (μ + ν).real i = (↑(μ.toSignedMeasure + ν.toSignedMeasure) : Set α → ℝ) i
h₁ : μ.real i + ν.real i = (↑(μ.toSignedMeasure + ν.toSignedMeasure) : Set α → ℝ) i
h₂ : μ.real i + ν.real i = (↑μ.toSignedMeasure : Set α → ℝ) i + (↑ν.toSignedMeasure : Set α → ℝ) i
⊢ (↑(μ + ν).toSignedMeasure : Set α → ℝ) i = (↑(μ.toSignedMeasure + ν.toSignedMeasure) : Set α → ℝ) i
have h₃ : μ.real i + ν.real i = μ.real i + (↑ν.toSignedMeasure : Set α → ℝ) i
Tactic: rw [toSignedMeasure_apply_measurable hi, measureReal_add_apply,
    VectorMeasure.add_apply, toSignedMeasure_apply_measurable hi,
    toSignedMeasure_apply_measurable hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
h : (μ + ν).real i = (↑(μ.toSignedMeasure + ν.toSignedMeasure) : Set α → ℝ) i
h₁ : μ.real i + ν.real i = (↑(μ.toSignedMeasure + ν.toSignedMeasure) : Set α → ℝ) i
h₂ : μ.real i + ν.real i = (↑μ.toSignedMeasure : Set α → ℝ) i + (↑ν.toSignedMeasure : Set α → ℝ) i
h₃ : μ.real i + ν.real i = μ.real i + (↑ν.toSignedMeasure : Set α → ℝ) i
⊢ (↑(μ + ν).toSignedMeasure : Set α → ℝ) i = (↑(μ.toSignedMeasure + ν.toSignedMeasure) : Set α → ℝ) i
have h₄ : μ.real i + ν.real i = μ.real i + ν.real i
Tactic: rw [toSignedMeasure_apply_measurable hi, measureReal_add_apply,
    VectorMeasure.add_apply, toSignedMeasure_apply_measurable hi,
    toSignedMeasure_apply_measurable hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
r : ℝ≥0
⊢ (r • μ).toSignedMeasure = r • μ.toSignedMeasure
have h : ∀ (i : Set α) (hi : MeasurableSet i),
  (↑(r • μ).toSignedMeasure : Set α → ℝ) i = (↑(r • μ.toSignedMeasure) : 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 μ
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ (↑(r • μ).toSignedMeasure : Set α → ℝ) i = (↑(r • μ.toSignedMeasure) : Set α → ℝ) i
have h : (↑r : ℝ) * μ.real i = r • μ.real i
Tactic: rw [toSignedMeasure_apply_measurable hi, VectorMeasure.smul_apply,
    toSignedMeasure_apply_measurable hi, measureReal_nnreal_smul_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
x : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (x i)
hf₂ : Pairwise (Disjoint on x)
⊢ HasSum (α := ℝ≥0∞) (fun (i : ℕ) ↦ (if MeasurableSet (x i) then (μ : (a : Set α) → ℝ≥0∞) (x i) else 0 : ℝ≥0∞))
    (if MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), x i) then (μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), x i) else 0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (∑' (b : ℕ), if MeasurableSet (x b) then (μ : (a : Set α) → ℝ≥0∞) (x b) else 0)
  (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (x i))
Tactic: rw [Summable.hasSum_iff ENNReal.summable, if_pos (MeasurableSet.iUnion hf₁),
      MeasureTheory.measure_iUnion hf₂ hf₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := VectorMeasure α ℝ≥0∞) (toENNRealVectorMeasure 0) 0
have h : ∀ (i : Set α), MeasurableSet i → (↑(toENNRealVectorMeasure 0) : Set α → ℝ≥0∞) i = (↑0 : Set α → ℝ≥0∞) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ (μ + ν).toENNRealVectorMeasure = μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure
have refine : ∀ (i : Set α) (hi : MeasurableSet i),
  (↑(μ + ν).toENNRealVectorMeasure : Set α → ℝ≥0∞) i =
    (↑(μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) : Set α → ℝ≥0∞) i
Tactic: refine MeasureTheory.VectorMeasure.ext fun i hi => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
i : Set α
hi : MeasurableSet i
⊢ (↑(μ + ν).toENNRealVectorMeasure : Set α → ℝ≥0∞) i =
    (↑(μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) : Set α → ℝ≥0∞) i
have rw : (μ + ν : (a : Set α) → ℝ≥0∞) i = (↑(μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) : Set α → ℝ≥0∞) i
Tactic: rw [toENNRealVectorMeasure_apply_measurable hi, add_apply, VectorMeasure.add_apply,
    toENNRealVectorMeasure_apply_measurable hi, toENNRealVectorMeasure_apply_measurable hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
i : Set α
hi : MeasurableSet i
rw : (μ + ν : (a : Set α) → ℝ≥0∞) i = (↑(μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) : Set α → ℝ≥0∞) i
⊢ (↑(μ + ν).toENNRealVectorMeasure : Set α → ℝ≥0∞) i =
    (↑(μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) : Set α → ℝ≥0∞) i
have rw₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) =
  (↑(μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) : Set α → ℝ≥0∞) i
Tactic: rw [toENNRealVectorMeasure_apply_measurable hi, add_apply, VectorMeasure.add_apply,
    toENNRealVectorMeasure_apply_measurable hi, toENNRealVectorMeasure_apply_measurable hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
i : Set α
hi : MeasurableSet i
rw : (μ + ν : (a : Set α) → ℝ≥0∞) i = (↑(μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) : Set α → ℝ≥0∞) i
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) =
    (↑(μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) : Set α → ℝ≥0∞) i
⊢ (↑(μ + ν).toENNRealVectorMeasure : Set α → ℝ≥0∞) i =
    (↑(μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) : Set α → ℝ≥0∞) i
have rw₂ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) =
  (↑μ.toENNRealVectorMeasure : Set α → ℝ≥0∞) i + (↑ν.toENNRealVectorMeasure : Set α → ℝ≥0∞) i
Tactic: rw [toENNRealVectorMeasure_apply_measurable hi, add_apply, VectorMeasure.add_apply,
    toENNRealVectorMeasure_apply_measurable hi, toENNRealVectorMeasure_apply_measurable hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
i : Set α
hi : MeasurableSet i
rw : (μ + ν : (a : Set α) → ℝ≥0∞) i = (↑(μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) : Set α → ℝ≥0∞) i
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) =
    (↑(μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) : Set α → ℝ≥0∞) i
rw₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) =
    (↑μ.toENNRealVectorMeasure : Set α → ℝ≥0∞) i + (↑ν.toENNRealVectorMeasure : Set α → ℝ≥0∞) i
⊢ (↑(μ + ν).toENNRealVectorMeasure : Set α → ℝ≥0∞) i =
    (↑(μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) : Set α → ℝ≥0∞) i
have rw₃ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) =
  HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((↑ν.toENNRealVectorMeasure : Set α → ℝ≥0∞) i)
Tactic: rw [toENNRealVectorMeasure_apply_measurable hi, add_apply, VectorMeasure.add_apply,
    toENNRealVectorMeasure_apply_measurable hi, toENNRealVectorMeasure_apply_measurable hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
i : Set α
hi : MeasurableSet i
rw : (μ + ν : (a : Set α) → ℝ≥0∞) i = (↑(μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) : Set α → ℝ≥0∞) i
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) =
    (↑(μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) : Set α → ℝ≥0∞) i
rw₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) =
    (↑μ.toENNRealVectorMeasure : Set α → ℝ≥0∞) i + (↑ν.toENNRealVectorMeasure : Set α → ℝ≥0∞) i
rw₃ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((↑ν.toENNRealVectorMeasure : Set α → ℝ≥0∞) i)
⊢ (↑(μ + ν).toENNRealVectorMeasure : Set α → ℝ≥0∞) i =
    (↑(μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) : Set α → ℝ≥0∞) i
have rw₄ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
Tactic: rw [toENNRealVectorMeasure_apply_measurable hi, add_apply, VectorMeasure.add_apply,
    toENNRealVectorMeasure_apply_measurable hi, toENNRealVectorMeasure_apply_measurable hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
⊢ (↑(μ.toSignedMeasure - ν.toSignedMeasure) : Set α → ℝ) i = μ.real i - ν.real i
have rw : (↑μ.toSignedMeasure : Set α → ℝ) i - (↑ν.toSignedMeasure : Set α → ℝ) i = μ.real i - ν.real i
Tactic: rw [VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
    Measure.toSignedMeasure_apply_measurable hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
rw : (↑μ.toSignedMeasure : Set α → ℝ) i - (↑ν.toSignedMeasure : Set α → ℝ) i = μ.real i - ν.real i
⊢ (↑(μ.toSignedMeasure - ν.toSignedMeasure) : Set α → ℝ) i = μ.real i - ν.real i
have rw₁ : μ.real i - (↑ν.toSignedMeasure : Set α → ℝ) i = μ.real i - ν.real i
Tactic: rw [VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
    Measure.toSignedMeasure_apply_measurable hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
i : Set α
hi : MeasurableSet i
rw : (↑μ.toSignedMeasure : Set α → ℝ) i - (↑ν.toSignedMeasure : Set α → ℝ) i = μ.real i - ν.real i
rw₁ : μ.real i - (↑ν.toSignedMeasure : Set α → ℝ) i = μ.real i - ν.real i
⊢ (↑(μ.toSignedMeasure - ν.toSignedMeasure) : Set α → ℝ) i = μ.real i - ν.real i
have rw₂ : μ.real i - ν.real i = μ.real i - ν.real i
Tactic: rw [VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
    Measure.toSignedMeasure_apply_measurable hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
v : VectorMeasure α ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (v.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s = (↑v : Set α → ℝ≥0∞) s
have rw : ((ofMeasurable (fun (s : Set α) (x : MeasurableSet s) ↦ (↑v : Set α → ℝ≥0∞) s) sorry sorry : Measure α) : (a : Set α) → ℝ≥0∞)
    s =
  (↑v : Set α → ℝ≥0∞) s
Tactic: rw [ennrealToMeasure, ofMeasurable_apply _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
v : VectorMeasure α ℝ≥0∞
s : Set α
hs : MeasurableSet s
rw :
  ((ofMeasurable (fun (s : Set α) (x : MeasurableSet s) ↦ (↑v : Set α → ℝ≥0∞) s) ⋯ ⋯ : Measure α) : (a : Set α) → ℝ≥0∞)
      s =
    (↑v : Set α → ℝ≥0∞) s
⊢ (v.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s = (↑v : Set α → ℝ≥0∞) s
have rw₁ : (↑v : Set α → ℝ≥0∞) s = (↑v : Set α → ℝ≥0∞) s
Tactic: rw [ennrealToMeasure, ofMeasurable_apply _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : VectorMeasure α ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ (↑μ.ennrealToMeasure.toENNRealVectorMeasure : Set α → ℝ≥0∞) s = (↑μ : Set α → ℝ≥0∞) s
have rw : (μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s = (↑μ : Set α → ℝ≥0∞) s
Tactic: rw [toENNRealVectorMeasure_apply_measurable hs, ennrealToMeasure_apply hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : VectorMeasure α ℝ≥0∞
s : Set α
hs : MeasurableSet s
rw : (μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s = (↑μ : Set α → ℝ≥0∞) s
⊢ (↑μ.ennrealToMeasure.toENNRealVectorMeasure : Set α → ℝ≥0∞) s = (↑μ : Set α → ℝ≥0∞) s
have rw₁ : (↑μ : Set α → ℝ≥0∞) s = (↑μ : Set α → ℝ≥0∞) s
Tactic: rw [toENNRealVectorMeasure_apply_measurable hs, ennrealToMeasure_apply hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.toENNRealVectorMeasure.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : (↑μ.toENNRealVectorMeasure : Set α → ℝ≥0∞) s = (μ : (a : Set α) → ℝ≥0∞) s
Tactic: rw [ennrealToMeasure_apply hs, toENNRealVectorMeasure_apply_measurable hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
rw : (↑μ.toENNRealVectorMeasure : Set α → ℝ≥0∞) s = (μ : (a : Set α) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞) ((μ.toENNRealVectorMeasure.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [ennrealToMeasure_apply hs, toENNRealVectorMeasure_apply_measurable hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
v_1 v : VectorMeasure α M
f : α → β
hf : Measurable f
g : ℕ → Set β
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
⊢ HasSum (fun (i : ℕ) ↦ if MeasurableSet (g i) then (↑v : Set α → M) (f ⁻¹' g i) else 0)
    (if MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), g i) then (↑v : Set α → M) (f ⁻¹' ⋃ (i : ℕ), g i) else 0)
have h : ∀ (x : ℕ), (if MeasurableSet (g x) then (↑v : Set α → M) (f ⁻¹' g x) else 0) = (↑v : Set α → M) (f ⁻¹' g x)
Tactic: convert! v.m_iUnion (fun i => hf (hg₁ i)) fun i j hij => (hg₂ hij).preimage _
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
v_1 v : VectorMeasure α M
f : α → β
hf : Measurable f
g : ℕ → Set β
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
h : ∀ (x : ℕ), (if MeasurableSet (g x) then (↑v : Set α → M) (f ⁻¹' g x) else 0) = (↑v : Set α → M) (f ⁻¹' g x)
⊢ HasSum (fun (i : ℕ) ↦ if MeasurableSet (g i) then (↑v : Set α → M) (f ⁻¹' g i) else 0)
    (if MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), g i) then (↑v : Set α → M) (f ⁻¹' ⋃ (i : ℕ), g i) else 0)
have h₁ : (if MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), g i) then (↑v : Set α → M) (f ⁻¹' ⋃ (i : ℕ), g i) else 0) =
  (↑v : Set α → M) (⋃ (i : ℕ), f ⁻¹' g i)
Tactic: convert! v.m_iUnion (fun i => hf (hg₁ i)) fun i j hij => (hg₂ hij).preimage _
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
v_1 v : VectorMeasure α M
f : α → β
hf : Measurable f
g : ℕ → Set β
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
x : ℕ
⊢ (if MeasurableSet (g x) then (↑v : Set α → M) (f ⁻¹' g x) else 0) = (↑v : Set α → M) (f ⁻¹' g x)
have h : (↑v : Set α → M) (f ⁻¹' g x) = (↑v : Set α → M) (f ⁻¹' g x)
Tactic: rw [if_pos (hg₁ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
v_1 v : VectorMeasure α M
f : α → β
hf : Measurable f
g : ℕ → Set β
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
⊢ (if MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), g i) then (↑v : Set α → M) (f ⁻¹' ⋃ (i : ℕ), g i) else 0) =
    (↑v : Set α → M) (⋃ (i : ℕ), f ⁻¹' g i)
have h : (if MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), g i) then (↑v : Set α → M) (⋃ (i : ℕ), f ⁻¹' g i) else 0) =
  (↑v : Set α → M) (⋃ (i : ℕ), f ⁻¹' g i)
Tactic: rw [Set.preimage_iUnion, if_pos (MeasurableSet.iUnion hg₁)]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
v_1 v : VectorMeasure α M
f : α → β
hf : Measurable f
g : ℕ → Set β
hg₁ : ∀ (i : ℕ), MeasurableSet (g i)
hg₂ : Pairwise (Disjoint on g)
h :
  (if MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), g i) then (↑v : Set α → M) (⋃ (i : ℕ), f ⁻¹' g i) else 0) =
    (↑v : Set α → M) (⋃ (i : ℕ), f ⁻¹' g i)
⊢ (if MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), g i) then (↑v : Set α → M) (f ⁻¹' ⋃ (i : ℕ), g i) else 0) =
    (↑v : Set α → M) (⋃ (i : ℕ), f ⁻¹' g i)
have h₁ : (↑v : Set α → M) (⋃ (i : ℕ), f ⁻¹' g i) = (↑v : Set α → M) (⋃ (i : ℕ), f ⁻¹' g i)
Tactic: rw [Set.preimage_iUnion, if_pos (MeasurableSet.iUnion hg₁)]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
v : VectorMeasure α M
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ (↑(v.map f) : Set β → M) s = (↑v : Set α → M) (f ⁻¹' s)
have rw : (↑{ measureOf' := fun (s : Set β) ↦ if MeasurableSet s then (↑v : Set α → M) (f ⁻¹' s) else 0, empty' := sorry,
          not_measurable' := sorry, m_iUnion' := sorry : VectorMeasure β M } :
      Set β → M)
    s =
  (↑v : Set α → M) (f ⁻¹' s)
Tactic: rw [map, dif_pos hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ (↑(v.map id) : Set α → M) i = (↑v : Set α → M) i
have rw : (↑v : Set α → M) (id ⁻¹' i) = (↑v : Set α → M) i
Tactic: rw [map_apply v measurable_id hi, Set.preimage_id]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
M : Type u_3
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
rw : (↑v : Set α → M) (id ⁻¹' i) = (↑v : Set α → M) i
⊢ (↑(v.map id) : Set α → M) i = (↑v : Set α → M) i
have rw₁ : (↑v : Set α → M) i = (↑v : Set α → M) i
Tactic: rw [map_apply v measurable_id hi, Set.preimage_id]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
f : α → β
⊢ Eq (α := VectorMeasure β M) (map 0 f) 0
have pos : ∀ (hf : Measurable f), Eq (α := VectorMeasure β M) (map 0 f) 0
Tactic: by_cases hf : Measurable f
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
f : α → β
pos : ∀ (hf : Measurable f), Eq (α := VectorMeasure β M) (map 0 f) 0
⊢ Eq (α := VectorMeasure β M) (map 0 f) 0
have neg : ∀ (hf : ¬Measurable f), Eq (α := VectorMeasure β M) (map 0 f) 0
Tactic: by_cases hf : Measurable f
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
f : α → β
hf : Measurable f
⊢ Eq (α := VectorMeasure β M) (map 0 f) 0
have pos : ∀ (i : Set β) (hi : MeasurableSet i), Eq.{u_3 + 1} (α := M) ((↑(map 0 f) : 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
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
f : α → β
hf : Measurable f
i : Set β
hi : MeasurableSet i
⊢ Eq.{u_3 + 1} (α := M) ((↑(map 0 f) : Set β → M) i) ((↑0 : Set β → M) i)
have pos : Eq.{u_3 + 1} (α := M) ((↑0 : Set α → M) (f ⁻¹' i)) ((↑0 : Set β → M) i)
Tactic: rw [map_apply _ hf hi, zero_apply, zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
f : α → β
hf : Measurable f
i : Set β
hi : MeasurableSet i
pos : Eq.{u_3 + 1} (α := M) ((↑0 : Set α → M) (f ⁻¹' i)) ((↑0 : Set β → M) i)
⊢ Eq.{u_3 + 1} (α := M) ((↑(map 0 f) : Set β → M) i) ((↑0 : Set β → M) i)
have pos₁ : Eq.{u_3 + 1} (α := M) 0 ((↑0 : Set β → M) i)
Tactic: rw [map_apply _ hf hi, zero_apply, zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
f : α → β
hf : Measurable f
i : Set β
hi : MeasurableSet i
pos : Eq.{u_3 + 1} (α := M) ((↑0 : Set α → M) (f ⁻¹' i)) ((↑0 : Set β → M) i)
pos₁ : Eq.{u_3 + 1} (α := M) 0 ((↑0 : Set β → M) i)
⊢ Eq.{u_3 + 1} (α := M) ((↑(map 0 f) : Set β → M) i) ((↑0 : Set β → M) i)
have pos₂ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [map_apply _ hf hi, zero_apply, zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
v_1 : VectorMeasure α M
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
v : VectorMeasure α M
f : M →+ N
hf : Continuous[inst_3, inst_5] (⇑f : (a : M) → N)
⊢ Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) ((↑v : Set α → M) ∅) : N) (0 : N)
have rw : Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
Tactic: rw [empty, AddMonoidHom.map_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
m inst : MeasurableSpace α
inst_1 : MeasurableSpace β
M : Type u_3
inst_2 : AddCommMonoid M
inst_3 : TopologicalSpace M
v_1 : VectorMeasure α M
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
v : VectorMeasure α M
f : M →+ N
hf : Continuous[inst_3, inst_5] (⇑f : (a : M) → N)
rw : Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) 0 : N) (0 : N)
⊢ Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) ((↑v : Set α → M) ∅) : N) (0 : N)
have rw₁ : Eq.{u_4 + 1} (α := N) 0 0
Tactic: rw [empty, AddMonoidHom.map_zero]