awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hC : C ∈ F.powerset
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ 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)
have 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)
Tactic: by_cases hC' : C = ∅
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hC' : C = ∅
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ 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)
have 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)
Tactic: by_cases hC' : C = ∅
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases hC' : C = ∅
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
    (∑ 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∞))
have 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∞))
Tactic: simp [indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞))
have 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∞)
Tactic: refine sum_le_sum fun C hC ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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
⊢ 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∞)
have 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∞)
Tactic: by_cases hPC : P C = ∅
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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∞)
⊢ 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∞)
have 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∞)
Tactic: by_cases hPC : P C = ∅
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (hypothesis)
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∞)
have hCM : (↑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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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 ∈ 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∞)
have rw : (↑Cs : Set (Finset ι)).Pairwise (Disjoint on P)
Tactic: rw [← smul_sum, ← Cs.tsum_subtype, μ.restrict_biUnion_finset _ P_meas, Measure.sum_apply _ ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
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₂
⊢ (↑Cs : Set (Finset ι)).Pairwise (Disjoint on P)
have refine : ∀ (C₁ : Finset ι) (hC₁ : C₁ ∈ (↑Cs : Set (Finset ι))) (C₂ : Finset ι) (hC₂ : C₂ ∈ (↑Cs : Set (Finset ι))) (hC : C₁ ≠ C₂)
  (x : α) (hx : x ∈ P C₁ ∩ P C₂), C₁ = C₂
Tactic: refine fun C₁ hC₁ C₂ hC₂ hC ↦ Set.disjoint_iff.mpr fun x hx ↦ hC <| ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
⊢ 𝒜.Nonempty
have rcases : ∀ (t : Set X) (ht : t ∈ 𝒜), 𝒜.Nonempty
Tactic: rcases h𝒜.approx ∅ MeasurableSet.empty (by simp) 1 (by simp) with ⟨t, ht, -⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
⊢ Set.Nonempty.{u_1} (α := Set X) {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
have rcases : ∀ (t : Set X) (ht : t ∈ 𝒜) (hμt : (μ : (a : Set X) → ℝ≥0∞) (∅ ∆ t) < ENNReal.ofReal 1),
  Set.Nonempty.{u_1} (α := Set X) {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
Tactic: rcases h𝒜.approx ∅ MeasurableSet.empty (by simp) 1 (by simp) with ⟨t, ht, hμt⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
hμt : (μ : (a : Set X) → ℝ≥0∞) (∅ ∆ t) < ENNReal.ofReal 1
⊢ Set.Nonempty.{u_1} (α := Set X) {s : Set X | s ∈ 𝒜 ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
have refine : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine ⟨t, ht, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
hμt : (μ : (a : Set X) → ℝ≥0∞) (∅ ∆ t) < ENNReal.ofReal 1
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
have h : t = ∅ ∆ t
Tactic: convert! ne_top_of_lt hμt
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
hμt : (μ : (a : Set X) → ℝ≥0∞) (∅ ∆ t) < ENNReal.ofReal 1
⊢ t = ∅ ∆ t
have h : t = ⊥ ∆ t
Tactic: rw [← bot_eq_empty, bot_symmDiff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
t : Set X
ht : t ∈ 𝒜
hμt : (μ : (a : Set X) → ℝ≥0∞) (∅ ∆ t) < ENNReal.ofReal 1
h : t = ⊥ ∆ t
⊢ t = ∅ ∆ t
have h₁ : t = t
Tactic: rw [← bot_eq_empty, bot_symmDiff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set (NullMeasurableSpace X μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
⊢ ∃ t ∈ 𝒜, (μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have obtain : ∀ (t : Set X) (ht : t ∈ 𝒜) (hμst : (μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s ∆ t) < ENNReal.ofReal ε),
  ∃ t ∈ 𝒜, (μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
Tactic: obtain ⟨t, ht, hμst⟩ :=
      h𝒜.approx (toMeasurable μ s) (measurableSet_toMeasurable μ s) (by simpa) ε ε_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set (NullMeasurableSpace X μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
t : Set X
ht : t ∈ 𝒜
hμst : (μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s ∆ t) < ENNReal.ofReal ε
⊢ ∃ t ∈ 𝒜, (μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have refine : (μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
Tactic: refine ⟨t, ht, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set (NullMeasurableSpace X μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
t : Set X
ht : t ∈ 𝒜
hμst : (μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s ∆ t) < ENNReal.ofReal ε
⊢ (μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) (s ∆ t) < ENNReal.ofReal ε
have h : Eq (α := ℝ≥0∞) ((μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) (s ∆ t) : ℝ≥0∞)
  ((μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s ∆ t) : ℝ≥0∞)
Tactic: convert! hμst using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.SeparableMeasure (goal)
Goal:
X : Type u_1
m : MeasurableSpace X
μ : Measure X
𝒜 : Set (Set X)
h𝒜 : μ.MeasureDense 𝒜
s : Set (NullMeasurableSpace X μ)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ε : ℝ
ε_pos : 0 < ε
t : Set X
ht : t ∈ 𝒜
hμst : (μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s ∆ t) < ENNReal.ofReal ε
⊢ Eq (α := ℝ≥0∞) ((μ.completion : (a : Set (NullMeasurableSpace X μ)) → ℝ≥0∞) (s ∆ t) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s ∆ t) : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (s ∆ t) : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (toMeasurable μ s ∆ t) : ℝ≥0∞)
Tactic: rw [completion_apply]