awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : MeasurableSpace β
x_1 : β
v_1 : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
hx : Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x
⊢ MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i)

Tactic:
apply MeasurableSet.iUnion f_meas

Premises used: MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : MeasurableSpace β
x_1 : β
v_1 : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
hx : Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x
⊢ MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i)

Tactic:
have : MeasurableSet (⋃ i, f i) := by
      apply MeasurableSet.iUnion f_meas
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : MeasurableSpace β
x_1 : β
v_1 : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
hx : Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x
this : MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i)
pos : HasSum (fun (i : ℕ) ↦ if x ∈ f i then v else 0) v
⊢ HasSum (fun (i : ℕ) ↦ if MeasurableSet (f i) ∧ x ∈ f i then v else 0)
    (if MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i) ∧ Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x then v else 0)

Tactic:
simp only [f_meas, true_and, MeasurableSet.iUnion f_meas, hx, and_self, ↓reduceIte]

Premises used: and_self, reduceIte, MeasurableSet.iUnion, true_and
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : MeasurableSpace β
x_1 : β
v_1 : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
hx : Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x
this : MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i)
⊢ ∃ (j : ℕ), x ∈ f j

Tactic:
simpa using hx
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : MeasurableSpace β
x_1 : β
v_1 : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
hx : Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x
this : MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i)
pos : ∀ (j : ℕ) (hj : x ∈ f j), HasSum (fun (i : ℕ) ↦ if x ∈ f i then v else 0) v
⊢ HasSum (fun (i : ℕ) ↦ if x ∈ f i then v else 0) v

Tactic:
obtain ⟨j, hj⟩ : ∃ j, x ∈ f j := by simpa using hx
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : MeasurableSpace β
x_1 : β
v_1 : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
hx : Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x
this : MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i)
j : ℕ
hj : x ∈ f j
⊢ v = if x ∈ f j then v else 0

Tactic:
simp [hj]
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : MeasurableSpace β
x_1 : β
v_1 : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
hx : Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x
this : MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i)
j : ℕ
hj : x ∈ f j
pos : HasSum (fun (i : ℕ) ↦ if x ∈ f i then v else 0) (if x ∈ f j then v else 0)
⊢ HasSum (fun (i : ℕ) ↦ if x ∈ f i then v else 0) v

Tactic:
nth_rewrite 2 [show v = if x ∈ f j then v else 0 by simp [hj]]
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : MeasurableSpace β
x_1 : β
v_1 : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
hx : Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x
this : MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i)
j : ℕ
hj : x ∈ f j
pos : ∀ (b' : ℕ), b' ≠ j → (if x ∈ f b' then v else 0) = 0
⊢ HasSum (fun (i : ℕ) ↦ if x ∈ f i then v else 0) (if x ∈ f j then v else 0)

Tactic:
apply hasSum_single

Premises used: hasSum_single, SummationFilter.unconditional
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : MeasurableSpace β
x_1 : β
v_1 : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
hx : Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x
this : MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i)
j : ℕ
hj : x ∈ f j
i : ℕ
hi : i ≠ j
⊢ Disjoint (f i) (f j)

Tactic:
have : Disjoint (f i) (f j) := f_disj hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : MeasurableSpace β
x_1 : β
v_1 : M
s : Set β
x : β
v : M
f : ℕ → Set β
f_meas : ∀ (i : ℕ), MeasurableSet (f i)
f_disj : Pairwise (Disjoint on f)
hx : Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x
this_1 : MeasurableSet.{u_2} (α := β) (⋃ (i : ℕ), f i)
j : ℕ
hj : x ∈ f j
i : ℕ
hi : i ≠ j
this : Disjoint (f i) (f j)
⊢ (if x ∈ f i then v else 0) = 0

Tactic:
grind
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
β : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : MeasurableSpace β
x : β
v : M
s : Set β
hs : MeasurableSet s
hx : x ∈ s
⊢ (↑(dirac x v) : Set β → M) s = v

Tactic:
simp [dirac, hs, hx]

Premises used: MeasureTheory.VectorMeasure.dirac
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
β : Type u_2
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : MeasurableSpace β
x : β
v : M
s : Set β
hx : x ∉ s
⊢ (↑(dirac x v) : Set β → M) s = 0

Tactic:
simp [dirac, hx]

Premises used: MeasureTheory.VectorMeasure.dirac
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
⊢ (if MeasurableSet.{u_1} (α := α) ∅ then μ.real ∅ else 0) = 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
simp :
  HasSum (fun (i : ℕ) ↦ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (f i)))
    (ENNReal.toReal (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (f i)))
