-- Module: Mathlib.MeasureTheory.Measure.Restrict
Goal:
α : Type u_2
ι : Type u_6
x : MeasurableSpace α
μ : Measure α
s : ι → Set α
M : ℕ
hs_meas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (y : α), encard.{u_6} (α := ι) {i : ι | y ∈ s i} ≤ (↑M : ℕ∞)
refine :
  ∀ (t : Set α) (ht : MeasurableSet t),
    LE.le (α := ℝ≥0∞) (∑' (i : ι), (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      ((M • μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
refine₁ :
  ∀ (t : Set α) (ht : MeasurableSet t) (F : Finset ι),
    LE.le (α := ℝ≥0∞) (∑ i ∈ F, (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      ((M • μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
refine₂ refine₃ refine₄ :
  ∀ (t : Set α) (ht : MeasurableSet t) (F : Finset ι),
    LE.le (α := ℝ≥0∞) (∑ i ∈ F, (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
      ((M • μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
refine₅ :
  ∀ (t : Set α) (ht : MeasurableSet t) (F : Finset ι),
    let P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ;
    ∀ (P_meas : ∀ (C : Finset ι), MeasurableSet (P C)),
      LE.le (α := ℝ≥0∞) (∑ i ∈ F, (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
        ((M • μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
refine₆ :
  ∀ (t : Set α) (ht : MeasurableSet t) (F : Finset ι),
    let P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ;
    let G : (i : ι) → Set (Finset ι) := fun (i : ι) ↦ {C : Finset ι | C ∈ F.powerset ∧ i ∈ C};
    ∀ (P_meas : ∀ (C : Finset ι), MeasurableSet (P C)) (P_cover : ∀ {i : ι} (hi : i ∈ F), s i ⊆ ⋃ C ∈ G i, P C),
      LE.le (α := ℝ≥0∞) (∑ i ∈ F, (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
        ((M • μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
refine₇ :
  ∀ (t : Set α) (ht : MeasurableSet t) (F : Finset ι),
    let P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ;
    let Cs := F.powerset \ {∅};
    let G : (i : ι) → Set (Finset ι) := fun (i : ι) ↦ {C : Finset ι | C ∈ F.powerset ∧ i ∈ C};
    ∀ (P_meas : ∀ (C : Finset ι), MeasurableSet (P C)) (P_cover : ∀ {i : ι} (hi : i ∈ F), s i ⊆ ⋃ C ∈ G i, P C)
      (iUnion_P : Subset.{u_2} (α := Set α) (⋃ C ∈ Cs, P C) (⋃ (i : ι), s i)),
      LE.le (α := ℝ≥0∞) (∑ i ∈ F, (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
        ((M • μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
refine₈ :
  ∀ (t : Set α) (ht : MeasurableSet t) (F : Finset ι),
    let P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ;
    let Cs := F.powerset \ {∅};
    let G : (i : ι) → Set (Finset ι) := fun (i : ι) ↦ {C : Finset ι | C ∈ F.powerset ∧ i ∈ C};
    ∀ (P_meas : ∀ (C : Finset ι), MeasurableSet (P C)) (P_cover : ∀ {i : ι} (hi : i ∈ F), s i ⊆ ⋃ C ∈ G i, P C)
      (iUnion_P : Subset.{u_2} (α := Set α) (⋃ C ∈ Cs, P C) (⋃ (i : ι), s i))
      (P_subset_s : ∀ {i : ι} {C : Finset ι} (hiC : i ∈ C), P C ⊆ s i),
      LE.le (α := ℝ≥0∞) (∑ i ∈ F, (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
        ((M • μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
refine₉ :
  ∀ (t : Set α) (ht : MeasurableSet t) (F : Finset ι),
    let P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ;
    let Cs := F.powerset \ {∅};
    let G : (i : ι) → Set (Finset ι) := fun (i : ι) ↦ {C : Finset ι | C ∈ F.powerset ∧ i ∈ C};
    ∀ (P_meas : ∀ (C : Finset ι), MeasurableSet (P C)) (P_cover : ∀ {i : ι} (hi : i ∈ F), s i ⊆ ⋃ C ∈ G i, P C)
      (iUnion_P : Subset.{u_2} (α := Set α) (⋃ C ∈ Cs, P C) (⋃ (i : ι), s i))
      (P_subset_s : ∀ {i : ι} {C : Finset ι} (hiC : i ∈ C), P C ⊆ s i)
      (mem_C : ∀ {i : ι} (hi : i ∈ F) {C : Finset ι} {x : α} (hx : x ∈ P C) (hxs : x ∈ s i), i ∈ C),
      LE.le (α := ℝ≥0∞) (∑ i ∈ F, (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
        ((M • μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
refine₁₀ :
  ∀ (t : Set α) (ht : MeasurableSet t) (F : Finset ι),
    let P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ;
    let Cs := F.powerset \ {∅};
    let G : (i : ι) → Set (Finset ι) := fun (i : ι) ↦ {C : Finset ι | C ∈ F.powerset ∧ i ∈ C};
    ∀ (P_meas : ∀ (C : Finset ι), MeasurableSet (P C)) (P_cover : ∀ {i : ι} (hi : i ∈ F), s i ⊆ ⋃ C ∈ G i, P C)
      (iUnion_P : Subset.{u_2} (α := Set α) (⋃ C ∈ Cs, P C) (⋃ (i : ι), s i))
      (P_subset_s : ∀ {i : ι} {C : Finset ι} (hiC : i ∈ C), P C ⊆ s i)
      (mem_C : ∀ {i : ι} (hi : i ∈ F) {C : Finset ι} {x : α} (hx : x ∈ P C) (hxs : x ∈ s i), i ∈ C)
      (C_subset_C : ∀ {C₁ C₂ : Finset ι} (hC₁ : C₁ ∈ Cs) {x : α} (hx : x ∈ P C₁ ∩ P C₂), C₁ ⊆ C₂),
      LE.le (α := ℝ≥0∞) (∑ i ∈ F, (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
        ((M • μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (sum fun (i : ι) ↦ μ.restrict (s i)) ≤ M • μ.restrict (⋃ (i : ι), s i)

Tactic:
classical
  refine le_iff.mpr (fun t ht ↦ le_of_eq_of_le (sum_apply _ ht) ?_)
  refine ENNReal.summable.tsum_le_of_sum_le (fun F ↦ ?_)
  -- `P` is a partition of `⋃ i ∈ F, s i` indexed by `C ∈ Cs` (nonempty subsets of `F`).
  -- `P` is a partition of `s i` when restricted to `C ∈ G i` (subsets of `F` containing `i`).
  let P (C : Finset ι) := (⋂ i ∈ C, s i) ∩ (⋂ i ∈ (F \ C), (s i)ᶜ)
  let Cs := F.powerset \ {∅}
  let G (i : ι) := { C | C ∈ F.powerset ∧ i ∈ C }
  have P_meas C : MeasurableSet (P C) :=
    measurableSet_biInter C (fun i _ ↦ hs_meas i) |>.inter <|
      measurableSet_biInter _ (fun i _ ↦ (hs_meas i).compl)
  have P_cover {i : ι} (hi : i ∈ F) : s i ⊆ ⋃ C ∈ G i, P C := by
    refine fun x hx ↦ Set.mem_biUnion (x := F.filter (x ∈ s ·)) ?_ ?_
    · exact ⟨Finset.mem_powerset.mpr (filter_subset _ F), mem_filter.mpr ⟨hi, hx⟩⟩
    · simp_rw [P, mem_inter_iff, mem_iInter, Finset.mem_sdiff, mem_filter]; tauto
  have iUnion_P : ⋃ C ∈ Cs, P C ⊆ ⋃ i, s i := by
    intro x hx
    simp_rw [Cs, toFinset_diff, Finset.mem_sdiff, mem_iUnion] at hx
    have ⟨C, ⟨_, C_nonempty⟩, hxC⟩ := hx
    have ⟨i, hi⟩ := Finset.nonempty_iff_ne_empty.mpr <| Finset.notMem_singleton.mp C_nonempty
    exact ⟨s i, ⟨i, rfl⟩, hxC.1 (s i) ⟨i, by simp [hi]⟩⟩
  have P_subset_s {i : ι} {C : Finset ι} (hiC : i ∈ C) : P C ⊆ s i := by
    intro x hx
    simp only [P, mem_inter_iff, mem_iInter] at hx
    exact hx.1 i hiC
  have mem_C {i} (hi : i ∈ F) {C : Finset ι} {x : α} (hx : x ∈ P C) (hxs : x ∈ s i) : i ∈ C := by
    rw [mem_inter_iff, mem_iInter₂, mem_iInter₂] at hx
    exact of_not_not fun h ↦ hx.2 i (mem_sdiff.mpr ⟨hi, h⟩) hxs
  have C_subset_C {C₁ C₂} (hC₁ : C₁ ∈ Cs) {x : α} (hx : x ∈ P C₁ ∩ P C₂) : C₁ ⊆ C₂ :=
    fun i hi ↦ mem_C (mem_powerset.mp (sdiff_subset hC₁) hi) hx.2 <| P_subset_s hi hx.1
  calc ∑ i ∈ F, (μ.restrict (s i)) t
    _ ≤ ∑ i ∈ F, Measure.sum (fun (C : G i) ↦ μ.restrict (P C)) t :=
      F.sum_le_sum fun i hi ↦ (restrict_mono_set μ (P_cover hi) t).trans <|
        restrict_biUnion_le ((finite_toSet F.powerset).subset (sep_subset _ _)).countable t
    _ = ∑ i ∈ F, ∑' (C : G i), μ.restrict (P C) t := by simp_rw [Measure.sum_apply _ ht]
    _ = ∑' C, ∑ i ∈ F, (G i).indicator (fun C ↦ μ.restrict (P C) t) C := by
      rw [Summable.tsum_finsetSum (fun _ _ ↦ ENNReal.summable)]
      congr with i
      rw [tsum_subtype (G i) (fun C ↦ (μ.restrict (P C)) t)]
    _ = ∑ C ∈ Cs, ∑ i ∈ F, (C : Set ι).indicator (fun _ ↦ (μ.restrict (P C)) t) i := by
      rw [sum_eq_tsum_indicator]
      congr with C
      by_cases hC : C ∈ F.powerset <;> by_cases hC' : C = ∅ <;>
        simp [hC, hC', Cs, G, indicator, -Finset.mem_powerset, -coe_powerset]
    _ = ∑ C ∈ Cs, {a ∈ F | a ∈ C}.card • μ.restrict (P C) t := by simp [indicator]; rfl
    _ ≤ ∑ C ∈ Cs, M • μ.restrict (P C) t := by
      refine sum_le_sum fun C hC ↦ ?_
      by_cases hPC : P C = ∅
      · simp [hPC]
      have hCM : (C : Set ι).encard ≤ M :=
        have ⟨x, hx⟩ := Set.nonempty_iff_ne_empty.mpr hPC
        (encard_mono (mem_iInter₂.mp hx.1)).trans (hs x)
      exact nsmul_le_nsmul_left zero_le <| calc {a ∈ F | a ∈ C}.card
        _ ≤ C.card := card_mono <| fun i hi ↦ (F.mem_filter.mp hi).2
        _ = (C : Set ι).ncard := (ncard_coe_finset C).symm
        _ ≤ M := ENat.toNat_le_of_le_coe hCM
    _ = M • (μ.restrict (⋃ C ∈ Cs, (P C)) t) := by
      rw [← smul_sum, ← Cs.tsum_subtype, μ.restrict_biUnion_finset _ P_meas, Measure.sum_apply _ ht]
      refine fun C₁ hC₁ C₂ hC₂ hC ↦ Set.disjoint_iff.mpr fun x hx ↦ hC <| ?_
      exact subset_antisymm (C_subset_C hC₁ hx) (C_subset_C hC₂ (Set.inter_comm _ _ ▸ hx))
    _ ≤ (M • μ.restrict (⋃ i, s i)) t := by
      rw [Measure.smul_apply]
      exact nsmul_le_nsmul_right (μ.restrict_mono_set iUnion_P t) M

Premises used: Iff.mpr, MeasureTheory.Measure.sum_apply, ENNReal.summable, Summable.tsum_le_of_sum_le, MeasureTheory.Measure.le_iff, le_of_eq_of_le