-- Mathlib/MeasureTheory/Measure/AddContent.lean
lemma addContent_le_sum_of_subset_sUnion {m : AddContent C} (hC : IsSetSemiring C)
    {J : Finset (Set α)} (h_ss : ↑J ⊆ C) (ht : t ∈ C) (htJ : t ⊆ ⋃₀ ↑J) :
    m t ≤ ∑ u ∈ J, m u

Proof state:
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
⊢ m t ≤ ∑ u ∈ J, m u

Tactic:
have ht_eq : t = ⋃₀ Jt := by
  rw [coe_image, sUnion_image, ← inter_iUnion₂, inter_eq_self_of_subset_left]
  rwa [← sUnion_eq_biUnion]

Result:
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
ht_eq : t = ⋃₀ ↑Jt
⊢ m t ≤ ∑ u ∈ J, m u

Proof state:
case refine_2
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
ht_eq : t = ⋃₀ ↑Jt
⊢ ⋃₀ ↑Jt ∈ C

Tactic:
rwa [← ht_eq]

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
⊢ t ⊆ ⋃ i ∈ ↑J, i

Tactic:
rwa [← sUnion_eq_biUnion]

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
⊢ t = ⋃₀ ↑Jt

Tactic:
rw [coe_image, sUnion_image, ← inter_iUnion₂, inter_eq_self_of_subset_left]

Result:
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
⊢ t ⊆ ⋃ i ∈ ↑J, i

Proof state:
case refine_1
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
ht_eq : t = ⋃₀ ↑Jt
⊢ ↑Jt ⊆ C

Tactic:
intro s

Result:
case refine_1
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
ht_eq : t = ⋃₀ ↑Jt
s : Set α
⊢ s ∈ ↑Jt → s ∈ C

Proof state:
case refine_1
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
ht_eq : t = ⋃₀ ↑Jt
s : Set α
⊢ ∀ x ∈ J, t ∩ x = s → s ∈ C

Tactic:
rintro u hu rfl

Result:
case refine_1
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
ht_eq : t = ⋃₀ ↑Jt
u : Set α
hu : u ∈ J
⊢ t ∩ u ∈ C

Proof state:
case refine_1
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
ht_eq : t = ⋃₀ ↑Jt
u : Set α
hu : u ∈ J
⊢ t ∩ u ∈ C

Tactic:
exact hC.inter_mem _ ht _ (h_ss hu)

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
ht_eq : t = ⋃₀ ↑Jt
⊢ m (⋃₀ ↑Jt) ≤ ∑ u ∈ J, m u

Tactic:
refine (addContent_sUnion_le_sum hC Jt ?_ ?_).trans ?_

Result:
case refine_1
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
ht_eq : t = ⋃₀ ↑Jt
⊢ ↑Jt ⊆ C

case refine_2
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
ht_eq : t = ⋃₀ ↑Jt
⊢ ⋃₀ ↑Jt ∈ C

case refine_3
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
ht_eq : t = ⋃₀ ↑Jt
⊢ ∑ u ∈ Jt, m u ≤ ∑ u ∈ J, m u

Proof state:
case refine_3
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
ht_eq : t = ⋃₀ ↑Jt
u : Set α
hu : u ∈ J
⊢ m (t ∩ u) ≤ m u

Tactic:
exact addContent_mono hC (hC.inter_mem _ ht _ (h_ss hu)) (h_ss hu) inter_subset_right

Result:
no goals

Proof state:
case refine_3
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
ht_eq : t = ⋃₀ ↑Jt
⊢ ∑ u ∈ Jt, m u ≤ ∑ u ∈ J, m u

Tactic:
refine (Finset.sum_image_le_of_nonneg fun _ _ ↦ zero_le _).trans (sum_le_sum fun u hu ↦ ?_)

Result:
case refine_3
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
ht_eq : t = ⋃₀ ↑Jt
u : Set α
hu : u ∈ J
⊢ m (t ∩ u) ≤ m u

Proof state:
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
ht_eq : t = ⋃₀ ↑Jt
⊢ m t ≤ ∑ u ∈ J, m u

Tactic:
rw [ht_eq]

Result:
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
ht_eq : t = ⋃₀ ↑Jt
⊢ m (⋃₀ ↑Jt) ≤ ∑ u ∈ J, m u

Proof state:
case refine_1
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
ht_eq : t = ⋃₀ ↑Jt
s : Set α
⊢ s ∈ ↑Jt → s ∈ C

Tactic:
simp only [Jt, coe_image, Set.mem_image, mem_coe, forall_exists_index, and_imp]

Result:
case refine_1
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
ht_eq : t = ⋃₀ ↑Jt
s : Set α
⊢ ∀ x ∈ J, t ∩ x = s → s ∈ C

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

Tactic:
let Jt := J.image (fun u ↦ t ∩ u)

Result:
α : Type u_1
C : Set (Set α)
t : Set α
m : AddContent C
hC : IsSetSemiring C
J : Finset (Set α)
h_ss : ↑J ⊆ C
ht : t ∈ C
htJ : t ⊆ ⋃₀ ↑J
Jt : Finset (Set α) := Finset.image (fun u => t ∩ u) J
⊢ m t ≤ ∑ u ∈ J, m u