-- Mathlib/MeasureTheory/Measure/AddContent.lean
lemma addContent_union' (hs : s ∈ C) (ht : t ∈ C) (hst : s ∪ t ∈ C) (h_dis : Disjoint s t) :
    m (s ∪ t) = m s + m t

Proof state:
case h.e'_2.h.e'_6
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
h : m (⋃₀ ↑{s, t}) = ∑ u ∈ {s, t}, m u
⊢ s ∪ t = ⋃₀ ↑{s, t}

Tactic:
simp only [coe_pair, sUnion_insert, sUnion_singleton]

Result:
no goals

Proof state:
case neg.refine_3
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
⊢ ⋃₀ ↑{s, t} ∈ C

Tactic:
simp only [coe_pair, sUnion_insert, sUnion_singleton]

Result:
case neg.refine_3
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
⊢ s ∪ t ∈ C

Proof state:
case neg
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
⊢ m (s ∪ t) = m s + m t

Tactic:
have h := addContent_sUnion (m := m) (I := {s, t}) ?_ ?_ ?_

Result:
case neg.refine_4
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
h : m (⋃₀ ↑{s, t}) = ∑ u ∈ {s, t}, m u
⊢ m (s ∪ t) = m s + m t

case neg.refine_1
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
⊢ ↑{s, t} ⊆ C

case neg.refine_2
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
⊢ (↑{s, t}).PairwiseDisjoint id

case neg.refine_3
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
⊢ ⋃₀ ↑{s, t} ∈ C

Proof state:
case neg.refine_1
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
⊢ ↑{s, t} ⊆ C

Tactic:
simp only [coe_pair, Set.insert_subset_iff, hs, ht, Set.singleton_subset_iff, and_self_iff]

Result:
no goals

Proof state:
case neg.refine_4
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
h : m (⋃₀ ↑{s, t}) = ∑ u ∈ {s, t}, m u
⊢ m (s ∪ t) = m s + m t

case neg.refine_1
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
⊢ ↑{s, t} ⊆ C

case neg.refine_2
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
⊢ (↑{s, t}).PairwiseDisjoint id

case neg.refine_3
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
⊢ ⋃₀ ↑{s, t} ∈ C

Tactic:
rotate_left

Result:
case neg.refine_1
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
⊢ ↑{s, t} ⊆ C

case neg.refine_2
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
⊢ (↑{s, t}).PairwiseDisjoint id

case neg.refine_3
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
⊢ ⋃₀ ↑{s, t} ∈ C

case neg.refine_4
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
h : m (⋃₀ ↑{s, t}) = ∑ u ∈ {s, t}, m u
⊢ m (s ∪ t) = m s + m t

Proof state:
case h.e'_3
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
h : m (⋃₀ ↑{s, t}) = ∑ u ∈ {s, t}, m u
⊢ s ∉ {t}

Tactic:
simp only [Finset.mem_singleton]

Result:
case h.e'_3
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
h : m (⋃₀ ↑{s, t}) = ∑ u ∈ {s, t}, m u
⊢ ¬s = t

Proof state:
case pos
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : s = ∅
⊢ m (s ∪ t) = m s + m t

Tactic:
simp only [hs_empty, Set.empty_union, addContent_empty, zero_add]

Result:
no goals

Proof state:
case neg.refine_3
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
⊢ s ∪ t ∈ C

Tactic:
exact hst

Result:
no goals

Proof state:
case h.e'_3
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
h : m (⋃₀ ↑{s, t}) = ∑ u ∈ {s, t}, m u
⊢ m s + m t = ∑ u ∈ {s, t}, m u

Tactic:
rw [sum_insert, sum_singleton]

Result:
case h.e'_3
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
h : m (⋃₀ ↑{s, t}) = ∑ u ∈ {s, t}, m u
⊢ s ∉ {t}

Proof state:
case neg.refine_2
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
⊢ ¬s = t → Disjoint s t

Tactic:
exact fun _ => h_dis

Result:
no goals

Proof state:
case neg.refine_4
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
h : m (⋃₀ ↑{s, t}) = ∑ u ∈ {s, t}, m u
⊢ m (s ∪ t) = m s + m t

Tactic:
convert h

Result:
case h.e'_2.h.e'_6
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
h : m (⋃₀ ↑{s, t}) = ∑ u ∈ {s, t}, m u
⊢ s ∪ t = ⋃₀ ↑{s, t}

case h.e'_3
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
h : m (⋃₀ ↑{s, t}) = ∑ u ∈ {s, t}, m u
⊢ m s + m t = ∑ u ∈ {s, t}, m u

Proof state:
case neg.refine_2
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
⊢ (↑{s, t}).PairwiseDisjoint id

Tactic:
simp only [coe_pair, Set.pairwiseDisjoint_insert, pairwiseDisjoint_singleton,
  mem_singleton_iff, Ne, id, forall_eq, true_and]

Result:
case neg.refine_2
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
⊢ ¬s = t → Disjoint s t

Proof state:
case h.e'_3
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s s
hs_empty : ¬s = ∅
h : m (⋃₀ ↑{s, t}) = ∑ u ∈ {s, t}, m u
hs_eq_t : s = t
⊢ s = ∅

Tactic:
exact Disjoint.eq_bot_of_self h_dis

Result:
no goals

Proof state:
case h.e'_3
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
h : m (⋃₀ ↑{s, t}) = ∑ u ∈ {s, t}, m u
⊢ ¬s = t

Tactic:
refine fun hs_eq_t => hs_empty ?_

Result:
case h.e'_3
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
h : m (⋃₀ ↑{s, t}) = ∑ u ∈ {s, t}, m u
hs_eq_t : s = t
⊢ s = ∅

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
⊢ m (s ∪ t) = m s + m t

Tactic:
by_cases hs_empty : s = ∅

Result:
case pos
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : s = ∅
⊢ m (s ∪ t) = m s + m t

case neg
α : Type u_1
C : Set (Set α)
s t : Set α
m : AddContent C
hs : s ∈ C
ht : t ∈ C
hst : s ∪ t ∈ C
h_dis : Disjoint s t
hs_empty : ¬s = ∅
⊢ m (s ∪ t) = m s + m t