-- Mathlib/MeasureTheory/Measure/AddContent.lean
theorem eq_add_disjointOfDiff_of_subset (hC : IsSetSemiring C)
    (hs : s ∈ C) (ht : t ∈ C) (hst : s ⊆ t) :
    m t = m s + ∑ i ∈ hC.disjointOfDiff ht hs, m i

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ m (⋃₀ insert s ↑(hC.disjointOfDiff ht hs)) = m s + ∑ i ∈ hC.disjointOfDiff ht hs, m i

Tactic:
rw [← coe_insert, addContent_sUnion]

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ∑ u ∈ insert s (hC.disjointOfDiff ht hs), m u = m s + ∑ i ∈ hC.disjointOfDiff ht hs, m i

case h_ss
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ↑(insert s (hC.disjointOfDiff ht hs)) ⊆ C

case h_dis
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ (↑(insert s (hC.disjointOfDiff ht hs))).PairwiseDisjoint id

case h_mem
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ⋃₀ ↑(insert s (hC.disjointOfDiff ht hs)) ∈ C

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ m t = m s + ∑ i ∈ hC.disjointOfDiff ht hs, m i

Tactic:
conv_lhs => rw [← hC.sUnion_insert_disjointOfDiff ht hs hst]

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ m (⋃₀ insert s ↑(hC.disjointOfDiff ht hs)) = m s + ∑ i ∈ hC.disjointOfDiff ht hs, m i

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ∑ u ∈ insert s (hC.disjointOfDiff ht hs), m u = m s + ∑ i ∈ hC.disjointOfDiff ht hs, m i

Tactic:
rw [sum_insert]

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ s ∉ hC.disjointOfDiff ht hs

Proof state:
case h_dis
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ (↑(insert s (hC.disjointOfDiff ht hs))).PairwiseDisjoint id

Tactic:
rw [coe_insert]

Result:
case h_dis
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ (insert s ↑(hC.disjointOfDiff ht hs)).PairwiseDisjoint id

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ s ∉ hC.disjointOfDiff ht hs

Tactic:
exact hC.nmem_disjointOfDiff ht hs

Result:
no goals

Proof state:
case h_ss
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ↑(insert s (hC.disjointOfDiff ht hs)) ⊆ C

Tactic:
rw [coe_insert]

Result:
case h_ss
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ insert s ↑(hC.disjointOfDiff ht hs) ⊆ C

Proof state:
case h_mem
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ⋃₀ insert s ↑(hC.disjointOfDiff ht hs) ∈ C

Tactic:
rwa [hC.sUnion_insert_disjointOfDiff ht hs hst]

Result:
no goals

Proof state:
case h_ss
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ insert s ↑(hC.disjointOfDiff ht hs) ⊆ C

Tactic:
exact Set.insert_subset hs (hC.subset_disjointOfDiff ht hs)

Result:
no goals

Proof state:
case h_dis
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ (insert s ↑(hC.disjointOfDiff ht hs)).PairwiseDisjoint id

Tactic:
exact hC.pairwiseDisjoint_insert_disjointOfDiff ht hs

Result:
no goals

Proof state:
case h_mem
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ⋃₀ ↑(insert s (hC.disjointOfDiff ht hs)) ∈ C

Tactic:
rw [coe_insert]

Result:
case h_mem
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : s ⊆ t
⊢ ⋃₀ insert s ↑(hC.disjointOfDiff ht hs) ∈ C