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)
⊢ ∀ {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
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
⊢ ∃ (i : Finset ι) (_ : i ∈ F.powerset ∧ i ∉ {∅}), x ∈ P i

Tactic:
simp_rw [Cs, toFinset_diff, Finset.mem_sdiff, mem_iUnion] at hx

Premises used: Set.toFinset_diff, Set.mem_iUnion, Finset.mem_sdiff
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
have : ∀ C ∈ F.powerset, ∀ (C_nonempty : C ∉ {∅}) (hxC : x ∈ P C), Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x

Tactic:
have ⟨C, ⟨_, C_nonempty⟩, hxC⟩ := hx
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
have : ∀ (i : ι) (hi : i ∈ C), Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x

Tactic:
have ⟨i, hi⟩ := Finset.nonempty_iff_ne_empty.mpr <| Finset.notMem_singleton.mp C_nonempty
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
i : ι
hi : i ∈ C
⊢ (fun (i : ι) ↦ (⋂ (_ : i ∈ C), s i : Set α)) i = s i

Tactic:
simp [hi]
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
i : ι
hi : i ∈ C
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), s i) x

Tactic:
exact ⟨s i, ⟨i, rfl⟩, hxC.1 (s i) ⟨i, by simp [hi]⟩⟩
-- 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
⊢ 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]⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
⊢ (∀ (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

Premises used: Set.mem_inter_iff, Set.mem_iInter
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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 : (∀ (i : ι) (i_1 : i ∈ C), x ∈ s i) ∧ ∀ (i : ι) (i_1 : i ∈ F \ C), x ∈ (s i)ᶜ
⊢ x ∈ s i

Tactic:
hx.1 i hiC

Premises used: And.left
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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 : (∀ (i : ι) (i_1 : i ∈ C), x ∈ s i) ∧ ∀ (i : ι) (i_1 : i ∈ F \ C), x ∈ (s i)ᶜ
⊢ x ∈ s i

Tactic:
exact hx.1 i hiC

Premises used: And.left
-- 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)
⊢ ∀ {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
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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 : ι) (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

Premises used: Set.mem_inter_iff, Set.mem_iInter₂
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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
hx₁ : (∀ (i : ι) (j : i ∈ C), x ∈ s i) ∧ ∀ (i : ι) (j : i ∈ F \ C), x ∈ (s i)ᶜ
⊢ x ∈ s i

Tactic:
rw [mem_inter_iff, mem_iInter₂, mem_iInter₂] at hx

Premises used: Set.mem_inter_iff, Set.mem_iInter₂
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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 : (∀ (i : ι) (j : i ∈ C), x ∈ s i) ∧ ∀ (i : ι) (j : i ∈ F \ C), x ∈ (s i)ᶜ
hxs : x ∈ s i
⊢ i ∈ C

Tactic:
of_not_not fun h ↦ hx.2 i (mem_sdiff.mpr ⟨hi, h⟩) hxs

Premises used: Iff.mpr, Finset.mem_sdiff, And.right, And.intro, of_not_not
-- Module: Mathlib.MeasureTheory.Measure.Restrict
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 : (∀ (i : ι) (j : i ∈ C), x ∈ s i) ∧ ∀ (i : ι) (j : i ∈ F \ C), x ∈ (s i)ᶜ
hxs : x ∈ s i
⊢ i ∈ C

Tactic:
exact of_not_not fun h ↦ hx.2 i (mem_sdiff.mpr ⟨hi, h⟩) hxs

Premises used: Iff.mpr, Finset.mem_sdiff, And.right, And.intro, of_not_not
-- 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
⊢ ∀ {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
-- 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₁ 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
-- 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∞) (∑ i ∈ F, (μ.restrict (s i) : (a : Set α) → ℝ≥0∞) t)
    (∑ i ∈ F, ((sum fun (C : (↑(G i) : Type u_6)) ↦ μ.restrict (P (↑C : Finset ι)) : Measure α) : (a : Set α) → ℝ≥0∞) t)

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

Premises used: MeasureTheory.Measure.restrict_biUnion_le, Membership.mem, MeasureTheory.Measure.restrict_mono_set, Set.Finite.subset, SetLike.coe, Finset.powerset, Finset.sum_le_sum, Finset.finite_toSet, LE.le.trans, Set.sep_subset, Set.Finite.countable
-- 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∞)
    (∑ 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)

Tactic:
simp_rw [Measure.sum_apply _ ht]

Premises used: MeasureTheory.Measure.sum_apply
-- 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∞) (∑ 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)
⊢ 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)

Tactic:
rw [Summable.tsum_finsetSum (fun _ _ ↦ ENNReal.summable)]

Premises used: ENNReal.summable, Summable.tsum_finsetSum
-- 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 :
  ∀ (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)
⊢ 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:
congr with i
-- 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₂
i : ι
e_f 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)
⊢ 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:
rw [tsum_subtype (G i) (fun C ↦ (μ.restrict (P C)) t)]

Premises used: tsum_subtype, MeasureTheory.Measure.restrict, DFunLike.coe