-- Mathlib/MeasureTheory/Measure/AddContent.lean
lemma addContent_biUnion_le {ι : Type*} (hC : IsSetRing C) {s : ι → Set α}
    {S : Finset ι} (hs : ∀ n ∈ S, s n ∈ C) :
    m (⋃ i ∈ S, s i) ≤ ∑ i ∈ S, m (s i)

Proof state:
case insert
α : Type u_1
C : Set (Set α)
m : AddContent C
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → m (⋃ i ∈ S, s i) ≤ ∑ i ∈ S, m (s i)
hs : ∀ n ∈ insert i S, s n ∈ C
⊢ m (⋃ i_1 ∈ insert i S, s i_1) ≤ ∑ i ∈ insert i S, m (s i)

Tactic:
rw [Finset.sum_insert hiS]

Result:
case insert
α : Type u_1
C : Set (Set α)
m : AddContent C
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → m (⋃ i ∈ S, s i) ≤ ∑ i ∈ S, m (s i)
hs : ∀ n ∈ insert i S, s n ∈ C
⊢ m (⋃ i_1 ∈ insert i S, s i_1) ≤ m (s i) + ∑ x ∈ S, m (s x)

Proof state:
case empty
α : Type u_1
C : Set (Set α)
m : AddContent C
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
hs : ∀ n ∈ ∅, s n ∈ C
⊢ m (⋃ i ∈ ∅, s i) ≤ ∑ i ∈ ∅, m (s i)

Tactic:
simp

Result:
no goals

Proof state:
case insert
α : Type u_1
C : Set (Set α)
m : AddContent C
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → m (⋃ i ∈ S, s i) ≤ ∑ i ∈ S, m (s i)
hs : ∀ n ∈ insert i S, s n ∈ C
⊢ m (⋃ i_1 ∈ insert i S, s i_1) ≤ m (s i) + ∑ x ∈ S, m (s x)

Tactic:
simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]

Result:
case insert
α : Type u_1
C : Set (Set α)
m : AddContent C
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → m (⋃ i ∈ S, s i) ≤ ∑ i ∈ S, m (s i)
hs : ∀ n ∈ insert i S, s n ∈ C
⊢ m (s i ∪ ⋃ x ∈ ↑S, s x) ≤ m (s i) + ∑ x ∈ S, m (s x)

Proof state:
case insert
α : Type u_1
C : Set (Set α)
m : AddContent C
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → m (⋃ i ∈ S, s i) ≤ ∑ i ∈ S, m (s i)
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
⊢ m (s i) + m (⋃ i ∈ S, s i) ≤ m (s i) + ∑ x ∈ S, m (s x)

Tactic:
exact add_le_add le_rfl (h hs.2)

Result:
no goals

Proof state:
case insert
α : Type u_1
C : Set (Set α)
m : AddContent C
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → m (⋃ i ∈ S, s i) ≤ ∑ i ∈ S, m (s i)
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
⊢ m (s i ∪ ⋃ x ∈ ↑S, s x) ≤ m (s i) + ∑ x ∈ S, m (s x)

Tactic:
refine (addContent_union_le hC hs.1 (hC.biUnion_mem S hs.2)).trans ?_

Result:
case insert
α : Type u_1
C : Set (Set α)
m : AddContent C
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → m (⋃ i ∈ S, s i) ≤ ∑ i ∈ S, m (s i)
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
⊢ m (s i) + m (⋃ i ∈ S, s i) ≤ m (s i) + ∑ x ∈ S, m (s x)

Proof state:
case insert
α : Type u_1
C : Set (Set α)
m : AddContent C
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → m (⋃ i ∈ S, s i) ≤ ∑ i ∈ S, m (s i)
hs : ∀ n ∈ insert i S, s n ∈ C
⊢ m (s i ∪ ⋃ x ∈ ↑S, s x) ≤ m (s i) + ∑ x ∈ S, m (s x)

Tactic:
simp only [Finset.mem_insert, forall_eq_or_imp] at hs

Result:
case insert
α : Type u_1
C : Set (Set α)
m : AddContent C
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
i : ι
S : Finset ι
hiS : i ∉ S
h : (∀ n ∈ S, s n ∈ C) → m (⋃ i ∈ S, s i) ≤ ∑ i ∈ S, m (s i)
hs : s i ∈ C ∧ ∀ a ∈ S, s a ∈ C
⊢ m (s i ∪ ⋃ x ∈ ↑S, s x) ≤ m (s i) + ∑ x ∈ S, m (s x)

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hs : ∀ n ∈ S, s n ∈ C
⊢ m (⋃ i ∈ S, s i) ≤ ∑ i ∈ S, m (s i)

Tactic:
classical
induction S using Finset.induction with
| empty => simp
| @insert i S hiS h =>
  rw [Finset.sum_insert hiS]
  simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
  simp only [Finset.mem_insert, forall_eq_or_imp] at hs
  refine (addContent_union_le hC hs.1 (hC.biUnion_mem S hs.2)).trans ?_
  exact add_le_add le_rfl (h hs.2)

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
m : AddContent C
ι : Type u_2
hC : IsSetRing C
s : ι → Set α
S : Finset ι
hs : ∀ n ∈ S, s n ∈ C
⊢ m (⋃ i ∈ S, s i) ≤ ∑ i ∈ S, m (s i)

Tactic:
induction S using Finset.induction with
| empty => simp
| @insert i S hiS h =>
  rw [Finset.sum_insert hiS]
  simp_rw [← Finset.mem_coe, Finset.coe_insert, Set.biUnion_insert]
  simp only [Finset.mem_insert, forall_eq_or_imp] at hs
  refine (addContent_union_le hC hs.1 (hC.biUnion_mem S hs.2)).trans ?_
  exact add_le_add le_rfl (h hs.2)

Result:
no goals