awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
this : HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (n : ℕ), s n))
⊢ Tendsto (α := ℕ) ((fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, (↑v : Set α → M) (t i)) ∘ fun (a : ℕ) ↦ a + 1) atTop
    (𝓝 ((↑v : Set α → M) (⋃ (n : ℕ), s n)))

Tactic:
(HasSum.tendsto_sum_nat this).comp (tendsto_add_atTop_nat 1)

Premises used: HasSum.tendsto_sum_nat, Filter.tendsto_add_atTop_nat, Filter.Tendsto.comp, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
this : HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (n : ℕ), s n))
h :
  ∀ (n : ℕ),
    (↑v : Set α → M) (s n) = ((fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, (↑v : Set α → M) (t i)) ∘ fun (a : ℕ) ↦ a + 1) n
⊢ Tendsto (fun (n : ℕ) ↦ (↑v : Set α → M) (s n)) atTop (𝓝 ((↑v : Set α → M) (⋃ (n : ℕ), s n)))

Tactic:
convert! (HasSum.tendsto_sum_nat this).comp (tendsto_add_atTop_nat 1) with n

Premises used: HasSum.tendsto_sum_nat, Filter.tendsto_add_atTop_nat, Filter.Tendsto.comp, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
this : HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (n : ℕ), s n))
n : ℕ
h : (↑v : Set α → M) (s n) = ∑ i ∈ Finset.range (n + 1), (↑v : Set α → M) (t i)
⊢ (↑v : Set α → M) (s n) = ((fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, (↑v : Set α → M) (t i)) ∘ fun (a : ℕ) ↦ a + 1) n

Tactic:
dsimp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
this : HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (n : ℕ), s n))
n : ℕ
h : (↑v : Set α → M) (s n) = (↑v : Set α → M) (⋃ b ∈ Finset.range (n + 1), t b)
h₁ : (↑(Finset.range (n + 1)) : Set ℕ).PairwiseDisjoint t
h₂ : ∀ b ∈ Finset.range (n + 1), MeasurableSet (t b)
⊢ (↑v : Set α → M) (s n) = ∑ i ∈ Finset.range (n + 1), (↑v : Set α → M) (t i)

Tactic:
rw [← of_biUnion_finset]

Premises used: MeasureTheory.VectorMeasure.of_biUnion_finset
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
this : HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (n : ℕ), s n))
n : ℕ
h : (↑v : Set α → M) (s n) = (↑v : Set α → M) ((partialSups s : (a : ℕ) → Set α) n)
h₁ h₂ : (↑v : Set α → M) (s n) = (↑v : Set α → M) (s n)
⊢ (↑v : Set α → M) (s n) = (↑v : Set α → M) (⋃ b ∈ Finset.range (n + 1), t b)

Tactic:
rw [biUnion_range_succ_disjointed, Monotone.partialSups_eq hm]

Premises used: biUnion_range_succ_disjointed, Monotone.partialSups_eq
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
this : HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (n : ℕ), s n))
n : ℕ
⊢ (↑(Finset.range (n + 1)) : Set ℕ).PairwiseDisjoint t

Tactic:
fun i hi j hj hij ↦ disjoint_disjointed _ hij

Premises used: Set.PairwiseDisjoint, Set.Pairwise, disjoint_disjointed
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
this : HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (n : ℕ), s n))
n : ℕ
⊢ (↑(Finset.range (n + 1)) : Set ℕ).PairwiseDisjoint t

Tactic:
exact fun i hi j hj hij ↦ disjoint_disjointed _ hij

Premises used: disjoint_disjointed
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
this : HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (n : ℕ), s n))
n : ℕ
⊢ ∀ b ∈ Finset.range (n + 1), MeasurableSet (t b)

Tactic:
fun b hb ↦ ht _
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
v : VectorMeasure α M
inst_2 : T2Space M
s : ℕ → Set α
hm : Monotone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
t : ℕ → Set α := disjointed s
ht : ∀ (n : ℕ), MeasurableSet (t n)
this : HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (n : ℕ), s n))
n : ℕ
⊢ ∀ b ∈ Finset.range (n + 1), MeasurableSet (t b)

