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_1 : 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)
i : ι
hi : i ∈ F
x : α
hx : x ∈ s i
refine_2 : ∀ (i : ι) (i_1 : i ∈ F ∧ x ∈ s i), x ∈ s i
refine_2₁ : ∀ (i : ι) (i_1 : i ∈ F ∧ ¬(i ∈ F ∧ x ∈ s i)), x ∈ (s i)ᶜ
refine_2₂ refine_2₃ refine_2₄ : ∀ (i : ι), i ∈ F ∧ x ∈ s i → x ∈ s i
refine_2₅ refine_2₆ refine_2₇ : ∀ (i : ι), i ∈ F ∧ ¬(i ∈ F ∧ x ∈ s i) → x ∈ (s i)ᶜ
refine_2₈ refine_2₉ refine_2₁₀ : ∀ i ∈ F, x ∈ s i → x ∈ s i
⊢ (∀ (i : ι) (i_1 : i ∈ F ∧ x ∈ s i), x ∈ s i) ∧ ∀ (i : ι) (i_1 : i ∈ F ∧ ¬(i ∈ F ∧ x ∈ s i)), x ∈ (s i)ᶜ
have refine_2₁₁ : ∀ (i : ι), x ∈ s i → i ∈ F → ¬(i ∈ F ∧ x ∈ s i) → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
x_1 : 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)
i : ι
hi : i ∈ F
x : α
hx : x ∈ s i
refine_2 : ∀ (i : ι) (i_1 : i ∈ F ∧ x ∈ s i), x ∈ s i
refine_2₁ : ∀ (i : ι) (i_1 : i ∈ F ∧ ¬(i ∈ F ∧ x ∈ s i)), x ∈ (s i)ᶜ
refine_2₂ refine_2₃ refine_2₄ : ∀ (i : ι), i ∈ F ∧ x ∈ s i → x ∈ s i
refine_2₅ refine_2₆ refine_2₇ : ∀ (i : ι), i ∈ F ∧ ¬(i ∈ F ∧ x ∈ s i) → x ∈ (s i)ᶜ
refine_2₈ refine_2₉ refine_2₁₀ : ∀ i ∈ F, x ∈ s i → x ∈ s i
refine_2₁₁ refine_2₁₂ refine_2₁₃ : ∀ (i : ι), x ∈ s i → i ∈ F → ¬(i ∈ F ∧ x ∈ s i) → False
⊢ (∀ (i : ι) (i_1 : i ∈ F ∧ x ∈ s i), x ∈ s i) ∧ ∀ (i : ι) (i_1 : i ∈ F ∧ ¬(i ∈ F ∧ x ∈ s i)), x ∈ (s i)ᶜ
have refine_2₁₄ : ∀ (i : ι), x ∈ s i → i ∈ F → i ∉ F → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
x_1 : 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)
i : ι
hi : i ∈ F
x : α
hx : x ∈ s i
refine_2 : ∀ (i : ι) (i_1 : i ∈ F ∧ x ∈ s i), x ∈ s i
refine_2₁ : ∀ (i : ι) (i_1 : i ∈ F ∧ ¬(i ∈ F ∧ x ∈ s i)), x ∈ (s i)ᶜ
refine_2₂ refine_2₃ refine_2₄ : ∀ (i : ι), i ∈ F ∧ x ∈ s i → x ∈ s i
refine_2₅ refine_2₆ refine_2₇ : ∀ (i : ι), i ∈ F ∧ ¬(i ∈ F ∧ x ∈ s i) → x ∈ (s i)ᶜ
refine_2₈ refine_2₉ refine_2₁₀ : ∀ i ∈ F, x ∈ s i → x ∈ s i
refine_2₁₁ refine_2₁₂ refine_2₁₃ : ∀ (i : ι), x ∈ s i → i ∈ F → ¬(i ∈ F ∧ x ∈ s i) → False
refine_2₁₄ : ∀ (i : ι), x ∈ s i → i ∈ F → i ∉ F → False
⊢ (∀ (i : ι) (i_1 : i ∈ F ∧ x ∈ s i), x ∈ s i) ∧ ∀ (i : ι) (i_1 : i ∈ F ∧ ¬(i ∈ F ∧ x ∈ s i)), x ∈ (s i)ᶜ
have refine_2₁₅ : ∀ (i : ι), x ∈ s i → i ∈ F → x ∉ s i → False
Tactic: tauto
-- 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)
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ F, (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((M • μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have P_cover : ∀ {i : ι} (hi : i ∈ F), s i ⊆ ⋃ C ∈ G i, P C
Tactic: 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (hypothesis)
Goal:
α : Type u_2
ι : Type u_6
x_1 : 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
x : α
hx : Membership.mem (γ := Set α) (⋃ C ∈ Cs, P C) x
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
have hx₁ : ∃ (i : Finset ι) (_ : i ∈ F.powerset ∧ i ∉ {∅}), x ∈ P i
Tactic: simp_rw [Cs, toFinset_diff, Finset.mem_sdiff, mem_iUnion] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
x_1 : 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
x : α
hx : ∃ (i : Finset ι) (_ : i ∈ F.powerset ∧ i ∉ {∅}), x ∈ P i
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
have have : ∀ C ∈ F.powerset, ∀ (C_nonempty : C ∉ {∅}) (hxC : x ∈ P C), Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
Tactic: have ⟨C, ⟨_, C_nonempty⟩, hxC⟩ := hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (goal)
Goal:
α : Type u_2
ι : Type u_6
x_1 : 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
x : α
hx : ∃ (i : Finset ι) (_ : i ∈ F.powerset ∧ i ∉ {∅}), x ∈ P i
C : Finset ι
left : C ∈ F.powerset
C_nonempty : C ∉ {∅}
hxC : x ∈ P C
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
have have : ∀ (i : ι) (hi : i ∈ C), Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
Tactic: have ⟨i, hi⟩ := Finset.nonempty_iff_ne_empty.mpr <| Finset.notMem_singleton.mp C_nonempty
-- 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
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ F, (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((M • μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have iUnion_P : Subset.{u_2} (α := Set α) (⋃ C ∈ Cs, P C) (⋃ (i : ι), s i)
Tactic: 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]⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (hypothesis)
Goal:
α : Type u_2
ι : Type u_6
x_1 : 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)
i : ι
C : Finset ι
hiC : i ∈ C
x : α
hx : x ∈ P C
⊢ x ∈ s i
have hx₁ : (∀ (i : ι) (i_1 : i ∈ C), x ∈ s i) ∧ ∀ (i : ι) (i_1 : i ∈ F \ C), x ∈ (s i)ᶜ
Tactic: simp only [P, mem_inter_iff, mem_iInter] at hx
Cleared hypotheses: hx
-- 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)
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ F, (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((M • μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have P_subset_s : ∀ {i : ι} {C : Finset ι} (hiC : i ∈ C), P C ⊆ s i
Tactic: 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Restrict (hypothesis)
Goal:
α : Type u_2
ι : Type u_6
x_1 : 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
i : ι
hi : i ∈ F
C : Finset ι
x : α
hx : x ∈ P C
hxs : x ∈ s i
⊢ i ∈ C
have hx₁ : (∀ (i : ι) (j : i ∈ C), x ∈ s i) ∧ ∀ (i : ι) (j : i ∈ F \ C), x ∈ (s i)ᶜ
Tactic: rw [mem_inter_iff, mem_iInter₂, mem_iInter₂] at hx
Cleared hypotheses: hx, hxs
-- 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
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ F, (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((M • μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have mem_C : ∀ {i : ι} (hi : i ∈ F) {C : Finset ι} {x : α} (hx : x ∈ P C) (hxs : x ∈ s i), i ∈ C
Tactic: 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
-- 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
⊢ LE.le (α := ℝ≥0∞) (∑ i ∈ F, (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
    ((M • μ.restrict (⋃ (i : ι), s i) : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have C_subset_C : ∀ {C₁ C₂ : Finset ι} (hC₁ : C₁ ∈ Cs) {x : α} (hx : x ∈ P C₁ ∩ P C₂), C₁ ⊆ C₂
Tactic: 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
-- 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∞) (∑ 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)
have rw : Eq (α := ℝ≥0∞) (∑ i ∈ F, ∑' (C : (↑(G i) : Type u_6)), (μ.restrict (P (↑C : Finset ι)) : (a : Set α) → ℝ≥0∞) t)
  (∑ i ∈ F, ∑' (b : Finset ι), (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) b)
Tactic: rw [Summable.tsum_finsetSum (fun _ _ ↦ ENNReal.summable)]
-- 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∞) (∑ i ∈ F, ∑' (C : (↑(G i) : Type u_6)), (μ.restrict (P (↑C : Finset ι)) : (a : Set α) → ℝ≥0∞) t)
    (∑ i ∈ F, ∑' (b : Finset ι), (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) b)
have e_f : ∀ (i : ι),
  Eq (α := ℝ≥0∞) (∑' (C : (↑(G i) : Type u_6)), (μ.restrict (P (↑C : Finset ι)) : (a : Set α) → ℝ≥0∞) t)
    (∑' (b : Finset ι), (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) b)
Tactic: congr with i
-- 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₂
i : ι
⊢ Eq (α := ℝ≥0∞) (∑' (C : (↑(G i) : Type u_6)), (μ.restrict (P (↑C : Finset ι)) : (a : Set α) → ℝ≥0∞) t)
    (∑' (b : Finset ι), (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) b)
have e_f : Eq (α := ℝ≥0∞)
  (∑' (x_1 : Finset ι), (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) x_1)
  (∑' (b : Finset ι), (G i).indicator (fun (C : Finset ι) ↦ (μ.restrict (P C) : (a : Set α) → ℝ≥0∞) t) b)
Tactic: rw [tsum_subtype (G i) (fun C ↦ (μ.restrict (P C)) t)]
-- 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 : 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)
have 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)
Tactic: rw [sum_eq_tsum_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₂
⊢ 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)
have 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)
Tactic: congr with 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 ι
⊢ 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 ∈ 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