-- 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 : ℕ∞)
t : Set α
ht : MeasurableSet t
F : Finset ι
P : (C : Finset ι) → Set α := fun (C : Finset ι) ↦ (⋂ i ∈ C, s i) ∩ ⋂ i ∈ F \ C, (s i)ᶜ
Cs : Finset (Finset ι) := F.powerset \ {∅}
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₂
calc :
  Eq (α := ℝ≥0∞)
    (∑ i ∈ F, ((sum fun (C : (↑(G i) : Type u_6)) ↦ μ.restrict (P (↑C : Finset ι)) : Measure α) : (a : Set α) → ℝ≥0∞) t)
    (∑ i ∈ F, ∑' (C : (↑(G i) : Type u_6)), (μ.restrict (P (↑C : Finset ι)) : (a : Set α) → ℝ≥0∞) t)
calc₁ :
  Eq (α := ℝ≥0∞) (∑ i ∈ F, ∑' (C : (↑(G i) : Type u_6)), (μ.restrict (P (↑C : Finset ι)) : (a : Set α) → ℝ≥0∞) t)
    (∑' (C : Finset ι), ∑ i ∈ F, (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) C)
calc₂ :
  Eq (α := ℝ≥0∞)
    (∑' (C : Finset ι), ∑ i ∈ F, (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) C)
    (∑ C ∈ Cs, ∑ i ∈ F, (↑C : Set ι).indicator (fun (x_1 : ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) i)
calc₃ :
  Eq (α := ℝ≥0∞)
    (∑ C ∈ Cs, ∑ i ∈ F, (↑C : Set ι).indicator (fun (x_1 : ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) i)
    (∑ C ∈ Cs, HSMul.hSMul (β := ℝ≥0∞) (#({a ∈ F | a ∈ C})) ((μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞))
calc₄ :
  LE.le (α := ℝ≥0∞)
    (∑ C ∈ Cs, HSMul.hSMul (β := ℝ≥0∞) (#({a ∈ F | a ∈ C})) ((μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞))
    (∑ C ∈ Cs, HSMul.hSMul (β := ℝ≥0∞) M ((μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞))
calc₅ :
  ∑ C ∈ Cs, HSMul.hSMul (β := ℝ≥0∞) M ((μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    HSMul.hSMul (β := ℝ≥0∞) M ((μ.restrict (⋃ C ∈ Cs, P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
calc₆ :
  HSMul.hSMul (β := ℝ≥0∞) M ((μ.restrict (⋃ C ∈ Cs, P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    (M • μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ F, (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((M • μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
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: MeasureTheory.Measure.restrict_biUnion_le, Membership.mem, MeasureTheory.Measure.restrict_mono_set, MeasureTheory.Measure.restrict, Set.Finite.subset, SetLike.coe, Finset.powerset, Finset.sum_le_sum, HSMul.hSMul, Finset.finite_toSet, LE.le.trans, Set.sep_subset, DFunLike.coe, Set.iUnion, Set.Finite.countable