awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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
⊢ MeasurableSet i

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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
⊢ MeasurableSet j

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi : 0 ≤[i] s
j : Set α
hj : MeasurableSet j
⊢ LE.le (α := ℝ) 0 ((↑(VectorMeasure.restrict 0 i) : Set α → ℝ) j)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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
refine_2 :
  ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      s.toMeasureOfZeroLE' i hi₂ (⋃ (i : ℕ), f i) ⋯ = ∑' (i_1 : ℕ), s.toMeasureOfZeroLE' i hi₂ (f i_1) ⋯
⊢ Measure α

Tactic:
refine Measure.ofMeasurable (s.toMeasureOfZeroLE' i hi₂) ?_ ?_

Premises used: MeasureTheory.Measure.ofMeasurable, MeasureTheory.SignedMeasure.toMeasureOfZeroLE'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
refine_1 : (↑(NNReal.mk 0 ⋯) : ℝ≥0∞) = 0
⊢ s.toMeasureOfZeroLE' i hi₂ ∅ ⋯ = 0

Tactic:
simp_rw [toMeasureOfZeroLE', s.restrict_apply hi₁ MeasurableSet.empty, Set.empty_inter i,
      s.empty]

Premises used: MeasureTheory.VectorMeasure.empty, MeasurableSet.empty, MeasureTheory.VectorMeasure.restrict_apply, Set.empty_inter, MeasureTheory.SignedMeasure.toMeasureOfZeroLE'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i : Set α
hi₁ : MeasurableSet i
hi₂ : 0 ≤[i] s
⊢ (↑(NNReal.mk 0 ⋯) : ℝ≥0∞) = 0

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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)
⊢ ∀ (n : ℕ), MeasurableSet (i ∩ f n)

Tactic:
have h₁ : ∀ n, MeasurableSet (i ∩ f n) := fun n => hi₁.inter (hf₁ n)
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m_1 : 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)
n m : ℕ
hnm : n ≠ m
⊢ Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint (fun (n : ℕ) ↦ i ∩ f n) n m

Tactic:
((hf₂ hnm).inf_left' i).inf_right' i

Premises used: Disjoint.inf_right', Disjoint.inf_left'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m_1 : 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)
n m : ℕ
hnm : n ≠ m
⊢ Function.onFun.{1, u_1 + 1, 1} (β := Set α) Disjoint (fun (n : ℕ) ↦ i ∩ f n) n m

Tactic:
exact ((hf₂ hnm).inf_left' i).inf_right' i

Premises used: Disjoint.inf_right', Disjoint.inf_left'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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)
⊢ 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
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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)
refine_2 :
  (↑(NNReal.mk (∑' (i_1 : ℕ), (↑s : Set α → ℝ) (i ∩ f i_1)) ⋯) : ℝ≥0∞) =
    ∑' (i_1 : ℕ), (↑(NNReal.mk ((↑(VectorMeasure.restrict s i) : Set α → ℝ) (f i_1)) ⋯) : ℝ≥0∞)
⊢ s.toMeasureOfZeroLE' i hi₂ (⋃ (i : ℕ), f i) ⋯ = ∑' (i_1 : ℕ), s.toMeasureOfZeroLE' i hi₂ (f i_1) ⋯

Tactic:
simp only [toMeasureOfZeroLE', s.restrict_apply hi₁ (MeasurableSet.iUnion hf₁), Set.inter_comm,
      Set.inter_iUnion, s.of_disjoint_iUnion h₁ h₂]

Premises used: MeasureTheory.VectorMeasure.restrict_apply, MeasureTheory.VectorMeasure.of_disjoint_iUnion, Set.inter_comm, Set.inter_iUnion, MeasurableSet.iUnion, MeasureTheory.SignedMeasure.toMeasureOfZeroLE'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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)
⊢ ∀ (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₂)
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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∞))
refine_2₁ : Summable (α := ℝ≥0) fun (n : ℕ) ↦ NNReal.mk ((↑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∞)

Tactic:
rw [NNReal.coe_tsum_of_nonneg h, ENNReal.coe_tsum]

Premises used: ENNReal.coe_tsum, NNReal.coe_tsum_of_nonneg
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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∞))

Tactic:
tsum_congr fun n => ?_

Premises used: tsum_congr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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 :
  ∀ (n : ℕ),
    (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ f n)) ⋯) : ℝ≥0∞) =
      (↑(NNReal.mk ((↑(VectorMeasure.restrict s i) : Set α → ℝ) (f n)) ⋯) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∑' (a : ℕ), (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ f a)) ⋯) : ℝ≥0∞))
    (∑' (i_1 : ℕ), (↑(NNReal.mk ((↑(VectorMeasure.restrict s i) : Set α → ℝ) (f i_1)) ⋯) : ℝ≥0∞))

Tactic:
refine tsum_congr fun n => ?_

Premises used: tsum_congr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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 : ℕ
refine_2 : (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ f n)) ⋯) : ℝ≥0∞) = (↑(NNReal.mk ((↑s : Set α → ℝ) (f n ∩ i)) ⋯) : ℝ≥0∞)
⊢ (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ f n)) ⋯) : ℝ≥0∞) =
    (↑(NNReal.mk ((↑(VectorMeasure.restrict s i) : Set α → ℝ) (f n)) ⋯) : ℝ≥0∞)