Tactic:
exact fun b hb ↦ ht _
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
inst_3 : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
n : ℕ
⊢ (↑v : Set α → M) (s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (s n)ᶜ

Tactic:
simp [of_compl (hs n)]

Premises used: MeasureTheory.VectorMeasure.of_compl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
inst_3 : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
⊢ ∀ (n : ℕ), (↑v : Set α → M) (s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (s n)ᶜ

Tactic:
have I n : v (s n) = v univ - v (s n)ᶜ := by simp [of_compl (hs n)]
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
inst_3 : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
I : ∀ (n : ℕ), (↑v : Set α → M) (s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (s n)ᶜ
rw : (↑v : Set α → M) (⋂ (n : ℕ), s n) = (↑v : Set α → M) (⋃ (b : ℕ), (s b)ᶜ)ᶜ
⊢ (↑v : Set α → M) (⋂ (n : ℕ), s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (⋃ (n : ℕ), (s n)ᶜ)

Tactic:
rw [← of_compl (MeasurableSet.iUnion (fun n ↦ (hs n).compl))]

Premises used: MeasurableSet.compl, MeasurableSet.iUnion, MeasureTheory.VectorMeasure.of_compl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
inst_3 : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
I : ∀ (n : ℕ), (↑v : Set α → M) (s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (s n)ᶜ
⊢ (↑v : Set α → M) (⋂ (n : ℕ), s n) = (↑v : Set α → M) (⋃ (b : ℕ), (s b)ᶜ)ᶜ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
inst_3 : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
I : ∀ (n : ℕ), (↑v : Set α → M) (s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (s n)ᶜ
⊢ (↑v : Set α → M) (⋂ (n : ℕ), s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (⋃ (n : ℕ), (s n)ᶜ)

Tactic:
have J : v (⋂ n, s n) = v univ - v (⋃ n, (s n)ᶜ) := by
    rw [← of_compl (MeasurableSet.iUnion (fun n ↦ (hs n).compl))]
    simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
inst_3 : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
I : ∀ (n : ℕ), (↑v : Set α → M) (s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (s n)ᶜ
J : (↑v : Set α → M) (⋂ (n : ℕ), s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (⋃ (n : ℕ), (s n)ᶜ)
simp_rw :
  Tendsto (fun (n : ℕ) ↦ (↑v : Set α → M) univ - (↑v : Set α → M) (s n)ᶜ) atTop
    (𝓝 ((↑v : Set α → M) univ - (↑v : Set α → M) (⋃ (n : ℕ), (s n)ᶜ)))
⊢ Tendsto (fun (n : ℕ) ↦ (↑v : Set α → M) (s n)) atTop (𝓝 ((↑v : Set α → M) (⋂ (n : ℕ), s n)))

Tactic:
simp_rw [I, J]
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
inst_3 : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
I : ∀ (n : ℕ), (↑v : Set α → M) (s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (s n)ᶜ
J : (↑v : Set α → M) (⋂ (n : ℕ), s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (⋃ (n : ℕ), (s n)ᶜ)
apply : Tendsto (fun (x : ℕ) ↦ (↑v : Set α → M) (s x)ᶜ) atTop (𝓝 ((↑v : Set α → M) (⋃ (n : ℕ), (s n)ᶜ)))
⊢ Tendsto (fun (n : ℕ) ↦ (↑v : Set α → M) univ - (↑v : Set α → M) (s n)ᶜ) atTop
    (𝓝 ((↑v : Set α → M) univ - (↑v : Set α → M) (⋃ (n : ℕ), (s n)ᶜ)))

Tactic:
apply tendsto_const_nhds.sub

Premises used: tendsto_const_nhds, Filter.Tendsto.sub
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
inst_3 : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
I : ∀ (n : ℕ), (↑v : Set α → M) (s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (s n)ᶜ
J : (↑v : Set α → M) (⋂ (n : ℕ), s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (⋃ (n : ℕ), (s n)ᶜ)
i j : ℕ
hij : i ≤ j
⊢ (s i)ᶜ ≤ (s j)ᶜ

Tactic:
simpa using hm hij
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_4
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : T2Space M
inst_3 : ContinuousSub M
v : VectorMeasure α M
s : ℕ → Set α
hm : Antitone s
hs : ∀ (i : ℕ), MeasurableSet (s i)
I : ∀ (n : ℕ), (↑v : Set α → M) (s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (s n)ᶜ
J : (↑v : Set α → M) (⋂ (n : ℕ), s n) = (↑v : Set α → M) univ - (↑v : Set α → M) (⋃ (n : ℕ), (s n)ᶜ)
⊢ Tendsto (fun (x : ℕ) ↦ (↑v : Set α → M) (s x)ᶜ) atTop (𝓝 ((↑v : Set α → M) (⋃ (n : ℕ), (s n)ᶜ)))

Tactic:
exact tendsto_vectorMeasure_iUnion_atTop_nat (fun i j hij ↦ by simpa using hm hij)
    (fun i ↦ (hs i).compl)

Premises used: MeasurableSet.compl, MeasureTheory.VectorMeasure.tendsto_vectorMeasure_iUnion_atTop_nat
-- 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
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
rw : r • (↑v : Set α → M) ∅ = 0
rw₁ : HSMul.hSMul (β := M) r 0 = 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := M) 0 0
⊢ (r • (↑v : Set α → M)) ∅ = 0

Tactic:
rw [Pi.smul_apply, empty, smul_zero]

Premises used: MeasureTheory.VectorMeasure.empty, smul_zero, Pi.smul_apply
-- 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
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
x : Set α
hi : ¬MeasurableSet x
rw : r • (↑v : Set α → M) x = 0
rw₁ : HSMul.hSMul (β := M) r 0 = 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := M) 0 0
⊢ (r • (↑v : Set α → M)) x = 0

Tactic:
rw [Pi.smul_apply, v.not_measurable hi, smul_zero]

Premises used: MeasureTheory.VectorMeasure.not_measurable, smul_zero, Pi.smul_apply
-- 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
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
x : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (x i)
hf₂ : Pairwise (Disjoint on x)
⊢ HasSum (fun (i : ℕ) ↦ (r • (↑v : Set α → M)) (x i)) ((r • (↑v : Set α → M)) (⋃ (i : ℕ), x i))

Tactic:
HasSum.const_smul _ (v.m_iUnion hf₁ hf₂)

Premises used: MeasureTheory.VectorMeasure.m_iUnion, HasSum.const_smul
-- 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
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
x : ℕ → Set α
hf₁ : ∀ (i : ℕ), MeasurableSet (x i)
hf₂ : Pairwise (Disjoint on x)
⊢ HasSum (fun (i : ℕ) ↦ (r • (↑v : Set α → M)) (x i)) ((r • (↑v : Set α → M)) (⋃ (i : ℕ), x i))

Tactic:
exact HasSum.const_smul _ (v.m_iUnion hf₁ hf₂)

Premises used: MeasureTheory.VectorMeasure.m_iUnion, HasSum.const_smul
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
⊢ (↑(r • v) : Set α → M) = r • (↑v : Set α → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
R : Type u_4
inst_2 : Semiring R
inst_3 : DistribMulAction R M
inst_4 : ContinuousConstSMul R M
r : R
v : VectorMeasure α M
i : Set α
⊢ (↑(r • v) : Set α → M) i = r • (↑v : Set α → M) i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : IsEmpty α
μ : VectorMeasure α M
s : Set α
⊢ (↑μ : Set α → M) s = 0

Tactic:
simp [eq_empty_of_isEmpty s]

Premises used: Set.eq_empty_of_isEmpty
-- 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 : IsEmpty α
μ ν : VectorMeasure α M
h : ∀ (i : Set α), MeasurableSet i → (↑μ : Set α → M) i = (↑ν : Set α → M) i
⊢ μ = ν

Tactic:
ext
-- 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 : IsEmpty α
μ ν : VectorMeasure α M
i : Set α
h_1 : MeasurableSet i
h : 0 = (↑ν : Set α → M) i
h₁ h₂ : Eq.{u_3 + 1} (α := M) 0 0
⊢ (↑μ : Set α → M) i = (↑ν : Set α → M) i

Tactic:
rw [apply_eq_zero_of_isEmpty, apply_eq_zero_of_isEmpty]

Premises used: MeasureTheory.VectorMeasure.apply_eq_zero_of_isEmpty
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : IsEmpty α
μ : VectorMeasure α M
⊢ μ = 0

Tactic:
Subsingleton.elim μ 0

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
⊢ Eq (α := Set α → M) (↑0 : Set α → M) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
i : Set α
⊢ Eq.{u_3 + 1} (α := M) ((↑0 : Set α → M) i) 0

Tactic:
rfl

Premises used: rfl
-- 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 : ContinuousAdd M
v w : VectorMeasure α M
⊢ ((↑v : Set α → M) + (↑w : Set α → M)) ∅ = 0

Tactic:
simp
-- 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 : ContinuousAdd M
v w : VectorMeasure α M
x : Set α
hi : ¬MeasurableSet x
rw : (↑v : Set α → M) x + (↑w : Set α → M) x = 0
rw₁ : 0 + (↑w : Set α → M) x = 0
rw₂ : HAdd.hAdd (α := M) 0 0 = 0
rw₃ rw₄ : Eq.{u_3 + 1} (α := M) 0 0
⊢ ((↑v : Set α → M) + (↑w : Set α → M)) x = 0

Tactic:
rw [Pi.add_apply, v.not_measurable hi, w.not_measurable hi, add_zero]

Premises used: MeasureTheory.VectorMeasure.not_measurable, Pi.add_apply, add_zero
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousAdd M
v w : VectorMeasure α M
⊢ (↑(v + w) : Set α → M) = (↑v : Set α → M) + (↑w : Set α → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousAdd M
v w : VectorMeasure α M
i : Set α
⊢ (↑(v + w) : Set α → M) i = (↑v : Set α → M) i + (↑w : Set α → M) i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousAdd M
ι : Type u_4
I : Finset ι
v : ι → VectorMeasure α M
⊢ Eq (α := Set α → M) (↑(∑ i ∈ I, v i) : Set α → M) (∑ i ∈ I, (↑(v i) : Set α → M))

Tactic:
map_sum coeFnAddMonoidHom v I

Premises used: MeasureTheory.VectorMeasure.coeFnAddMonoidHom, map_sum
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : IsTopologicalAddGroup M
v : VectorMeasure α M
⊢ (-(↑v : Set α → M)) ∅ = 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : IsTopologicalAddGroup M
v : VectorMeasure α M
x : Set α
hi : ¬MeasurableSet x
rw : -(↑v : Set α → M) x = 0
rw₁ : (↑v : Set α → M) x = 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := M) 0 0
⊢ (-(↑v : Set α → M)) x = 0

Tactic:
rw [Pi.neg_apply, neg_eq_zero, v.not_measurable hi]

Premises used: MeasureTheory.VectorMeasure.not_measurable, neg_eq_zero, Pi.neg_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : IsTopologicalAddGroup M
v : VectorMeasure α M
⊢ (↑(-v) : Set α → M) = -(↑v : Set α → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : IsTopologicalAddGroup M
v : VectorMeasure α M
i : Set α
⊢ (↑(-v) : Set α → M) i = -(↑v : Set α → M) i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : IsTopologicalAddGroup M
v w : VectorMeasure α M
⊢ ((↑v : Set α → M) - (↑w : Set α → M)) ∅ = 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : IsTopologicalAddGroup M
v w : VectorMeasure α M
x : Set α
hi : ¬MeasurableSet x
rw : (↑v : Set α → M) x - (↑w : Set α → M) x = 0
rw₁ : 0 - (↑w : Set α → M) x = 0
rw₂ : HSub.hSub (α := M) 0 0 = 0
rw₃ rw₄ : Eq.{u_3 + 1} (α := M) 0 0
⊢ ((↑v : Set α → M) - (↑w : Set α → M)) x = 0

Tactic:
rw [Pi.sub_apply, v.not_measurable hi, w.not_measurable hi, sub_zero]

Premises used: sub_zero, MeasureTheory.VectorMeasure.not_measurable, Pi.sub_apply
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : IsTopologicalAddGroup M
v w : VectorMeasure α M
⊢ (↑(v - w) : Set α → M) = (↑v : Set α → M) - (↑w : Set α → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst : AddCommGroup M
inst_1 : TopologicalSpace M
inst_2 : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
⊢ (↑(v - w) : Set α → M) i = (↑v : Set α → M) i - (↑w : Set α → M) i

Tactic:
rfl

Premises used: rfl
-- 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
⊢ (if MeasurableSet.{u_2} (α := β) ∅ ∧ Membership.mem (γ := Set β) ∅ x then v else 0) = 0

Tactic:
simp
-- 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
⊢ ∀ ⦃i : Set β⦄, ¬MeasurableSet i → (if MeasurableSet i ∧ x ∈ i then v else 0) = 0

Tactic:
simp +contextual
-- 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)
pos :
  ∀ (hx : Membership.mem (γ := Set β) (⋃ (i : ℕ), f i) x),
    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)
neg :
  ∀ (hx : x ∉ ⋃ (i : ℕ), f i),
    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)
⊢ 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:
by_cases hx : x ∈ ⋃ i, f i
-- 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 : x ∉ ⋃ (i : ℕ), f i
⊢ ∀ (x_2 : ℕ), x ∉ f x_2

Tactic:
simp only [mem_iUnion, not_exists] at hx

Premises used: Set.mem_iUnion, not_exists
-- 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 : ∀ (x_2 : ℕ), x ∉ f x_2
⊢ 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 [hx, hasSum_zero]

Premises used: hasSum_zero