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
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
⊢ Disjoint (A ∩ B) (A \ B)

Tactic:
exact Set.disjoint_of_subset_left A.inter_subset_right disjoint_sdiff_self_right

Premises used: disjoint_sdiff_self_right, Set.disjoint_of_subset_left, Set.inter_subset_right
-- 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
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
⊢ MeasurableSet (A \ B)

Tactic:
hA.diff hB

Premises used: MeasurableSet.diff
-- 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
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
⊢ MeasurableSet (A \ B)

Tactic:
exact hA.diff hB

Premises used: MeasurableSet.diff
-- 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
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
⊢ MeasurableSet (A ∩ B)

Tactic:
hA.inter hB

Premises used: MeasurableSet.inter
-- 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
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
⊢ MeasurableSet (A ∩ B)

Tactic:
exact hA.inter hB

Premises used: MeasurableSet.inter
-- 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
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
h : Disjoint (A ∩ B) (B \ A)
hA₁ : MeasurableSet (A ∩ B)
hB₁ : MeasurableSet (B \ A)
⊢ (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B ∪ B \ A)

Tactic:
rw [of_union, h', add_zero]

Premises used: MeasureTheory.VectorMeasure.of_union, add_zero
-- 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
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
⊢ Disjoint (A ∩ B) (B \ A)

Tactic:
Set.disjoint_of_subset_left A.inter_subset_left disjoint_sdiff_self_right

Premises used: disjoint_sdiff_self_right, Set.disjoint_of_subset_left, Set.inter_subset_left
-- 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
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
⊢ Disjoint (A ∩ B) (B \ A)

Tactic:
exact Set.disjoint_of_subset_left A.inter_subset_left disjoint_sdiff_self_right

Premises used: disjoint_sdiff_self_right, Set.disjoint_of_subset_left, Set.inter_subset_left
-- 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
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
⊢ MeasurableSet (B \ A)

Tactic:
hB.diff hA

Premises used: MeasurableSet.diff
-- 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
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
⊢ MeasurableSet (B \ A)

Tactic:
exact hB.diff hA

Premises used: MeasurableSet.diff
-- 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
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
rw : (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (B \ A ∪ A ∩ B) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B
rw₁ : (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (B \ A ∪ B ∩ A) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B
rw₂ rw₃ : (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B
⊢ (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B ∪ B \ A) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B

Tactic:
rw [Set.union_comm, Set.inter_comm, Set.diff_union_inter]

Premises used: Set.union_comm, Set.inter_comm, Set.diff_union_inter
-- 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
A B : Set α
hA : MeasurableSet A
hB : MeasurableSet B
h' : (↑v : Set α → M) (B \ A) = 0
v₁ : (↑v : Set α → M) A = (↑v : Set α → M) (A \ B ∪ A ∩ B)
v₂ : (↑v : Set α → M) (A \ B ∪ A ∩ B) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B)
v₃ : (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B ∪ B \ A)
v₄ : (↑v : Set α → M) (A \ B) + (↑v : Set α → M) (A ∩ B ∪ B \ A) = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B
⊢ (↑v : Set α → M) A = (↑v : Set α → M) (A \ B) + (↑v : Set α → M) B

Tactic:
calc
    v A = v (A \ B ∪ A ∩ B) := by simp only [Set.diff_union_inter]
    _ = v (A \ B) + v (A ∩ B) := by
      rw [of_union]
      · rw [disjoint_comm]
        exact Set.disjoint_of_subset_left A.inter_subset_right disjoint_sdiff_self_right
      · exact hA.diff hB
      · exact hA.inter hB
    _ = v (A \ B) + v (A ∩ B ∪ B \ A) := by
      rw [of_union, h', add_zero]
      · exact Set.disjoint_of_subset_left A.inter_subset_left disjoint_sdiff_self_right
      · exact hA.inter hB
      · exact hB.diff hA
    _ = v (A \ B) + v B := by rw [Set.union_comm, Set.inter_comm, Set.diff_union_inter]

Premises used: MeasureTheory.VectorMeasure.measureOf', Inter.inter, SDiff.sdiff, Union.union
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : Countable β
f : β → Set α
M : Type u_4
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : PartialOrder M
inst_4 : IsOrderedAddMonoid M
inst_5 : OrderClosedTopology M
v : VectorMeasure α M
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
hf₃ : ∀ (i : β), 0 ≤ (↑v : Set α → M) (f i)
⊢ 0 ≤ (↑v : Set α → M) (⋃ (i : β), f i)

Tactic:
(v.of_disjoint_iUnion hf₁ hf₂).symm ▸ tsum_nonneg hf₃

Premises used: Eq.rec, MeasureTheory.VectorMeasure.of_disjoint_iUnion, tsum_nonneg, Eq.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : Countable β
f : β → Set α
M : Type u_4
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : PartialOrder M
inst_4 : IsOrderedAddMonoid M
inst_5 : OrderClosedTopology M
v : VectorMeasure α M
hf₁ : ∀ (i : β), MeasurableSet (f i)
hf₂ : Pairwise (Disjoint on f)
hf₃ : ∀ (i : β), (↑v : Set α → M) (f i) ≤ 0
⊢ (↑v : Set α → M) (⋃ (i : β), f i) ≤ 0

Tactic:
(v.of_disjoint_iUnion hf₁ hf₂).symm ▸ tsum_nonpos hf₃

Premises used: tsum_nonpos, Eq.rec, MeasureTheory.VectorMeasure.of_disjoint_iUnion, Eq.symm
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : 0 ≤ (↑s : Set α → ℝ) A
hB₂ : 0 ≤ (↑s : Set α → ℝ) B
hAB : (↑s : Set α → ℝ) (A ∪ B) = 0
⊢ (↑s : Set α → ℝ) A + (↑s : Set α → ℝ) B = 0

Tactic:
rw [of_union h hA₁ hB₁] at hAB

Premises used: MeasureTheory.VectorMeasure.of_union
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : 0 ≤ (↑s : Set α → ℝ) A
hB₂ : 0 ≤ (↑s : Set α → ℝ) B
hAB : (↑s : Set α → ℝ) A + (↑s : Set α → ℝ) B = 0
linarith : (↑s : Set α → ℝ) A < 0 → 0 - (↑s : Set α → ℝ) A + ((↑s : Set α → ℝ) A - 0) = 0
linarith₁ :
  0 < (↑s : Set α → ℝ) A →
    0 - (↑s : Set α → ℝ) B + ((↑s : Set α → ℝ) A + (↑s : Set α → ℝ) B - 0) + (0 - (↑s : Set α → ℝ) A) = 0
⊢ (↑s : Set α → ℝ) A = 0

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : (↑s : Set α → ℝ) A ≤ 0
hB₂ : (↑s : Set α → ℝ) B ≤ 0
hAB : (↑s : Set α → ℝ) (A ∪ B) = 0
⊢ (↑s : Set α → ℝ) A + (↑s : Set α → ℝ) B = 0

Tactic:
rw [of_union h hA₁ hB₁] at hAB

Premises used: MeasureTheory.VectorMeasure.of_union
-- Module: Mathlib.MeasureTheory.VectorMeasure.Basic
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : (↑s : Set α → ℝ) A ≤ 0
hB₂ : (↑s : Set α → ℝ) B ≤ 0
hAB : (↑s : Set α → ℝ) A + (↑s : Set α → ℝ) B = 0
linarith :
  (↑s : Set α → ℝ) A < 0 →
    (↑s : Set α → ℝ) B - 0 + -((↑s : Set α → ℝ) A + (↑s : Set α → ℝ) B - 0) + ((↑s : Set α → ℝ) A - 0) = 0
linarith₁ : 0 < (↑s : Set α → ℝ) A → (↑s : Set α → ℝ) A - 0 + (0 - (↑s : Set α → ℝ) A) = 0
⊢ (↑s : Set α → ℝ) A = 0

Tactic:
linarith
-- 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
ι : Type u_4
f : ι → Set α
hd : (↑∅ : Set ι).PairwiseDisjoint f
hm : ∀ (b : ι), Membership.mem (γ := Finset ι) ∅ b → MeasurableSet (f b)
⊢ (↑v : Set α → M) (⋃ (b : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ b), f b) = ∑ p ∈ ∅, (↑v : Set α → M) (f p)

Tactic:
simp
-- 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
ι : Type u_4
f : ι → Set α
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
hd : (↑(Insert.insert a s) : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ Insert.insert a s, MeasurableSet (f b)
insert : (↑v : Set α → M) (f a ∪ ⋃ x ∈ s, f x) = (↑v : Set α → M) (f a) + ∑ p ∈ s, (↑v : Set α → M) (f p)
⊢ (↑v : Set α → M) (⋃ b ∈ Insert.insert a s, f b) = ∑ p ∈ Insert.insert a s, (↑v : Set α → M) (f p)

Tactic:
simp only [Finset.mem_insert, iUnion_iUnion_eq_or_left, has, not_false_eq_true,
      Finset.sum_insert]

Premises used: Finset.mem_insert, Set.iUnion_iUnion_eq_or_left, Finset.sum_insert, not_false_eq_true
-- 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
ι : Type u_4
f : ι → Set α
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
hd : (↑(Insert.insert a s) : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ Insert.insert a s, MeasurableSet (f b)
insert : (↑s : Set ι).PairwiseDisjoint f
insert₁ : ∀ b ∈ s, MeasurableSet (f b)
insert₂ : Disjoint (f a) (⋃ x ∈ s, f x)
insert₃ : MeasurableSet (f a)
insert₄ : MeasurableSet.{u_1} (α := α) (⋃ x ∈ s, f x)
⊢ (↑v : Set α → M) (f a ∪ ⋃ x ∈ s, f x) = (↑v : Set α → M) (f a) + ∑ p ∈ s, (↑v : Set α → M) (f p)

Tactic:
rw [of_union, ih]

Premises used: MeasureTheory.VectorMeasure.of_union
-- 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
ι : Type u_4
f : ι → Set α
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
hd : (↑(insert a s) : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ insert a s, MeasurableSet (f b)
⊢ (↑s : Set ι) ⊆ (↑(insert a s) : Set ι)

Tactic:
simp
-- 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
ι : Type u_4
f : ι → Set α
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
hd : (↑(insert a s) : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ insert a s, MeasurableSet (f b)
⊢ (↑s : Set ι).PairwiseDisjoint f

Tactic:
exact hd.subset (by simp)

Premises used: Set.PairwiseDisjoint.subset
-- 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
ι : Type u_4
f : ι → Set α
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
hd : (↑(insert a s) : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ insert a s, MeasurableSet (f b)
⊢ ∀ b ∈ s, MeasurableSet (f b)

Tactic:
grind
-- 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
ι : Type u_4
f : ι → Set α
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
hd : (↑(Insert.insert a s) : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ Insert.insert a s, MeasurableSet (f b)
insert : ∀ (i : ι) (i_1 : i ∈ s), Disjoint (f a) (f i)
⊢ Disjoint (f a) (⋃ x ∈ s, f x)

Tactic:
simp only [disjoint_iUnion_right]

Premises used: Set.disjoint_iUnion_right
-- 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
ι : Type u_4
f : ι → Set α
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
hd : (↑(insert a s) : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ insert a s, MeasurableSet (f b)
i : ι
hi : i ∈ s
⊢ a ∈ (↑(insert a s) : Set ι)

Tactic:
simp
-- 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
ι : Type u_4
f : ι → Set α
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
hd : (↑(insert a s) : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ insert a s, MeasurableSet (f b)
i : ι
hi : i ∈ s
⊢ i ∈ (↑(insert a s) : Set ι)

Tactic:
simp [hi]
-- 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
ι : Type u_4
f : ι → Set α
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
hd : (↑(insert a s) : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ insert a s, MeasurableSet (f b)
i : ι
hi : i ∈ s
⊢ a ≠ i

Tactic:
grind
-- 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
ι : Type u_4
f : ι → Set α
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
hd : (↑(insert a s) : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ insert a s, MeasurableSet (f b)
⊢ ∀ (i : ι) (i_1 : i ∈ s), Disjoint (f a) (f i)

Tactic:
exact fun i hi ↦ hd (by simp) (by simp [hi]) (by grind)
-- 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
ι : Type u_4
f : ι → Set α
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
hd : (↑(insert a s) : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ insert a s, MeasurableSet (f b)
⊢ a ∈ insert a s

Tactic:
simp
-- 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
ι : Type u_4
f : ι → Set α
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
hd : (↑(insert a s) : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ insert a s, MeasurableSet (f b)
⊢ MeasurableSet (f a)

Tactic:
apply hm _ (by simp)
-- 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
ι : Type u_4
f : ι → Set α
a : ι
s : Finset ι
has : a ∉ s
ih :
  ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)
hd : (↑(insert a s) : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ insert a s, MeasurableSet (f b)
⊢ MeasurableSet.{u_1} (α := α) (⋃ x ∈ s, f x)

Tactic:
apply Finset.measurableSet_biUnion _ (by grind)

Premises used: Finset.measurableSet_biUnion
-- 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
ι : Type u_4
s : Finset ι
f : ι → Set α
hd : (↑s : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ s, MeasurableSet (f b)
empty :
  ∀ (hd : (↑∅ : Set ι).PairwiseDisjoint f) (hm : ∀ (b : ι), Membership.mem (γ := Finset ι) ∅ b → MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ (b : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ b), f b) = ∑ p ∈ ∅, (↑v : Set α → M) (f p)
insert :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (ih :
      ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
        (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p))
    (hd : (↑(Insert.insert a s) : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ Insert.insert a s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ Insert.insert a s, f b) = ∑ p ∈ Insert.insert a s, (↑v : Set α → M) (f p)
⊢ (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)

Tactic:
induction s using Finset.induction with
  | empty => simp
  | insert a s has ih =>
    simp only [Finset.mem_insert, iUnion_iUnion_eq_or_left, has, not_false_eq_true,
      Finset.sum_insert]
    rw [of_union, ih]
    · exact hd.subset (by simp)
    · grind
    · simp only [disjoint_iUnion_right]
      exact fun i hi ↦ hd (by simp) (by simp [hi]) (by grind)
    · apply hm _ (by simp)
    · apply Finset.measurableSet_biUnion _ (by grind)

Premises used: MeasureTheory.VectorMeasure.empty, Insert.insert, Finset.mem_insert, MeasureTheory.VectorMeasure.of_union, Set.disjoint_iUnion_right, Set.PairwiseDisjoint.subset, Set.iUnion_iUnion_eq_or_left, Finset.sum_insert, not_false_eq_true, Finset.measurableSet_biUnion
-- 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
ι : Type u_4
s : Finset ι
f : ι → Set α
hd : (↑s : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ s, MeasurableSet (f b)
empty :
  ∀ (hd : (↑∅ : Set ι).PairwiseDisjoint f) (hm : ∀ (b : ι), Membership.mem (γ := Finset ι) ∅ b → MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ (b : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ b), f b) = ∑ p ∈ ∅, (↑v : Set α → M) (f p)
insert :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (ih :
      ∀ (hd : (↑s : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)),
        (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p))
    (hd : (↑(Insert.insert a s) : Set ι).PairwiseDisjoint f) (hm : ∀ b ∈ Insert.insert a s, MeasurableSet (f b)),
    (↑v : Set α → M) (⋃ b ∈ Insert.insert a s, f b) = ∑ p ∈ Insert.insert a s, (↑v : Set α → M) (f p)
⊢ (↑v : Set α → M) (⋃ b ∈ s, f b) = ∑ p ∈ s, (↑v : Set α → M) (f p)

Tactic:
classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s has ih =>
    simp only [Finset.mem_insert, iUnion_iUnion_eq_or_left, has, not_false_eq_true,
      Finset.sum_insert]
    rw [of_union, ih]
    · exact hd.subset (by simp)
    · grind
    · simp only [disjoint_iUnion_right]
      exact fun i hi ↦ hd (by simp) (by simp [hi]) (by grind)
    · apply hm _ (by simp)
    · apply Finset.measurableSet_biUnion _ (by grind)

Premises used: MeasureTheory.VectorMeasure.empty, Insert.insert, Finset.mem_insert, MeasureTheory.VectorMeasure.of_union, Set.disjoint_iUnion_right, Set.PairwiseDisjoint.subset, Set.iUnion_iUnion_eq_or_left, Finset.sum_insert, not_false_eq_true, Finset.measurableSet_biUnion
-- 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
⊢ ∀ (n : ℕ), MeasurableSet (t n)

Tactic:
have ht n : MeasurableSet (t n) := .disjointed (fun n ↦ hs n) n
-- 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)
rw : HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (i : ℕ), disjointed s i))
⊢ HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (n : ℕ), s n))

Tactic:
rw [← iUnion_disjointed]

Premises used: iUnion_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)
⊢ HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (i : ℕ), disjointed s i))

Tactic:
apply m_iUnion _ ht (disjoint_disjointed _)

Premises used: disjoint_disjointed, MeasureTheory.VectorMeasure.m_iUnion
-- 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)
⊢ HasSum (fun (n : ℕ) ↦ (↑v : Set α → M) (t n)) ((↑v : Set α → M) (⋃ (n : ℕ), s n))

Tactic:
have : HasSum (fun n ↦ v (t n)) (v (⋃ n, s n)) := by
    rw [← iUnion_disjointed]
    apply m_iUnion _ ht (disjoint_disjointed _)