⊢ HasSum (fun (i : ℕ) ↦ if MeasurableSet (f i) then μ.real (f i) else 0)
    (if MeasurableSet.{u_1} (α := α) (⋃ (i : ℕ), f i) then μ.real (⋃ (i : ℕ), f i) else 0)

Tactic:
simp only [*, MeasurableSet.iUnion hf₁, if_true, measure_iUnion hf₂ hf₁, measureReal_def]

Premises used: if_true, MeasureTheory.measure_iUnion, MeasureTheory.measureReal_def, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
rw :
  HasSum (α := ℝ) (fun (i : ℕ) ↦ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (f i)))
    (∑' (a : ℕ), ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (f a)))
rw₁ : ∀ (a : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f a) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HasSum (fun (i : ℕ) ↦ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (f i)))
    (ENNReal.toReal (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (f i)))

Tactic:
rw [ENNReal.tsum_toReal_eq]

Premises used: ENNReal.tsum_toReal_eq
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ HasSum (α := ℝ) (fun (i : ℕ) ↦ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (f i)))
    (∑' (a : ℕ), ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (f a)))

Tactic:
(summable_measure_toReal hf₁ hf₂).hasSum

Premises used: MeasureTheory.Measure.real, Summable.hasSum, MeasureTheory.summable_measure_toReal
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ ∀ (a : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f a) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
fun _ ↦ measure_ne_top _ _

Premises used: MeasureTheory.measure_ne_top
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
hμ : IsFiniteMeasure μ
f : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
⊢ HasSum (α := ℝ) (fun (i : ℕ) ↦ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (f i)))
    (∑' (a : ℕ), ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (f a)))

Tactic:
exacts [(summable_measure_toReal hf₁ hf₂).hasSum, fun _ ↦ measure_ne_top _ _]

Premises used: MeasureTheory.measure_ne_top, Summable.hasSum, MeasureTheory.summable_measure_toReal
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
⊢ (↑μ.toSignedMeasure : Set α → ℝ) i = μ.real i

Tactic:
if_pos hi

Premises used: if_pos, ite
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ = ν
⊢ μ.toSignedMeasure = ν.toSignedMeasure

Tactic:
congr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
⊢ μ.toSignedMeasure = ν.toSignedMeasure ↔ μ = ν

Tactic:
⟨fun h => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
refine_1 : ∀ (h : μ.toSignedMeasure = ν.toSignedMeasure), μ = ν
refine_2 : ∀ (h : μ = ν), μ.toSignedMeasure = ν.toSignedMeasure
⊢ μ.toSignedMeasure = ν.toSignedMeasure ↔ μ = ν

Tactic:
refine ⟨fun h => ?_, fun h => ?_⟩
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
refine_1 :
  ∀ (i : Set α) (hi : MeasurableSet i),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
⊢ μ = ν

Tactic:
ext1 i hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
rw rw₁ : (↑ν.toSignedMeasure : Set α → ℝ) i = (↑ν.toSignedMeasure : Set α → ℝ) i
⊢ (↑μ.toSignedMeasure : Set α → ℝ) i = (↑ν.toSignedMeasure : Set α → ℝ) i

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
⊢ (↑μ.toSignedMeasure : Set α → ℝ) i = (↑ν.toSignedMeasure : Set α → ℝ) i

Tactic:
have : μ.toSignedMeasure i = ν.toSignedMeasure i := by rw [h]
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h : μ.toSignedMeasure = ν.toSignedMeasure
i : Set α
hi : MeasurableSet i
this : (↑μ.toSignedMeasure : Set α → ℝ) i = (↑ν.toSignedMeasure : Set α → ℝ) i
refine_1 :
  ∀ (this : μ.real i = (↑ν.toSignedMeasure : Set α → ℝ) i),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
refine_1₁ :
  ∀ (this : μ.real i = ν.real i), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
refine_1₂ refine_1₃ refine_1₄ refine_1₅ :
  ∀ (this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)

Tactic:
rwa [toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi,
        measureReal_eq_measureReal_iff] at this

Premises used: MeasureTheory.measureReal_eq_measureReal_iff, MeasureTheory.Measure.toSignedMeasure_apply_measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
h : ∀ (i : Set α), MeasurableSet i → (↑(toSignedMeasure 0) : Set α → ℝ) i = (↑0 : Set α → ℝ) i
⊢ Eq.{u_1 + 1} (α := SignedMeasure α) (toSignedMeasure 0) 0

Tactic:
ext i
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
i : Set α
h : MeasurableSet i
⊢ (↑(toSignedMeasure 0) : Set α → ℝ) i = (↑0 : Set α → ℝ) i

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
h :
  ∀ (i : Set α) (hi : MeasurableSet i),
    (↑(μ + ν).toSignedMeasure : Set α → ℝ) i = (↑(μ.toSignedMeasure + ν.toSignedMeasure) : Set α → ℝ) i
⊢ (μ + ν).toSignedMeasure = μ.toSignedMeasure + ν.toSignedMeasure

Tactic:
ext i hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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
h₄ h₅ : μ.real i + ν.real i = μ.real i + ν.real i
⊢ (↑(μ + ν).toSignedMeasure : Set α → ℝ) i = (↑(μ.toSignedMeasure + ν.toSignedMeasure) : Set α → ℝ) i

Tactic:
rw [toSignedMeasure_apply_measurable hi, measureReal_add_apply,
    VectorMeasure.add_apply, toSignedMeasure_apply_measurable hi,
    toSignedMeasure_apply_measurable hi]

Premises used: MeasureTheory.measureReal_add_apply, MeasureTheory.Measure.toSignedMeasure_apply_measurable, MeasureTheory.VectorMeasure.add_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
r : ℝ≥0
h :
  ∀ (i : Set α) (hi : MeasurableSet i),
    (↑(r • μ).toSignedMeasure : Set α → ℝ) i = (↑(r • μ.toSignedMeasure) : Set α → ℝ) i
⊢ (r • μ).toSignedMeasure = r • μ.toSignedMeasure

Tactic:
ext i hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
r : ℝ≥0
i : Set α
hi : MeasurableSet i
h : (↑r : ℝ) * μ.real i = r • μ.real i
⊢ (↑(r • μ).toSignedMeasure : Set α → ℝ) i = (↑(r • μ.toSignedMeasure) : Set α → ℝ) i

Tactic:
rw [toSignedMeasure_apply_measurable hi, VectorMeasure.smul_apply,
    toSignedMeasure_apply_measurable hi, measureReal_nnreal_smul_apply]

Premises used: MeasureTheory.VectorMeasure.smul_apply, MeasureTheory.Measure.toSignedMeasure_apply_measurable, MeasureTheory.measureReal_nnreal_smul_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ (↑r : ℝ) * μ.real i = r • μ.real i

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
⊢ Eq (α := ℝ≥0∞) (if MeasurableSet.{u_1} (α := α) ∅ then (μ : (a : Set α) → ℝ≥0∞) ∅ else 0 : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
x : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (x i)
hf₂ : Pairwise (Disjoint on x)
rw :
  Eq (α := ℝ≥0∞) (∑' (b : ℕ), if MeasurableSet (x b) then (μ : (a : Set α) → ℝ≥0∞) (x b) else 0)
    (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (x i))
⊢ 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∞)

Tactic:
rw [Summable.hasSum_iff ENNReal.summable, if_pos (MeasurableSet.iUnion hf₁),
      MeasureTheory.measure_iUnion hf₂ hf₁]

Premises used: ENNReal.summable, if_pos, MeasureTheory.measure_iUnion, Summable.hasSum_iff, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
x : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (x i)
hf₂ : Pairwise (Disjoint on x)
⊢ Eq (α := ℝ≥0∞) (∑' (b : ℕ), if MeasurableSet (x b) then (μ : (a : Set α) → ℝ≥0∞) (x b) else 0)
    (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (x i))

Tactic:
tsum_congr fun n => if_pos (hf₁ n)

Premises used: tsum_congr, if_pos
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
x : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (x i)
hf₂ : Pairwise (Disjoint on x)
⊢ Eq (α := ℝ≥0∞) (∑' (b : ℕ), if MeasurableSet (x b) then (μ : (a : Set α) → ℝ≥0∞) (x b) else 0)
    (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (x i))

Tactic:
exact tsum_congr fun n => if_pos (hf₁ n)

Premises used: tsum_congr, if_pos
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
i : Set α
hi : MeasurableSet i
⊢ (↑μ.toENNRealVectorMeasure : Set α → ℝ≥0∞) i = (μ : (a : Set α) → ℝ≥0∞) i

Tactic:
if_pos hi

Premises used: if_pos, ite
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
h : ∀ (i : Set α), MeasurableSet i → (↑(toENNRealVectorMeasure 0) : Set α → ℝ≥0∞) i = (↑0 : Set α → ℝ≥0∞) i
⊢ Eq.{u_1 + 1} (α := VectorMeasure α ℝ≥0∞) (toENNRealVectorMeasure 0) 0

Tactic:
ext i
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
i : Set α
h : MeasurableSet i
⊢ (↑(toENNRealVectorMeasure 0) : Set α → ℝ≥0∞) i = (↑0 : Set α → ℝ≥0∞) i

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
⊢ (μ + ν).toENNRealVectorMeasure = μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure

Tactic:
MeasureTheory.VectorMeasure.ext fun i hi => ?_

Premises used: MeasureTheory.VectorMeasure.ext
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
refine :
  ∀ (i : Set α) (hi : MeasurableSet i),
    (↑(μ + ν).toENNRealVectorMeasure : Set α → ℝ≥0∞) i =
      (↑(μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure) : Set α → ℝ≥0∞) i
⊢ (μ + ν).toENNRealVectorMeasure = μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure

Tactic:
refine MeasureTheory.VectorMeasure.ext fun i hi => ?_

Premises used: MeasureTheory.VectorMeasure.ext
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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)
rw₄ 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∞)
⊢ (↑(μ + ν).toENNRealVectorMeasure : 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]

Premises used: MeasureTheory.Measure.add_apply, MeasureTheory.VectorMeasure.add_apply, MeasureTheory.Measure.toENNRealVectorMeasure_apply_measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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
rw₂ rw₃ : μ.real i - ν.real i = μ.real i - ν.real i
⊢ (↑(μ.toSignedMeasure - ν.toSignedMeasure) : Set α → ℝ) i = μ.real i - ν.real i

Tactic:
rw [VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi,
    Measure.toSignedMeasure_apply_measurable hi]

Premises used: MeasureTheory.Measure.toSignedMeasure_apply_measurable, MeasureTheory.VectorMeasure.sub_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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
rw₁ rw₂ : (↑v : Set α → ℝ≥0∞) s = (↑v : Set α → ℝ≥0∞) s
⊢ (v.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s = (↑v : Set α → ℝ≥0∞) s

Tactic:
rw [ennrealToMeasure, ofMeasurable_apply _ hs]

Premises used: MeasureTheory.VectorMeasure.ennrealToMeasure, MeasureTheory.Measure.ofMeasurable_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := Measure α) (ennrealToMeasure 0) 0

Tactic:
simp [ennrealToMeasure]

Premises used: MeasureTheory.VectorMeasure.ennrealToMeasure
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : VectorMeasure α ℝ≥0∞
s : Set α
hs : MeasurableSet s
rw : (μ.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s = (↑μ : Set α → ℝ≥0∞) s
rw₁ rw₂ : (↑μ : Set α → ℝ≥0∞) s = (↑μ : Set α → ℝ≥0∞) s
⊢ (↑μ.ennrealToMeasure.toENNRealVectorMeasure : Set α → ℝ≥0∞) s = (↑μ : Set α → ℝ≥0∞) s

Tactic:
rw [toENNRealVectorMeasure_apply_measurable hs, ennrealToMeasure_apply hs]

Premises used: MeasureTheory.VectorMeasure.ennrealToMeasure_apply, MeasureTheory.Measure.toENNRealVectorMeasure_apply_measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
rw : (↑μ.toENNRealVectorMeasure : Set α → ℝ≥0∞) s = (μ : (a : Set α) → ℝ≥0∞) s
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.toENNRealVectorMeasure.ennrealToMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [ennrealToMeasure_apply hs, toENNRealVectorMeasure_apply_measurable hs]

Premises used: MeasureTheory.VectorMeasure.ennrealToMeasure_apply, MeasureTheory.Measure.toENNRealVectorMeasure_apply_measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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
⊢ (if MeasurableSet.{u_2} (α := β) ∅ then (↑v : Set α → M) (f ⁻¹' ∅) else 0) = 0

Tactic:
simp