Tactic:
simp_rw [s.restrict_apply hi₁ (hf₁ n), Set.inter_comm]

Premises used: MeasureTheory.VectorMeasure.restrict_apply, Set.inter_comm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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)
⊢ Summable (α := ℝ≥0) fun (n : ℕ) ↦ NNReal.mk ((↑s : Set α → ℝ) (i ∩ f n)) ⋯

Tactic:
(NNReal.summable_mk h).2 (s.m_iUnion h₁ h₂).summable

Premises used: Iff.mpr, NNReal.mk, NNReal, HasSum.summable, NNReal.summable_mk, MeasureTheory.VectorMeasure.m_iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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)
⊢ Summable (α := ℝ≥0) fun (n : ℕ) ↦ NNReal.mk ((↑s : Set α → ℝ) (i ∩ f n)) ⋯

Tactic:
exact (NNReal.summable_mk h).2 (s.m_iUnion h₁ h₂).summable

Premises used: Iff.mpr, HasSum.summable, NNReal.summable_mk, MeasureTheory.VectorMeasure.m_iUnion
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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∞)
simp_rw₃ : (↑(NNReal.mk ((↑s : Set α → ℝ) (j ∩ i)) ⋯) : ℝ≥0∞) = (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ j)) ⋯) : ℝ≥0∞)
⊢ (s.toMeasureOfZeroLE i hi₁ hi : (a : Set α) → ℝ≥0∞) j = (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ j)) ⋯) : ℝ≥0∞)

Tactic:
simp_rw [toMeasureOfZeroLE, Measure.ofMeasurable_apply _ hj₁, toMeasureOfZeroLE',
    s.restrict_apply hi₁ hj₁, Set.inter_comm]

Premises used: MeasureTheory.VectorMeasure.restrict_apply, MeasureTheory.SignedMeasure.toMeasureOfZeroLE, Set.inter_comm, MeasureTheory.Measure.ofMeasurable_apply, MeasureTheory.SignedMeasure.toMeasureOfZeroLE'
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : s ≤[i] 0
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ (s.toMeasureOfLEZero i hi₁ hi : (a : Set α) → ℝ≥0∞) j = (↑(NNReal.mk (-(↑s : Set α → ℝ) (i ∩ j)) ⋯) : ℝ≥0∞)

Tactic:
simp [toMeasureOfLEZero, toMeasureOfZeroLE_apply _ _ _ hj₁]

Premises used: MeasureTheory.SignedMeasure.toMeasureOfZeroLE_apply, MeasureTheory.SignedMeasure.toMeasureOfLEZero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : s ≤[i] 0
hi₁ : MeasurableSet i
hj₁ : MeasurableSet j
⊢ (s.toMeasureOfLEZero i hi₁ hi).real j = -(↑s : Set α → ℝ) (i ∩ j)

Tactic:
simp [measureReal_def, toMeasureOfLEZero_apply _ hi hi₁ hj₁]

Premises used: MeasureTheory.SignedMeasure.toMeasureOfLEZero_apply, MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : 0 ≤[i] s
hi₁ : MeasurableSet i
rw : (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ univ)) ⋯) : ℝ≥0∞) < ∞
⊢ LT.lt (α := ℝ≥0∞) ((s.toMeasureOfZeroLE i hi₁ hi : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [toMeasureOfZeroLE_apply s hi hi₁ MeasurableSet.univ]

Premises used: MeasureTheory.SignedMeasure.toMeasureOfZeroLE_apply, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : 0 ≤[i] s
hi₁ : MeasurableSet i
⊢ (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ univ)) ⋯) : ℝ≥0∞) < ∞

Tactic:
ENNReal.coe_lt_top

Premises used: ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : 0 ≤[i] s
hi₁ : MeasurableSet i
⊢ (↑(NNReal.mk ((↑s : Set α → ℝ) (i ∩ univ)) ⋯) : ℝ≥0∞) < ∞

Tactic:
exact ENNReal.coe_lt_top

