-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem hasSum_of_disjoint_iUnion (hm : ∀ i, MeasurableSet (f i)) (hd : Pairwise (Disjoint on f)) :
    HasSum (fun i => v (f i)) (v (⋃ i, f i))

Proof state:
case intro.convert_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ ∀ (i : ℕ), MeasurableSet (Function.extend e f (fun x => ∅) i)

Tactic:
simp [Function.apply_extend MeasurableSet, Function.comp_def, hm]

Result:
no goals

Proof state:
case h.e'_5.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
x✝ : ℕ
⊢ Function.extend e (fun i => ↑v (f i)) 0 x✝ = ↑v (Function.extend e f (fun x => ∅) x✝)

Tactic:
simp only [Pi.zero_def, Function.apply_extend v, Function.comp_def, empty]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ i, f i))

Tactic:
rcases Countable.exists_injective_nat β with ⟨e, he⟩

Result:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ i, f i))

Proof state:
case h.e'_6.h.e'_7
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ ⋃ i, f i = ⋃ i, Function.extend e f (fun x => ∅) i

Tactic:
exact (iSup_extend_bot he _).symm

Result:
no goals

Proof state:
case intro.convert_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ Pairwise (Disjoint on Function.extend e f fun x => ∅)

Tactic:
exact hd.disjoint_extend_bot (he.factorsThrough _)

Result:
no goals

Proof state:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ HasSum (Function.extend e (fun i => ↑v (f i)) 0) (↑v (⋃ i, f i))

Tactic:
convert m_iUnion v (f := Function.extend e f fun _ ↦ ∅) _ _

Result:
case h.e'_5.h
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
x✝ : ℕ
⊢ Function.extend e (fun i => ↑v (f i)) 0 x✝ = ↑v (Function.extend e f (fun x => ∅) x✝)

case h.e'_6.h.e'_7
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ ⋃ i, f i = ⋃ i, Function.extend e f (fun x => ∅) i

case intro.convert_1
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ ∀ (i : ℕ), MeasurableSet (Function.extend e f (fun x => ∅) i)

case intro.convert_2
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ Pairwise (Disjoint on Function.extend e f fun x => ∅)

Proof state:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ HasSum (fun i => ↑v (f i)) (↑v (⋃ i, f i))

Tactic:
rw [← hasSum_extend_zero he]

Result:
case intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : TopologicalSpace M
inst✝ : Countable β
v : VectorMeasure α M
f : β → Set α
hm : ∀ (i : β), MeasurableSet (f i)
hd : Pairwise (Disjoint on f)
e : β → ℕ
he : Function.Injective e
⊢ HasSum (Function.extend e (fun i => ↑v (f i)) 0) (↑v (⋃ i, f i))