-- Mathlib/MeasureTheory/Measure/AddContent.lean
lemma addContent_eq_add_disjointOfDiffUnion_of_subset (hC : IsSetSemiring C)
    (hs : s ∈ C) (hI : ↑I ⊆ C) (hI_ss : ∀ t ∈ I, t ⊆ s)
    (h_dis : PairwiseDisjoint (I : Set (Set α)) id) :
    m s = ∑ i ∈ I, m i + ∑ i ∈ hC.disjointOfDiffUnion hs hI, m i

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ m (⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI)) = ∑ i ∈ I, m i + ∑ i ∈ hC.disjointOfDiffUnion hs hI, m i

Tactic:
rw [addContent_sUnion]

Result:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ∑ u ∈ I ∪ hC.disjointOfDiffUnion hs hI, m u = ∑ i ∈ I, m i + ∑ i ∈ hC.disjointOfDiffUnion hs hI, m i

case h_ss
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ↑(I ∪ hC.disjointOfDiffUnion hs hI) ⊆ C

case h_dis
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ (↑(I ∪ hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id

case h_mem
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI) ∈ C

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ Disjoint I (hC.disjointOfDiffUnion hs hI)

Tactic:
exact hC.disjoint_disjointOfDiffUnion hs hI

Result:
no goals

Proof state:
case h_ss
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ↑I ∪ ↑(hC.disjointOfDiffUnion hs hI) ⊆ C

Tactic:
exact Set.union_subset hI (hC.disjointOfDiffUnion_subset hs hI)

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ m s = ∑ i ∈ I, m i + ∑ i ∈ hC.disjointOfDiffUnion hs hI, m i

Tactic:
conv_lhs => rw [← hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]

Result:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ m (⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI)) = ∑ i ∈ I, m i + ∑ i ∈ hC.disjointOfDiffUnion hs hI, m i

Proof state:
case h_dis
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ (↑I ∪ ↑(hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id

Tactic:
exact hC.pairwiseDisjoint_union_disjointOfDiffUnion hs hI h_dis

Result:
no goals

Proof state:
case h_dis
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ (↑(I ∪ hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id

Tactic:
rw [coe_union]

Result:
case h_dis
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ (↑I ∪ ↑(hC.disjointOfDiffUnion hs hI)).PairwiseDisjoint id

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ∑ u ∈ I ∪ hC.disjointOfDiffUnion hs hI, m u = ∑ i ∈ I, m i + ∑ i ∈ hC.disjointOfDiffUnion hs hI, m i

Tactic:
rw [sum_union]

Result:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ Disjoint I (hC.disjointOfDiffUnion hs hI)

Proof state:
case h_mem
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ⋃₀ ↑(I ∪ hC.disjointOfDiffUnion hs hI) ∈ C

Tactic:
rwa [hC.sUnion_union_disjointOfDiffUnion_of_subset hs hI hI_ss]

Result:
no goals

Proof state:
case h_ss
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ↑(I ∪ hC.disjointOfDiffUnion hs hI) ⊆ C

Tactic:
rw [coe_union]

Result:
case h_ss
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
h_dis : (↑I).PairwiseDisjoint id
⊢ ↑I ∪ ↑(hC.disjointOfDiffUnion hs hI) ⊆ C