Premises used: ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : s ≤[i] 0
hi₁ : MeasurableSet i
rw : (↑(NNReal.mk (-(↑s : Set α → ℝ) (i ∩ univ)) ⋯) : ℝ≥0∞) < ∞
⊢ LT.lt (α := ℝ≥0∞) ((s.toMeasureOfLEZero i hi₁ hi : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [toMeasureOfLEZero_apply s hi hi₁ MeasurableSet.univ]

Premises used: MeasureTheory.SignedMeasure.toMeasureOfLEZero_apply, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : s ≤[i] 0
hi₁ : MeasurableSet i
⊢ (↑(NNReal.mk (-(↑s : Set α → ℝ) (i ∩ univ)) ⋯) : ℝ≥0∞) < ∞

Tactic:
ENNReal.coe_lt_top

Premises used: ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
s : SignedMeasure α
i j : Set α
hi : s ≤[i] 0
hi₁ : MeasurableSet i
⊢ (↑(NNReal.mk (-(↑s : Set α → ℝ) (i ∩ univ)) ⋯) : ℝ≥0∞) < ∞

Tactic:
exact ENNReal.coe_lt_top

Premises used: ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
hs : 0 ≤[univ] s
h :
  ∀ (i : Set α) (hi : MeasurableSet i),
    (↑(s.toMeasureOfZeroLE univ ⋯ hs).toSignedMeasure : Set α → ℝ) i = (↑s : Set α → ℝ) i
⊢ (s.toMeasureOfZeroLE univ ⋯ hs).toSignedMeasure = s

Tactic:
ext i hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
hs : 0 ≤[univ] s
i : Set α
hi : MeasurableSet i
⊢ (↑(s.toMeasureOfZeroLE univ ⋯ hs).toSignedMeasure : Set α → ℝ) i = (↑s : Set α → ℝ) i

Tactic:
simp [hi, toMeasureOfZeroLE_apply _ _ _ hi, measureReal_def]

Premises used: MeasureTheory.SignedMeasure.toMeasureOfZeroLE_apply, MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
hs : s ≤[univ] 0
h :
  ∀ (i : Set α) (hi : MeasurableSet i),
    (↑(s.toMeasureOfLEZero univ ⋯ hs).toSignedMeasure : Set α → ℝ) i = (↑(-s) : Set α → ℝ) i
⊢ (s.toMeasureOfLEZero univ ⋯ hs).toSignedMeasure = -s

Tactic:
ext i hi
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
hs : s ≤[univ] 0
i : Set α
hi : MeasurableSet i
⊢ (↑(s.toMeasureOfLEZero univ ⋯ hs).toSignedMeasure : Set α → ℝ) i = (↑(-s) : Set α → ℝ) i

Tactic:
simp [hi, toMeasureOfLEZero_apply _ _ _ hi, measureReal_def]

Premises used: MeasureTheory.SignedMeasure.toMeasureOfLEZero_apply, MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
rw : 0 ≤[univ] μ.toSignedMeasure
⊢ 0 ≤ μ.toSignedMeasure

Tactic:
rw [← le_restrict_univ_iff_le]

Premises used: MeasureTheory.VectorMeasure.le_restrict_univ_iff_le
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
⊢ 0 ≤[univ] μ.toSignedMeasure

Tactic:
restrict_le_restrict_of_subset_le _ _ fun j hj₁ _ => ?_

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_of_subset_le
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
refine : ∀ (j : Set α) (hj₁ : MeasurableSet j), j ⊆ univ → (↑0 : Set α → ℝ) j ≤ (↑μ.toSignedMeasure : Set α → ℝ) j
⊢ 0 ≤[univ] μ.toSignedMeasure

Tactic:
refine restrict_le_restrict_of_subset_le _ _ fun j hj₁ _ => ?_

Premises used: MeasureTheory.VectorMeasure.restrict_le_restrict_of_subset_le
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
j : Set α
hj₁ : MeasurableSet j
h : j ⊆ univ
⊢ (↑0 : Set α → ℝ) j ≤ (↑μ.toSignedMeasure : Set α → ℝ) j

Tactic:
simp only [VectorMeasure.coe_zero, Pi.zero_apply, Measure.toSignedMeasure_apply_measurable hj₁,
    measureReal_nonneg]

Premises used: MeasureTheory.VectorMeasure.coe_zero, MeasureTheory.measureReal_nonneg, Pi.zero_apply, MeasureTheory.Measure.toSignedMeasure_apply_measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
⊢ μ.toSignedMeasure.toMeasureOfZeroLE univ ⋯ ⋯ = μ

Tactic:
Measure.ext fun i hi => ?_

Premises used: MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
refine :
  ∀ (i : Set α) (hi : MeasurableSet i),
    Eq (α := ℝ≥0∞) ((μ.toSignedMeasure.toMeasureOfZeroLE univ ⋯ ⋯ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
⊢ μ.toSignedMeasure.toMeasureOfZeroLE univ ⋯ ⋯ = μ

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

Premises used: MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(measure_lt_top _ _).ne

Premises used: MeasureTheory.measure_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
lift :
  ∀ (m_1 : ℝ≥0) (hm : (↑m_1 : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) i),
    (μ.toSignedMeasure.toMeasureOfZeroLE univ ⋯ ⋯ : (a : Set α) → ℝ≥0∞) i = (↑m_1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ.toSignedMeasure.toMeasureOfZeroLE univ ⋯ ⋯ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞)

Tactic:
lift μ i to ℝ≥0 using (measure_lt_top _ _).ne with m hm

Premises used: MeasureTheory.measure_lt_top, DFunLike.coe, LT.lt.ne
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
m : ℝ≥0
hm : (↑m : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) i
rw : NNReal.mk ((↑μ.toSignedMeasure : Set α → ℝ) (univ ∩ i)) ⋯ = m
⊢ (μ.toSignedMeasure.toMeasureOfZeroLE univ ⋯ ⋯ : (a : Set α) → ℝ≥0∞) i = (↑m : ℝ≥0∞)

Tactic:
rw [SignedMeasure.toMeasureOfZeroLE_apply _ _ _ hi, ENNReal.coe_inj]

Premises used: MeasureTheory.SignedMeasure.toMeasureOfZeroLE_apply, ENNReal.coe_inj
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m_1 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
i : Set α
hi : MeasurableSet i
m : ℝ≥0
hm : (↑m : ℝ≥0∞) = (μ : (a : Set α) → ℝ≥0∞) i
e_x : (↑μ.toSignedMeasure : Set α → ℝ) (univ ∩ i) = (↑m : ℝ)
⊢ NNReal.mk ((↑μ.toSignedMeasure : Set α → ℝ) (univ ∩ i)) ⋯ = m

Tactic:
congr
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
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 : Set α → ℝ) (univ ∩ i) = (↑m : ℝ)

Tactic:
simp [hi, ← hm, measureReal_def]

Premises used: MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Set α
hs : MeasurableSet s
h :
  ∀ (A : Set α) (hA : MeasurableSet A),
    (↑(VectorMeasure.restrict μ.toSignedMeasure s) : Set α → ℝ) A = (↑(μ.restrict s).toSignedMeasure : Set α → ℝ) A
⊢ VectorMeasure.restrict μ.toSignedMeasure s = (μ.restrict s).toSignedMeasure

Tactic:
ext A hA
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Set α
hs : MeasurableSet s
A : Set α
hA : MeasurableSet A
⊢ (↑(VectorMeasure.restrict μ.toSignedMeasure s) : Set α → ℝ) A = (↑(μ.restrict s).toSignedMeasure : Set α → ℝ) A

Tactic:
simp [VectorMeasure.restrict_apply, toSignedMeasure_apply, hA, hs]

Premises used: MeasureTheory.VectorMeasure.restrict_apply, MeasureTheory.Measure.toSignedMeasure_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
rw :
  (∀ (i : Set α), MeasurableSet i → (↑μ.toSignedMeasure : Set α → ℝ) i ≤ (↑ν.toSignedMeasure : Set α → ℝ) i) ↔
    ∀ (s : Set α),
      MeasurableSet s → LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ.toSignedMeasure ≤ ν.toSignedMeasure ↔ μ ≤ ν

Tactic:
rw [Measure.le_iff, VectorMeasure.le_iff]

Premises used: MeasureTheory.VectorMeasure.le_iff, MeasureTheory.Measure.le_iff
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
a :
  ∀ (s : Set α) (hs : MeasurableSet s),
    (↑μ.toSignedMeasure : Set α → ℝ) s ≤ (↑ν.toSignedMeasure : Set α → ℝ) s ↔
      LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (∀ (i : Set α), MeasurableSet i → (↑μ.toSignedMeasure : Set α → ℝ) i ≤ (↑ν.toSignedMeasure : Set α → ℝ) i) ↔
    ∀ (s : Set α),
      MeasurableSet s → LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
congrm ∀ s, (hs : MeasurableSet s) → ?_
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set α
hs : MeasurableSet s
a :
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) ≤ ENNReal.toReal ((ν : (a : Set α) → ℝ≥0∞) s) ↔
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (↑μ.toSignedMeasure : Set α → ℝ) s ≤ (↑ν.toSignedMeasure : Set α → ℝ) s ↔
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp_rw [toSignedMeasure_apply_measurable hs, real_def]

Premises used: MeasureTheory.Measure.real_def, MeasureTheory.Measure.toSignedMeasure_apply_measurable
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : IsFiniteMeasure ν
s : Set α
hs : MeasurableSet s
a : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
a₁ : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) ≤ ENNReal.toReal ((ν : (a : Set α) → ℝ≥0∞) s) ↔
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
apply ENNReal.toReal_le_toReal

Premises used: ENNReal.toReal_le_toReal