-- Mathlib/MeasureTheory/Measure/AddContent.lean
/-- An `addContent C` on a `SetSemiring C` is sub-additive. -/
lemma addContent_sUnion_le_sum {m : AddContent C} (hC : IsSetSemiring C)
    (J : Finset (Set α)) (h_ss : ↑J ⊆ C) (h_mem : ⋃₀ ↑J ∈ C) :
    m (⋃₀ ↑J) ≤ ∑ u ∈ J, m u

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)).PairwiseDisjoint id
h3 : ⋃₀ ↑J = ⋃₀ ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)
⊢ m (⋃₀ ↑J) ≤ ∑ u ∈ J, m u

Tactic:
rw [h3, addContent_sUnion h1 h2, sum_disjiUnion]

Result:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)).PairwiseDisjoint id
h3 : ⋃₀ ↑J = ⋃₀ ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)
⊢ ∑ i ∈ J, ∑ x ∈ hC.disjointOfUnion h_ss i, m x ≤ ∑ u ∈ J, m u

α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)).PairwiseDisjoint id
h3 : ⋃₀ ↑J = ⋃₀ ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)
⊢ ⋃₀ ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ∈ C

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)).PairwiseDisjoint id
h3 : ⋃₀ ↑J = ⋃₀ ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)
⊢ ∑ i ∈ J, ∑ x ∈ hC.disjointOfUnion h_ss i, m x ≤ ∑ u ∈ J, m u

Tactic:
apply sum_le_sum

Result:
case h
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)).PairwiseDisjoint id
h3 : ⋃₀ ↑J = ⋃₀ ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)
⊢ ∀ i ∈ J, ∑ x ∈ hC.disjointOfUnion h_ss i, m x ≤ m i

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)).PairwiseDisjoint id
⊢ ⋃₀ ↑J = ⋃₀ ⋃ x ∈ J, ↑(hC.disjointOfUnion h_ss x)

Tactic:
exact (Exists.choose_spec (hC.disjointOfUnion_props h_ss)).2.2.2.2.2

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)).PairwiseDisjoint id
h3 : ⋃₀ ↑J = ⋃₀ ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)
⊢ ⋃₀ ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ∈ C

Tactic:
simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe] at *

Result:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ⋃ x ∈ J, ↑(hC.disjointOfUnion h_ss x) ⊆ C
h2 : (⋃ x ∈ J, ↑(hC.disjointOfUnion h_ss x)).PairwiseDisjoint id
h3 : ⋃₀ ↑J = ⋃₀ ⋃ x ∈ J, ↑(hC.disjointOfUnion h_ss x)
⊢ ⋃₀ ⋃ x ∈ J, ↑(hC.disjointOfUnion h_ss x) ∈ C

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ⊆ C
⊢ (⋃ x ∈ J, ↑(hC.disjointOfUnion h_ss x)).PairwiseDisjoint id

Tactic:
exact hC.pairwiseDisjoint_biUnion_disjointOfUnion h_ss

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ⊆ C
⊢ m (⋃₀ ↑J) ≤ ∑ u ∈ J, m u

Tactic:
have h2 : PairwiseDisjoint (disjiUnion J (hC.disjointOfUnion h_ss)
    ((hC.pairwiseDisjoint_disjointOfUnion h_ss)) : Set (Set α)) id := by
  simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe]
  exact hC.pairwiseDisjoint_biUnion_disjointOfUnion h_ss

Result:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)).PairwiseDisjoint id
⊢ m (⋃₀ ↑J) ≤ ∑ u ∈ J, m u

Proof state:
case h
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)).PairwiseDisjoint id
h3 : ⋃₀ ↑J = ⋃₀ ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)
⊢ ∀ i ∈ J, ∑ x ∈ hC.disjointOfUnion h_ss i, m x ≤ m i

Tactic:
intro x hx

Result:
case h
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)).PairwiseDisjoint id
h3 : ⋃₀ ↑J = ⋃₀ ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)
x : Set α
hx : x ∈ J
⊢ ∑ x ∈ hC.disjointOfUnion h_ss x, m x ≤ m x

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
⊢ m (⋃₀ ↑J) ≤ ∑ u ∈ J, m u

Tactic:
have h1 : (disjiUnion J (hC.disjointOfUnion h_ss)
    (hC.pairwiseDisjoint_disjointOfUnion h_ss) : Set (Set α)) ⊆ C := by
  simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe, iUnion_subset_iff]
  exact fun _ x ↦ hC.disjointOfUnion_subset h_ss x

Result:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ⊆ C
⊢ m (⋃₀ ↑J) ≤ ∑ u ∈ J, m u

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)).PairwiseDisjoint id
⊢ ⋃₀ ↑J = ⋃₀ ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)

Tactic:
simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe]

Result:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)).PairwiseDisjoint id
⊢ ⋃₀ ↑J = ⋃₀ ⋃ x ∈ J, ↑(hC.disjointOfUnion h_ss x)

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ⋃ x ∈ J, ↑(hC.disjointOfUnion h_ss x) ⊆ C
h2 : (⋃ x ∈ J, ↑(hC.disjointOfUnion h_ss x)).PairwiseDisjoint id
h3 : ⋃₀ ↑J = ⋃₀ ⋃ x ∈ J, ↑(hC.disjointOfUnion h_ss x)
⊢ ⋃₀ ⋃ x ∈ J, ↑(hC.disjointOfUnion h_ss x) ∈ C

Tactic:
exact h3.symm ▸ h_mem

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
⊢ ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ⊆ C

Tactic:
simp only [disjiUnion_eq_biUnion, coe_biUnion, mem_coe, iUnion_subset_iff]

Result:
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
⊢ ∀ i ∈ J, ↑(hC.disjointOfUnion h_ss i) ⊆ C

Proof state:
case h
α : Type u_1
C : Set (Set α)
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_mem : ⋃₀ ↑J ∈ C
h1 : ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯) ⊆ C
h2 : (↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)).PairwiseDisjoint id
h3 : ⋃₀ ↑J = ⋃₀ ↑(J.disjiUnion (hC.disjointOfUnion h_ss) ⋯)
x : Set α
hx : x ∈ J
⊢ ∑ x ∈ hC.disjointOfUnion h_ss x, m x ≤ m x

Tactic:
refine sum_addContent_le_of_subset hC (hC.disjointOfUnion_subset h_ss hx)
  (hC.pairwiseDisjoint_disjointOfUnion_of_mem h_ss hx) (h_ss hx)
  (fun _ s ↦ hC.subset_of_mem_disjointOfUnion h_ss hx s)

Result:
no goals