awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
rw :
  Eq (α := ℝ≥0∞)
    (∑' (C : Finset ι), ∑ i ∈ F, (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) C)
    (∑' (x_1 : Finset ι),
      (↑Cs : Set (Finset ι)).indicator
        (fun (C : Finset ι) ↦
          ∑ i ∈ F, (↑C : Set ι).indicator (fun (x_2 : ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) i)
        x_1)
⊢ 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)

Tactic:
rw [sum_eq_tsum_indicator]

Premises used: sum_eq_tsum_indicator, SummationFilter.unconditional
-- 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₂
e_f :
  ∀ (C : Finset ι),
    Eq (α := ℝ≥0∞) (∑ i ∈ F, (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) C)
      ((↑Cs : Set (Finset ι)).indicator
        (fun (C : Finset ι) ↦
          ∑ i ∈ F, (↑C : Set ι).indicator (fun (x_1 : ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) i)
        C)
⊢ Eq (α := ℝ≥0∞)
    (∑' (C : Finset ι), ∑ i ∈ F, (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) C)
    (∑' (x_1 : Finset ι),
      (↑Cs : Set (Finset ι)).indicator
        (fun (C : Finset ι) ↦
          ∑ i ∈ F, (↑C : Set ι).indicator (fun (x_2 : ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) i)
        x_1)

Tactic:
congr with C
-- 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₂
C : Finset ι
pos :
  ∀ (hC : C ∈ F.powerset),
    Eq (α := ℝ≥0∞) (∑ i ∈ F, (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) C)
      ((↑Cs : Set (Finset ι)).indicator
        (fun (C : Finset ι) ↦
          ∑ i ∈ F, (↑C : Set ι).indicator (fun (x_1 : ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) i)
        C)
neg :
  ∀ (hC : C ∉ F.powerset),
    Eq (α := ℝ≥0∞) (∑ i ∈ F, (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) C)
      ((↑Cs : Set (Finset ι)).indicator
        (fun (C : Finset ι) ↦
          ∑ i ∈ F, (↑C : Set ι).indicator (fun (x_1 : ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) i)
        C)
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ F, (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) C)
    ((↑Cs : Set (Finset ι)).indicator
      (fun (C : Finset ι) ↦
        ∑ i ∈ F, (↑C : Set ι).indicator (fun (x_1 : ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) i)
      C)

Tactic:
by_cases hC : C ∈ F.powerset

Premises used: Finset.powerset
-- 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₂
C : Finset ι
hC : C ∈ F.powerset
pos :
  ∀ (hC' : C = ∅),
    Eq (α := ℝ≥0∞) (∑ i ∈ F, (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) C)
      ((↑Cs : Set (Finset ι)).indicator
        (fun (C : Finset ι) ↦
          ∑ i ∈ F, (↑C : Set ι).indicator (fun (x_1 : ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) i)
        C)
neg :
  ∀ (hC' : ¬C = ∅),
    Eq (α := ℝ≥0∞) (∑ i ∈ F, (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) C)
      ((↑Cs : Set (Finset ι)).indicator
        (fun (C : Finset ι) ↦
          ∑ i ∈ F, (↑C : Set ι).indicator (fun (x_1 : ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) i)
        C)
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ F, (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) C)
    ((↑Cs : Set (Finset ι)).indicator
      (fun (C : Finset ι) ↦
        ∑ i ∈ F, (↑C : Set ι).indicator (fun (x_1 : ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) i)
      C)

Tactic:
by_cases hC' : C = ∅
-- 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₂
C : Finset ι
hC : C ∉ F.powerset
pos :
  ∀ (hC' : C = ∅),
    Eq (α := ℝ≥0∞) (∑ i ∈ F, (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) C)
      ((↑Cs : Set (Finset ι)).indicator
        (fun (C : Finset ι) ↦
          ∑ i ∈ F, (↑C : Set ι).indicator (fun (x_1 : ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) i)
        C)
neg :
  ∀ (hC' : ¬C = ∅),
    Eq (α := ℝ≥0∞) (∑ i ∈ F, (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) C)
      ((↑Cs : Set (Finset ι)).indicator
        (fun (C : Finset ι) ↦
          ∑ i ∈ F, (↑C : Set ι).indicator (fun (x_1 : ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) i)
        C)
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ F, (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) C)
    ((↑Cs : Set (Finset ι)).indicator
      (fun (C : Finset ι) ↦
        ∑ i ∈ F, (↑C : Set ι).indicator (fun (x_1 : ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) i)
      C)

Tactic:
by_cases hC' : C = ∅
-- 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₂
C : Finset ι
hC : C ∈ F.powerset
hC' : C = ∅
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ F, (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) C)
    ((↑Cs : Set (Finset ι)).indicator
      (fun (C : Finset ι) ↦
        ∑ i ∈ F, (↑C : Set ι).indicator (fun (x_1 : ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) i)
      C)

Tactic:
simp [hC, hC', Cs, G, indicator, -Finset.mem_powerset, -coe_powerset]

Premises used: Finset.coe_powerset, Set.indicator, Finset.mem_powerset
-- 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₂
C : Finset ι
hC : C ∈ F.powerset
hC' : ¬C = ∅
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ F, (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) C)
    ((↑Cs : Set (Finset ι)).indicator
      (fun (C : Finset ι) ↦
        ∑ i ∈ F, (↑C : Set ι).indicator (fun (x_1 : ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) i)
      C)

Tactic:
simp [hC, hC', Cs, G, indicator, -Finset.mem_powerset, -coe_powerset]

Premises used: Finset.coe_powerset, Set.indicator, Finset.mem_powerset
-- 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₂
C : Finset ι
hC : C ∉ F.powerset
hC' : C = ∅
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ F, (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) C)
    ((↑Cs : Set (Finset ι)).indicator
      (fun (C : Finset ι) ↦
        ∑ i ∈ F, (↑C : Set ι).indicator (fun (x_1 : ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) i)
      C)

Tactic:
simp [hC, hC', Cs, G, indicator, -Finset.mem_powerset, -coe_powerset]

Premises used: Finset.coe_powerset, Set.indicator, Finset.mem_powerset
-- 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₂
C : Finset ι
hC : C ∉ F.powerset
hC' : ¬C = ∅
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ F, (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) C)
    ((↑Cs : Set (Finset ι)).indicator
      (fun (C : Finset ι) ↦
        ∑ i ∈ F, (↑C : Set ι).indicator (fun (x_1 : ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) i)
      C)

Tactic:
simp [hC, hC', Cs, G, indicator, -Finset.mem_powerset, -coe_powerset]

Premises used: Finset.coe_powerset, Set.indicator, Finset.mem_powerset
-- 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₂
simp :
  Eq (α := ℝ≥0∞)
    (∑ x_1 ∈ Cs,
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(#(F ∩ x_1)) : ℝ≥0∞) : ℝ≥0∞)
        ((μ.restrict (P x_1) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞))
    (∑ x_1 ∈ Cs,
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(#({a ∈ F | a ∈ x_1})) : ℝ≥0∞) : ℝ≥0∞)
        ((μ.restrict (P x_1) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞))
⊢ 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∞))

Tactic:
simp [indicator]

Premises used: Set.indicator
-- 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₂
⊢ Eq (α := ℝ≥0∞)
    (∑ x_1 ∈ Cs,
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(#(F ∩ x_1)) : ℝ≥0∞) : ℝ≥0∞)
        ((μ.restrict (P x_1) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞))
    (∑ x_1 ∈ Cs,
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((↑(#({a ∈ F | a ∈ x_1})) : ℝ≥0∞) : ℝ≥0∞)
        ((μ.restrict (P x_1) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞))

Tactic:
rfl
-- 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₂
⊢ 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∞))

Tactic:
sum_le_sum fun C hC ↦ ?_

Premises used: Finset.sum_le_sum
-- 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₂
refine :
  ∀ (C : Finset ι) (hC : C ∈ Cs),
    HSMul.hSMul (β := ℝ≥0∞) (#({a ∈ F | a ∈ C})) ((μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
      HSMul.hSMul (β := ℝ≥0∞) M ((μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ 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∞))

Tactic:
refine sum_le_sum fun C hC ↦ ?_

Premises used: Finset.sum_le_sum
-- 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₂
C : Finset ι
hC : C ∈ Cs
pos :
  ∀ (hPC : P C = ∅),
    HSMul.hSMul (β := ℝ≥0∞) (#({a ∈ F | a ∈ C})) ((μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
      HSMul.hSMul (β := ℝ≥0∞) M ((μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
neg :
  ∀ (hPC : ¬P C = ∅),
    HSMul.hSMul (β := ℝ≥0∞) (#({a ∈ F | a ∈ C})) ((μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
      HSMul.hSMul (β := ℝ≥0∞) M ((μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ HSMul.hSMul (β := ℝ≥0∞) (#({a ∈ F | a ∈ C})) ((μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    HSMul.hSMul (β := ℝ≥0∞) M ((μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
by_cases hPC : P C = ∅
-- 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₂
C : Finset ι
hC : C ∈ Cs
hPC : P C = ∅
⊢ HSMul.hSMul (β := ℝ≥0∞) (#({a ∈ F | a ∈ C})) ((μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    HSMul.hSMul (β := ℝ≥0∞) M ((μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
simp [hPC]
-- 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₂
C : Finset ι
hC : C ∈ Cs
hPC : ¬P C = ∅
⊢ (↑C : Set ι).encard ≤ (↑M : ℕ∞)

Tactic:
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)