[GOAL]
α : Type u_1
S : Set α
⊢ IsPiSystem {S}
[PROOFSTEP]
intro s h_s t h_t _
[GOAL]
α : Type u_1
S s : Set α
h_s : s ∈ {S}
t : Set α
h_t : t ∈ {S}
a✝ : Set.Nonempty (s ∩ t)
⊢ s ∩ t ∈ {S}
[PROOFSTEP]
rw [Set.mem_singleton_iff.1 h_s, Set.mem_singleton_iff.1 h_t, Set.inter_self, Set.mem_singleton_iff]
[GOAL]
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
⊢ IsPiSystem (insert ∅ S)
[PROOFSTEP]
intro s hs t ht hst
[GOAL]
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert ∅ S
t : Set α
ht : t ∈ insert ∅ S
hst : Set.Nonempty (s ∩ t)
⊢ s ∩ t ∈ insert ∅ S
[PROOFSTEP]
cases' hs with hs hs
[GOAL]
case inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : Set.Nonempty (s ∩ t)
hs : s = ∅
⊢ s ∩ t ∈ insert ∅ S
[PROOFSTEP]
simp [hs]
[GOAL]
case inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert ∅ S
hst : Set.Nonempty (s ∩ t)
hs : s ∈ S
⊢ s ∩ t ∈ insert ∅ S
[PROOFSTEP]
cases' ht with ht ht
[GOAL]
case inr.inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : Set.Nonempty (s ∩ t)
hs : s ∈ S
ht : t = ∅
⊢ s ∩ t ∈ insert ∅ S
[PROOFSTEP]
simp [ht]
[GOAL]
case inr.inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : Set.Nonempty (s ∩ t)
hs : s ∈ S
ht : t ∈ S
⊢ s ∩ t ∈ insert ∅ S
[PROOFSTEP]
exact Set.mem_insert_of_mem _ (h_pi s hs t ht hst)
[GOAL]
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
⊢ IsPiSystem (insert univ S)
[PROOFSTEP]
intro s hs t ht hst
[GOAL]
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s : Set α
hs : s ∈ insert univ S
t : Set α
ht : t ∈ insert univ S
hst : Set.Nonempty (s ∩ t)
⊢ s ∩ t ∈ insert univ S
[PROOFSTEP]
cases' hs with hs hs
[GOAL]
case inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : Set.Nonempty (s ∩ t)
hs : s = univ
⊢ s ∩ t ∈ insert univ S
[PROOFSTEP]
cases' ht with ht ht
[GOAL]
case inl.inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : Set.Nonempty (s ∩ t)
hs : s = univ
ht : t = univ
⊢ s ∩ t ∈ insert univ S
[PROOFSTEP]
simp [hs, ht]
[GOAL]
case inl.inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : Set.Nonempty (s ∩ t)
hs : s = univ
ht : t ∈ S
⊢ s ∩ t ∈ insert univ S
[PROOFSTEP]
simp [hs, ht]
[GOAL]
case inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
ht : t ∈ insert univ S
hst : Set.Nonempty (s ∩ t)
hs : s ∈ S
⊢ s ∩ t ∈ insert univ S
[PROOFSTEP]
cases' ht with ht ht
[GOAL]
case inr.inl
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : Set.Nonempty (s ∩ t)
hs : s ∈ S
ht : t = univ
⊢ s ∩ t ∈ insert univ S
[PROOFSTEP]
simp [hs, ht]
[GOAL]
case inr.inr
α : Type u_1
S : Set (Set α)
h_pi : IsPiSystem S
s t : Set α
hst : Set.Nonempty (s ∩ t)
hs : s ∈ S
ht : t ∈ S
⊢ s ∩ t ∈ insert univ S
[PROOFSTEP]
exact Set.mem_insert_of_mem _ (h_pi s hs t ht hst)
[GOAL]
α : Type u_1
β : Type u_2
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
⊢ IsPiSystem {s | ∃ t, t ∈ S ∧ f ⁻¹' t = s}
[PROOFSTEP]
rintro _ ⟨s, hs_mem, rfl⟩ _ ⟨t, ht_mem, rfl⟩ hst
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
s : Set β
hs_mem : s ∈ S
t : Set β
ht_mem : t ∈ S
hst : Set.Nonempty (f ⁻¹' s ∩ f ⁻¹' t)
⊢ f ⁻¹' s ∩ f ⁻¹' t ∈ {s | ∃ t, t ∈ S ∧ f ⁻¹' t = s}
[PROOFSTEP]
rw [← Set.preimage_inter] at hst ⊢
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
s : Set β
hs_mem : s ∈ S
t : Set β
ht_mem : t ∈ S
hst : Set.Nonempty (f ⁻¹' (s ∩ t))
⊢ f ⁻¹' (s ∩ t) ∈ {s | ∃ t, t ∈ S ∧ f ⁻¹' t = s}
[PROOFSTEP]
refine' ⟨s ∩ t, h_pi s hs_mem t ht_mem _, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
s : Set β
hs_mem : s ∈ S
t : Set β
ht_mem : t ∈ S
hst : Set.Nonempty (f ⁻¹' (s ∩ t))
⊢ Set.Nonempty (s ∩ t)
[PROOFSTEP]
by_contra h
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
s : Set β
hs_mem : s ∈ S
t : Set β
ht_mem : t ∈ S
hst : Set.Nonempty (f ⁻¹' (s ∩ t))
h : ¬Set.Nonempty (s ∩ t)
⊢ False
[PROOFSTEP]
rw [Set.not_nonempty_iff_eq_empty] at h 
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
s : Set β
hs_mem : s ∈ S
t : Set β
ht_mem : t ∈ S
hst : Set.Nonempty (f ⁻¹' (s ∩ t))
h : s ∩ t = ∅
⊢ False
[PROOFSTEP]
rw [h] at hst 
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
S : Set (Set β)
h_pi : IsPiSystem S
f : α → β
s : Set β
hs_mem : s ∈ S
t : Set β
ht_mem : t ∈ S
hst : Set.Nonempty (f ⁻¹' ∅)
h : s ∩ t = ∅
⊢ False
[PROOFSTEP]
simp at hst 
[GOAL]
α : Type u_1
ι : Sort u_2
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x x_1 => x ≤ x_1) p
⊢ IsPiSystem (⋃ (n : ι), p n)
[PROOFSTEP]
intro t1 ht1 t2 ht2 h
[GOAL]
α : Type u_1
ι : Sort u_2
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x x_1 => x ≤ x_1) p
t1 : Set α
ht1 : t1 ∈ ⋃ (n : ι), p n
t2 : Set α
ht2 : t2 ∈ ⋃ (n : ι), p n
h : Set.Nonempty (t1 ∩ t2)
⊢ t1 ∩ t2 ∈ ⋃ (n : ι), p n
[PROOFSTEP]
rw [Set.mem_iUnion] at ht1 ht2 ⊢
[GOAL]
α : Type u_1
ι : Sort u_2
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x x_1 => x ≤ x_1) p
t1 : Set α
ht1 : ∃ i, t1 ∈ p i
t2 : Set α
ht2 : ∃ i, t2 ∈ p i
h : Set.Nonempty (t1 ∩ t2)
⊢ ∃ i, t1 ∩ t2 ∈ p i
[PROOFSTEP]
cases' ht1 with n ht1
[GOAL]
case intro
α : Type u_1
ι : Sort u_2
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x x_1 => x ≤ x_1) p
t1 t2 : Set α
ht2 : ∃ i, t2 ∈ p i
h : Set.Nonempty (t1 ∩ t2)
n : ι
ht1 : t1 ∈ p n
⊢ ∃ i, t1 ∩ t2 ∈ p i
[PROOFSTEP]
cases' ht2 with m ht2
[GOAL]
case intro.intro
α : Type u_1
ι : Sort u_2
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x x_1 => x ≤ x_1) p
t1 t2 : Set α
h : Set.Nonempty (t1 ∩ t2)
n : ι
ht1 : t1 ∈ p n
m : ι
ht2 : t2 ∈ p m
⊢ ∃ i, t1 ∩ t2 ∈ p i
[PROOFSTEP]
obtain ⟨k, hpnk, hpmk⟩ : ∃ k, p n ≤ p k ∧ p m ≤ p k := hp_directed n m
[GOAL]
case intro.intro.intro.intro
α : Type u_1
ι : Sort u_2
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x x_1 => x ≤ x_1) p
t1 t2 : Set α
h : Set.Nonempty (t1 ∩ t2)
n : ι
ht1 : t1 ∈ p n
m : ι
ht2 : t2 ∈ p m
k : ι
hpnk : p n ≤ p k
hpmk : p m ≤ p k
⊢ ∃ i, t1 ∩ t2 ∈ p i
[PROOFSTEP]
exact ⟨k, hp_pi k t1 (hpnk ht1) t2 (hpmk ht2) h⟩
[GOAL]
α : Type u_1
ι : Sort u_2
ι' : Sort u_3
inst✝ : LinearOrder α
s : Set α
⊢ IsPiSystem (Iio '' s)
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ -
[GOAL]
case intro.intro.intro.intro
α : Type u_1
ι : Sort u_2
ι' : Sort u_3
inst✝ : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ Iio a ∩ Iio b ∈ Iio '' s
[PROOFSTEP]
exact ⟨a ⊓ b, inf_ind a b ha hb, Iio_inter_Iio.symm⟩
[GOAL]
α : Type u_1
ι : Sort u_2
ι' : Sort u_3
inst✝ : LinearOrder α
s : Set α
⊢ IsPiSystem (Iic '' s)
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ -
[GOAL]
case intro.intro.intro.intro
α : Type u_1
ι : Sort u_2
ι' : Sort u_3
inst✝ : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ Iic a ∩ Iic b ∈ Iic '' s
[PROOFSTEP]
exact ⟨a ⊓ b, inf_ind a b ha hb, Iic_inter_Iic.symm⟩
[GOAL]
α : Type u_1
ι : Sort u_2
ι' : Sort u_3
inst✝ : LinearOrder α
Ixx : α → α → Set α
p : α → α → Prop
Hne : ∀ {a b : α}, Set.Nonempty (Ixx a b) → p a b
Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)
s t : Set α
⊢ IsPiSystem {S | ∃ l, l ∈ s ∧ ∃ u, u ∈ t ∧ p l u ∧ Ixx l u = S}
[PROOFSTEP]
rintro _ ⟨l₁, hls₁, u₁, hut₁, _, rfl⟩ _ ⟨l₂, hls₂, u₂, hut₂, _, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Sort u_2
ι' : Sort u_3
inst✝ : LinearOrder α
Ixx : α → α → Set α
p : α → α → Prop
Hne : ∀ {a b : α}, Set.Nonempty (Ixx a b) → p a b
Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)
s t : Set α
l₁ : α
hls₁ : l₁ ∈ s
u₁ : α
hut₁ : u₁ ∈ t
left✝¹ : p l₁ u₁
l₂ : α
hls₂ : l₂ ∈ s
u₂ : α
hut₂ : u₂ ∈ t
left✝ : p l₂ u₂
⊢ Set.Nonempty (Ixx l₁ u₁ ∩ Ixx l₂ u₂) → Ixx l₁ u₁ ∩ Ixx l₂ u₂ ∈ {S | ∃ l, l ∈ s ∧ ∃ u, u ∈ t ∧ p l u ∧ Ixx l u = S}
[PROOFSTEP]
simp only [Hi]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Sort u_2
ι' : Sort u_3
inst✝ : LinearOrder α
Ixx : α → α → Set α
p : α → α → Prop
Hne : ∀ {a b : α}, Set.Nonempty (Ixx a b) → p a b
Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)
s t : Set α
l₁ : α
hls₁ : l₁ ∈ s
u₁ : α
hut₁ : u₁ ∈ t
left✝¹ : p l₁ u₁
l₂ : α
hls₂ : l₂ ∈ s
u₂ : α
hut₂ : u₂ ∈ t
left✝ : p l₂ u₂
⊢ Set.Nonempty (Ixx (max l₁ l₂) (min u₁ u₂)) →
    Ixx (max l₁ l₂) (min u₁ u₂) ∈ {S | ∃ l, l ∈ s ∧ ∃ u, u ∈ t ∧ p l u ∧ Ixx l u = S}
[PROOFSTEP]
exact fun H => ⟨l₁ ⊔ l₂, sup_ind l₁ l₂ hls₁ hls₂, u₁ ⊓ u₂, inf_ind u₁ u₂ hut₁ hut₂, Hne H, rfl⟩
[GOAL]
α : Type u_1
ι : Sort u_2
ι' : Sort u_3
inst✝ : LinearOrder α
Ixx : α → α → Set α
p : α → α → Prop
Hne : ∀ {a b : α}, Set.Nonempty (Ixx a b) → p a b
Hi : ∀ {a₁ b₁ a₂ b₂ : α}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)
f : ι → α
g : ι' → α
⊢ IsPiSystem {S | ∃ i j, p (f i) (g j) ∧ Ixx (f i) (g j) = S}
[PROOFSTEP]
simpa only [exists_range_iff] using isPiSystem_Ixx_mem (@Hne) (@Hi) (range f) (range g)
[GOAL]
α : Type u_1
ι : Sort u_2
ι' : Sort u_3
inst✝ : LinearOrder α
s t : Set α
⊢ ∀ {a₁ b₁ a₂ b₂ : α}, Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (max a₁ a₂) (min b₁ b₂)
[PROOFSTEP]
exact Icc_inter_Icc
[GOAL]
α : Type u_1
ι : Sort u_2
ι' : Sort u_3
inst✝ : LinearOrder α
f : ι → α
g : ι' → α
⊢ ∀ {a₁ b₁ a₂ b₂ : α}, Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (max a₁ a₂) (min b₁ b₂)
[PROOFSTEP]
exact Icc_inter_Icc
[GOAL]
α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x : Set α
h : x ∈ generatePiSystem S
⊢ x ∈ S
[PROOFSTEP]
induction' h with _ h_s s u _ _ h_nonempty h_s h_u
[GOAL]
case base
α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x s✝ : Set α
h_s : s✝ ∈ S
⊢ s✝ ∈ S
[PROOFSTEP]
exact h_s
[GOAL]
case inter
α : Type u_1
S : Set (Set α)
h_S : IsPiSystem S
x s u : Set α
h_s✝ : generatePiSystem S s
h_t✝ : generatePiSystem S u
h_nonempty : Set.Nonempty (s ∩ u)
h_s : s ∈ S
h_u : u ∈ S
⊢ s ∩ u ∈ S
[PROOFSTEP]
exact h_S _ h_s _ h_u h_nonempty
[GOAL]
α : Type u_1
S T : Set (Set α)
hST : S ⊆ T
t : Set α
ht : t ∈ generatePiSystem S
⊢ t ∈ generatePiSystem T
[PROOFSTEP]
induction' ht with s h_s s u _ _ h_nonempty h_s h_u
[GOAL]
case base
α : Type u_1
S T : Set (Set α)
hST : S ⊆ T
t s : Set α
h_s : s ∈ S
⊢ s ∈ generatePiSystem T
[PROOFSTEP]
exact generatePiSystem.base (Set.mem_of_subset_of_mem hST h_s)
[GOAL]
case inter
α : Type u_1
S T : Set (Set α)
hST : S ⊆ T
t s u : Set α
h_s✝ : generatePiSystem S s
h_t✝ : generatePiSystem S u
h_nonempty : Set.Nonempty (s ∩ u)
h_s : s ∈ generatePiSystem T
h_u : u ∈ generatePiSystem T
⊢ s ∩ u ∈ generatePiSystem T
[PROOFSTEP]
exact isPiSystem_generatePiSystem T _ h_s _ h_u h_nonempty
[GOAL]
α : Type u_1
M : MeasurableSpace α
S : Set (Set α)
h_meas_S : ∀ (s : Set α), s ∈ S → MeasurableSet s
t : Set α
h_in_pi : t ∈ generatePiSystem S
⊢ MeasurableSet t
[PROOFSTEP]
induction' h_in_pi with s h_s s u _ _ _ h_s h_u
[GOAL]
case base
α : Type u_1
M : MeasurableSpace α
S : Set (Set α)
h_meas_S : ∀ (s : Set α), s ∈ S → MeasurableSet s
t s : Set α
h_s : s ∈ S
⊢ MeasurableSet s
[PROOFSTEP]
apply h_meas_S _ h_s
[GOAL]
case inter
α : Type u_1
M : MeasurableSpace α
S : Set (Set α)
h_meas_S : ∀ (s : Set α), s ∈ S → MeasurableSet s
t s u : Set α
h_s✝ : generatePiSystem S s
h_t✝ : generatePiSystem S u
h_nonempty✝ : Set.Nonempty (s ∩ u)
h_s : MeasurableSet s
h_u : MeasurableSet u
⊢ MeasurableSet (s ∩ u)
[PROOFSTEP]
apply MeasurableSet.inter h_s h_u
[GOAL]
α : Type u_1
g : Set (Set α)
⊢ generateFrom (generatePiSystem g) = generateFrom g
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u_1
g : Set (Set α)
⊢ generateFrom (generatePiSystem g) ≤ generateFrom g
[PROOFSTEP]
apply generateFrom_le
[GOAL]
case a
α : Type u_1
g : Set (Set α)
⊢ generateFrom g ≤ generateFrom (generatePiSystem g)
[PROOFSTEP]
apply generateFrom_le
[GOAL]
case a.h
α : Type u_1
g : Set (Set α)
⊢ ∀ (t : Set α), t ∈ generatePiSystem g → MeasurableSet t
[PROOFSTEP]
exact fun t h_t => generateFrom_measurableSet_of_generatePiSystem t h_t
[GOAL]
case a.h
α : Type u_1
g : Set (Set α)
⊢ ∀ (t : Set α), t ∈ g → MeasurableSet t
[PROOFSTEP]
exact fun t h_t => measurableSet_generateFrom (generatePiSystem.base h_t)
[GOAL]
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ (b : β), g b)
⊢ ∃ T f, t = ⋂ (b : β) (_ : b ∈ T), f b ∧ ∀ (b : β), b ∈ T → f b ∈ g b
[PROOFSTEP]
induction' h_t with s h_s s t' h_gen_s h_gen_t' h_nonempty h_s h_t'
[GOAL]
case base
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t s : Set α
h_s : s ∈ ⋃ (b : β), g b
⊢ ∃ T f, s = ⋂ (b : β) (_ : b ∈ T), f b ∧ ∀ (b : β), b ∈ T → f b ∈ g b
[PROOFSTEP]
rcases h_s with ⟨t', ⟨⟨b, rfl⟩, h_s_in_t'⟩⟩
[GOAL]
case base.intro.intro.intro
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t s : Set α
b : β
h_s_in_t' : s ∈ (fun b => g b) b
⊢ ∃ T f, s = ⋂ (b : β) (_ : b ∈ T), f b ∧ ∀ (b : β), b ∈ T → f b ∈ g b
[PROOFSTEP]
refine' ⟨{ b }, fun _ => s, _⟩
[GOAL]
case base.intro.intro.intro
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t s : Set α
b : β
h_s_in_t' : s ∈ (fun b => g b) b
⊢ s = ⋂ (b_1 : β) (_ : b_1 ∈ {b}), (fun x => s) b_1 ∧ ∀ (b_1 : β), b_1 ∈ {b} → (fun x => s) b_1 ∈ g b_1
[PROOFSTEP]
simpa using h_s_in_t'
[GOAL]
case inter
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t s t' : Set α
h_gen_s : generatePiSystem (⋃ (b : β), g b) s
h_gen_t' : generatePiSystem (⋃ (b : β), g b) t'
h_nonempty : Set.Nonempty (s ∩ t')
h_s : ∃ T f, s = ⋂ (b : β) (_ : b ∈ T), f b ∧ ∀ (b : β), b ∈ T → f b ∈ g b
h_t' : ∃ T f, t' = ⋂ (b : β) (_ : b ∈ T), f b ∧ ∀ (b : β), b ∈ T → f b ∈ g b
⊢ ∃ T f, s ∩ t' = ⋂ (b : β) (_ : b ∈ T), f b ∧ ∀ (b : β), b ∈ T → f b ∈ g b
[PROOFSTEP]
rcases h_t' with ⟨T_t', ⟨f_t', ⟨rfl, h_t'⟩⟩⟩
[GOAL]
case inter.intro.intro.intro
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t s : Set α
h_gen_s : generatePiSystem (⋃ (b : β), g b) s
h_s : ∃ T f, s = ⋂ (b : β) (_ : b ∈ T), f b ∧ ∀ (b : β), b ∈ T → f b ∈ g b
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
h_nonempty : Set.Nonempty (s ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
⊢ ∃ T f, s ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b = ⋂ (b : β) (_ : b ∈ T), f b ∧ ∀ (b : β), b ∈ T → f b ∈ g b
[PROOFSTEP]
rcases h_s with ⟨T_s, ⟨f_s, ⟨rfl, h_s⟩⟩⟩
[GOAL]
case inter.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
⊢ ∃ T f,
    (⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b = ⋂ (b : β) (_ : b ∈ T), f b ∧
      ∀ (b : β), b ∈ T → f b ∈ g b
[PROOFSTEP]
use T_s ∪ T_t', fun b : β =>
  if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else (∅ : Set α)
[GOAL]
case h
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
⊢ ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b =
      ⋂ (b : β) (_ : b ∈ T_s ∪ T_t'),
        if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∧
    ∀ (b : β),
      b ∈ T_s ∪ T_t' →
        (if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∈ g b
[PROOFSTEP]
constructor
[GOAL]
case h.left
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
⊢ (⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b =
    ⋂ (b : β) (_ : b ∈ T_s ∪ T_t'),
      if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅
[PROOFSTEP]
ext a
[GOAL]
case h.left.h
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
⊢ a ∈ (⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b ↔
    a ∈
      ⋂ (b : β) (_ : b ∈ T_s ∪ T_t'),
        if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅
[PROOFSTEP]
simp_rw [Set.mem_inter_iff, Set.mem_iInter, Finset.mem_union, or_imp]
[GOAL]
case h.left.h
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
⊢ ((∀ (i : β), i ∈ T_s → a ∈ f_s i) ∧ ∀ (i : β), i ∈ T_t' → a ∈ f_t' i) ↔
    ∀ (i : β),
      (i ∈ T_s → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅) ∧
        (i ∈ T_t' → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅)
[PROOFSTEP]
rw [← forall_and]
[GOAL]
case h.left.h
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
⊢ (∀ (x : β), (x ∈ T_s → a ∈ f_s x) ∧ (x ∈ T_t' → a ∈ f_t' x)) ↔
    ∀ (i : β),
      (i ∈ T_s → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅) ∧
        (i ∈ T_t' → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅)
[PROOFSTEP]
constructor
[GOAL]
case h.left.h.mp
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
⊢ (∀ (x : β), (x ∈ T_s → a ∈ f_s x) ∧ (x ∈ T_t' → a ∈ f_t' x)) →
    ∀ (i : β),
      (i ∈ T_s → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅) ∧
        (i ∈ T_t' → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅)
[PROOFSTEP]
intro h1 b
[GOAL]
case h.left.h.mpr
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
⊢ (∀ (i : β),
      (i ∈ T_s → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅) ∧
        (i ∈ T_t' →
          a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅)) →
    ∀ (x : β), (x ∈ T_s → a ∈ f_s x) ∧ (x ∈ T_t' → a ∈ f_t' x)
[PROOFSTEP]
intro h1 b
[GOAL]
case h.left.h.mp
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
h1 : ∀ (x : β), (x ∈ T_s → a ∈ f_s x) ∧ (x ∈ T_t' → a ∈ f_t' x)
b : β
⊢ (b ∈ T_s → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∧
    (b ∈ T_t' → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
[PROOFSTEP]
by_cases hbs : b ∈ T_s
[GOAL]
case h.left.h.mpr
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
h1 :
  ∀ (i : β),
    (i ∈ T_s → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅) ∧
      (i ∈ T_t' → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅)
b : β
⊢ (b ∈ T_s → a ∈ f_s b) ∧ (b ∈ T_t' → a ∈ f_t' b)
[PROOFSTEP]
by_cases hbs : b ∈ T_s
[GOAL]
case pos
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
h1 : ∀ (x : β), (x ∈ T_s → a ∈ f_s x) ∧ (x ∈ T_t' → a ∈ f_t' x)
b : β
hbs : b ∈ T_s
⊢ (b ∈ T_s → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∧
    (b ∈ T_t' → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
[PROOFSTEP]
by_cases hbt : b ∈ T_t'
[GOAL]
case neg
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
h1 : ∀ (x : β), (x ∈ T_s → a ∈ f_s x) ∧ (x ∈ T_t' → a ∈ f_t' x)
b : β
hbs : ¬b ∈ T_s
⊢ (b ∈ T_s → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∧
    (b ∈ T_t' → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
[PROOFSTEP]
by_cases hbt : b ∈ T_t'
[GOAL]
case pos
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
h1 :
  ∀ (i : β),
    (i ∈ T_s → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅) ∧
      (i ∈ T_t' → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅)
b : β
hbs : b ∈ T_s
⊢ (b ∈ T_s → a ∈ f_s b) ∧ (b ∈ T_t' → a ∈ f_t' b)
[PROOFSTEP]
by_cases hbt : b ∈ T_t'
[GOAL]
case neg
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
h1 :
  ∀ (i : β),
    (i ∈ T_s → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅) ∧
      (i ∈ T_t' → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅)
b : β
hbs : ¬b ∈ T_s
⊢ (b ∈ T_s → a ∈ f_s b) ∧ (b ∈ T_t' → a ∈ f_t' b)
[PROOFSTEP]
by_cases hbt : b ∈ T_t'
[GOAL]
case pos
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
h1 : ∀ (x : β), (x ∈ T_s → a ∈ f_s x) ∧ (x ∈ T_t' → a ∈ f_t' x)
b : β
hbs : b ∈ T_s
hbt : b ∈ T_t'
⊢ (b ∈ T_s → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∧
    (b ∈ T_t' → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
[PROOFSTEP]
specialize h1 b
[GOAL]
case neg
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
h1 : ∀ (x : β), (x ∈ T_s → a ∈ f_s x) ∧ (x ∈ T_t' → a ∈ f_t' x)
b : β
hbs : b ∈ T_s
hbt : ¬b ∈ T_t'
⊢ (b ∈ T_s → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∧
    (b ∈ T_t' → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
[PROOFSTEP]
specialize h1 b
[GOAL]
case pos
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
h1 : ∀ (x : β), (x ∈ T_s → a ∈ f_s x) ∧ (x ∈ T_t' → a ∈ f_t' x)
b : β
hbs : ¬b ∈ T_s
hbt : b ∈ T_t'
⊢ (b ∈ T_s → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∧
    (b ∈ T_t' → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
[PROOFSTEP]
specialize h1 b
[GOAL]
case neg
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
h1 : ∀ (x : β), (x ∈ T_s → a ∈ f_s x) ∧ (x ∈ T_t' → a ∈ f_t' x)
b : β
hbs : ¬b ∈ T_s
hbt : ¬b ∈ T_t'
⊢ (b ∈ T_s → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∧
    (b ∈ T_t' → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
[PROOFSTEP]
specialize h1 b
[GOAL]
case pos
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
h1 :
  ∀ (i : β),
    (i ∈ T_s → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅) ∧
      (i ∈ T_t' → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅)
b : β
hbs : b ∈ T_s
hbt : b ∈ T_t'
⊢ (b ∈ T_s → a ∈ f_s b) ∧ (b ∈ T_t' → a ∈ f_t' b)
[PROOFSTEP]
specialize h1 b
[GOAL]
case neg
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
h1 :
  ∀ (i : β),
    (i ∈ T_s → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅) ∧
      (i ∈ T_t' → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅)
b : β
hbs : b ∈ T_s
hbt : ¬b ∈ T_t'
⊢ (b ∈ T_s → a ∈ f_s b) ∧ (b ∈ T_t' → a ∈ f_t' b)
[PROOFSTEP]
specialize h1 b
[GOAL]
case pos
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
h1 :
  ∀ (i : β),
    (i ∈ T_s → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅) ∧
      (i ∈ T_t' → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅)
b : β
hbs : ¬b ∈ T_s
hbt : b ∈ T_t'
⊢ (b ∈ T_s → a ∈ f_s b) ∧ (b ∈ T_t' → a ∈ f_t' b)
[PROOFSTEP]
specialize h1 b
[GOAL]
case neg
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
h1 :
  ∀ (i : β),
    (i ∈ T_s → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅) ∧
      (i ∈ T_t' → a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅)
b : β
hbs : ¬b ∈ T_s
hbt : ¬b ∈ T_t'
⊢ (b ∈ T_s → a ∈ f_s b) ∧ (b ∈ T_t' → a ∈ f_t' b)
[PROOFSTEP]
specialize h1 b
[GOAL]
case pos
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
b : β
hbs : b ∈ T_s
hbt : b ∈ T_t'
h1 : (b ∈ T_s → a ∈ f_s b) ∧ (b ∈ T_t' → a ∈ f_t' b)
⊢ (b ∈ T_s → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∧
    (b ∈ T_t' → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
[PROOFSTEP]
simp only [hbs, hbt, if_true, if_false, true_imp_iff, and_self_iff, false_imp_iff, and_true_iff, true_and_iff] at h1 ⊢
[GOAL]
case neg
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
b : β
hbs : b ∈ T_s
hbt : ¬b ∈ T_t'
h1 : (b ∈ T_s → a ∈ f_s b) ∧ (b ∈ T_t' → a ∈ f_t' b)
⊢ (b ∈ T_s → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∧
    (b ∈ T_t' → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
[PROOFSTEP]
simp only [hbs, hbt, if_true, if_false, true_imp_iff, and_self_iff, false_imp_iff, and_true_iff, true_and_iff] at h1 ⊢
[GOAL]
case pos
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
b : β
hbs : ¬b ∈ T_s
hbt : b ∈ T_t'
h1 : (b ∈ T_s → a ∈ f_s b) ∧ (b ∈ T_t' → a ∈ f_t' b)
⊢ (b ∈ T_s → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∧
    (b ∈ T_t' → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
[PROOFSTEP]
simp only [hbs, hbt, if_true, if_false, true_imp_iff, and_self_iff, false_imp_iff, and_true_iff, true_and_iff] at h1 ⊢
[GOAL]
case neg
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
b : β
hbs : ¬b ∈ T_s
hbt : ¬b ∈ T_t'
h1 : (b ∈ T_s → a ∈ f_s b) ∧ (b ∈ T_t' → a ∈ f_t' b)
⊢ (b ∈ T_s → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∧
    (b ∈ T_t' → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
[PROOFSTEP]
simp only [hbs, hbt, if_true, if_false, true_imp_iff, and_self_iff, false_imp_iff, and_true_iff, true_and_iff] at h1 ⊢
[GOAL]
case pos
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
b : β
hbs : b ∈ T_s
hbt : b ∈ T_t'
h1 :
  (b ∈ T_s → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∧
    (b ∈ T_t' → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
⊢ (b ∈ T_s → a ∈ f_s b) ∧ (b ∈ T_t' → a ∈ f_t' b)
[PROOFSTEP]
simp only [hbs, hbt, if_true, if_false, true_imp_iff, and_self_iff, false_imp_iff, and_true_iff, true_and_iff] at h1 ⊢
[GOAL]
case neg
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
b : β
hbs : b ∈ T_s
hbt : ¬b ∈ T_t'
h1 :
  (b ∈ T_s → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∧
    (b ∈ T_t' → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
⊢ (b ∈ T_s → a ∈ f_s b) ∧ (b ∈ T_t' → a ∈ f_t' b)
[PROOFSTEP]
simp only [hbs, hbt, if_true, if_false, true_imp_iff, and_self_iff, false_imp_iff, and_true_iff, true_and_iff] at h1 ⊢
[GOAL]
case pos
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
b : β
hbs : ¬b ∈ T_s
hbt : b ∈ T_t'
h1 :
  (b ∈ T_s → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∧
    (b ∈ T_t' → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
⊢ (b ∈ T_s → a ∈ f_s b) ∧ (b ∈ T_t' → a ∈ f_t' b)
[PROOFSTEP]
simp only [hbs, hbt, if_true, if_false, true_imp_iff, and_self_iff, false_imp_iff, and_true_iff, true_and_iff] at h1 ⊢
[GOAL]
case neg
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
b : β
hbs : ¬b ∈ T_s
hbt : ¬b ∈ T_t'
h1 :
  (b ∈ T_s → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∧
    (b ∈ T_t' → a ∈ if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅)
⊢ (b ∈ T_s → a ∈ f_s b) ∧ (b ∈ T_t' → a ∈ f_t' b)
[PROOFSTEP]
simp only [hbs, hbt, if_true, if_false, true_imp_iff, and_self_iff, false_imp_iff, and_true_iff, true_and_iff] at h1 ⊢
[GOAL]
case pos
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
b : β
hbs : b ∈ T_s
hbt : b ∈ T_t'
h1 : a ∈ f_s b ∧ a ∈ f_t' b
⊢ a ∈ f_s b ∩ f_t' b
case neg
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
b : β
hbs : b ∈ T_s
hbt : ¬b ∈ T_t'
h1 : a ∈ f_s b
⊢ a ∈ f_s b
case pos
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
b : β
hbs : ¬b ∈ T_s
hbt : b ∈ T_t'
h1 : a ∈ f_t' b
⊢ a ∈ f_t' b
case pos
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
b : β
hbs : b ∈ T_s
hbt : b ∈ T_t'
h1 : a ∈ f_s b ∩ f_t' b
⊢ a ∈ f_s b ∧ a ∈ f_t' b
case neg
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
b : β
hbs : b ∈ T_s
hbt : ¬b ∈ T_t'
h1 : a ∈ f_s b
⊢ a ∈ f_s b
case pos
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
b : β
hbs : ¬b ∈ T_s
hbt : b ∈ T_t'
h1 : a ∈ f_t' b
⊢ a ∈ f_t' b
[PROOFSTEP]
all_goals exact h1
[GOAL]
case pos
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
b : β
hbs : b ∈ T_s
hbt : b ∈ T_t'
h1 : a ∈ f_s b ∧ a ∈ f_t' b
⊢ a ∈ f_s b ∩ f_t' b
[PROOFSTEP]
exact h1
[GOAL]
case neg
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
b : β
hbs : b ∈ T_s
hbt : ¬b ∈ T_t'
h1 : a ∈ f_s b
⊢ a ∈ f_s b
[PROOFSTEP]
exact h1
[GOAL]
case pos
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
b : β
hbs : ¬b ∈ T_s
hbt : b ∈ T_t'
h1 : a ∈ f_t' b
⊢ a ∈ f_t' b
[PROOFSTEP]
exact h1
[GOAL]
case pos
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
b : β
hbs : b ∈ T_s
hbt : b ∈ T_t'
h1 : a ∈ f_s b ∩ f_t' b
⊢ a ∈ f_s b ∧ a ∈ f_t' b
[PROOFSTEP]
exact h1
[GOAL]
case neg
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
b : β
hbs : b ∈ T_s
hbt : ¬b ∈ T_t'
h1 : a ∈ f_s b
⊢ a ∈ f_s b
[PROOFSTEP]
exact h1
[GOAL]
case pos
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
a : α
b : β
hbs : ¬b ∈ T_s
hbt : b ∈ T_t'
h1 : a ∈ f_t' b
⊢ a ∈ f_t' b
[PROOFSTEP]
exact h1
[GOAL]
case h.right
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
⊢ ∀ (b : β),
    b ∈ T_s ∪ T_t' →
      (if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∈ g b
[PROOFSTEP]
intro b h_b
[GOAL]
case h.right
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
⊢ (if b ∈ T_s then if b ∈ T_t' then f_s b ∩ f_t' b else f_s b else if b ∈ T_t' then f_t' b else ∅) ∈ g b
[PROOFSTEP]
split_ifs with hbs hbt hbt
[GOAL]
case pos
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∈ T_s
hbt : b ∈ T_t'
⊢ f_s b ∩ f_t' b ∈ g b
[PROOFSTEP]
refine' h_pi b (f_s b) (h_s b hbs) (f_t' b) (h_t' b hbt) (Set.Nonempty.mono _ h_nonempty)
[GOAL]
case pos
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∈ T_s
hbt : b ∈ T_t'
⊢ (⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b ⊆ f_s b ∩ f_t' b
[PROOFSTEP]
exact Set.inter_subset_inter (Set.biInter_subset_of_mem hbs) (Set.biInter_subset_of_mem hbt)
[GOAL]
case neg
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : b ∈ T_s
hbt : ¬b ∈ T_t'
⊢ f_s b ∈ g b
[PROOFSTEP]
exact h_s b hbs
[GOAL]
case pos
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : ¬b ∈ T_s
hbt : b ∈ T_t'
⊢ f_t' b ∈ g b
[PROOFSTEP]
exact h_t' b hbt
[GOAL]
case neg
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
b : β
h_b : b ∈ T_s ∪ T_t'
hbs : ¬b ∈ T_s
hbt : ¬b ∈ T_t'
⊢ ∅ ∈ g b
[PROOFSTEP]
rw [Finset.mem_union] at h_b 
[GOAL]
case neg
α : Type u_1
β : Type u_2
g : β → Set (Set α)
h_pi : ∀ (b : β), IsPiSystem (g b)
t : Set α
T_t' : Finset β
f_t' : β → Set α
h_t' : ∀ (b : β), b ∈ T_t' → f_t' b ∈ g b
h_gen_t' : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
T_s : Finset β
f_s : β → Set α
h_s : ∀ (b : β), b ∈ T_s → f_s b ∈ g b
h_gen_s : generatePiSystem (⋃ (b : β), g b) (⋂ (b : β) (_ : b ∈ T_s), f_s b)
h_nonempty : Set.Nonempty ((⋂ (b : β) (_ : b ∈ T_s), f_s b) ∩ ⋂ (b : β) (_ : b ∈ T_t'), f_t' b)
b : β
h_b : b ∈ T_s ∨ b ∈ T_t'
hbs : ¬b ∈ T_s
hbt : ¬b ∈ T_t'
⊢ ∅ ∈ g b
[PROOFSTEP]
apply False.elim (h_b.elim hbs hbt)
[GOAL]
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
⊢ ∃ T f, ↑T ⊆ s ∧ t = ⋂ (b : β) (_ : b ∈ T), f b ∧ ∀ (b : β), b ∈ T → f b ∈ g b
[PROOFSTEP]
have : t ∈ generatePiSystem (⋃ b : Subtype s, (g ∘ Subtype.val) b) :=
  by
  suffices h1 : ⋃ b : Subtype s, (g ∘ Subtype.val) b = ⋃ b ∈ s, g b
  · rwa [h1]
  ext x
  simp only [exists_prop, Set.mem_iUnion, Function.comp_apply, Subtype.exists, Subtype.coe_mk]
  rfl
[GOAL]
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
⊢ t ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
[PROOFSTEP]
suffices h1 : ⋃ b : Subtype s, (g ∘ Subtype.val) b = ⋃ b ∈ s, g b
[GOAL]
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
h1 : ⋃ (b : Subtype s), (g ∘ Subtype.val) b = ⋃ (b : β) (_ : b ∈ s), g b
⊢ t ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
[PROOFSTEP]
rwa [h1]
[GOAL]
case h1
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
⊢ ⋃ (b : Subtype s), (g ∘ Subtype.val) b = ⋃ (b : β) (_ : b ∈ s), g b
[PROOFSTEP]
ext x
[GOAL]
case h1.h
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
x : Set α
⊢ x ∈ ⋃ (b : Subtype s), (g ∘ Subtype.val) b ↔ x ∈ ⋃ (b : β) (_ : b ∈ s), g b
[PROOFSTEP]
simp only [exists_prop, Set.mem_iUnion, Function.comp_apply, Subtype.exists, Subtype.coe_mk]
[GOAL]
case h1.h
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
x : Set α
⊢ (∃ a, s a ∧ x ∈ g a) ↔ ∃ i, i ∈ s ∧ x ∈ g i
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
t : Set α
h_t : t ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : t ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
⊢ ∃ T f, ↑T ⊆ s ∧ t = ⋂ (b : β) (_ : b ∈ T), f b ∧ ∀ (b : β), b ∈ T → f b ∈ g b
[PROOFSTEP]
rcases@mem_generatePiSystem_iUnion_elim α (Subtype s) (g ∘ Subtype.val) (fun b => h_pi b.val b.property) t this with
  ⟨T, ⟨f, ⟨rfl, h_t'⟩⟩⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
⊢ ∃ T_1 f_1,
    ↑T_1 ⊆ s ∧ ⋂ (b : Subtype s) (_ : b ∈ T), f b = ⋂ (b : β) (_ : b ∈ T_1), f_1 b ∧ ∀ (b : β), b ∈ T_1 → f_1 b ∈ g b
[PROOFSTEP]
refine'
  ⟨T.image (fun x : s => (x : β)), Function.extend (fun x : s => (x : β)) f fun _ : β => (∅ : Set α), by simp, _, _⟩
[GOAL]
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
⊢ ↑(Finset.image (fun x => ↑x) T) ⊆ s
[PROOFSTEP]
simp
[GOAL]
case intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
⊢ ⋂ (b : Subtype s) (_ : b ∈ T), f b =
    ⋂ (b : β) (_ : b ∈ Finset.image (fun x => ↑x) T), Function.extend (fun x => ↑x) f (fun x => ∅) b
[PROOFSTEP]
ext a
[GOAL]
case intro.intro.intro.refine'_1.h
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
⊢ a ∈ ⋂ (b : Subtype s) (_ : b ∈ T), f b ↔
    a ∈ ⋂ (b : β) (_ : b ∈ Finset.image (fun x => ↑x) T), Function.extend (fun x => ↑x) f (fun x => ∅) b
[PROOFSTEP]
constructor
[GOAL]
case intro.intro.intro.refine'_1.h.mp
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
⊢ a ∈ ⋂ (b : Subtype s) (_ : b ∈ T), f b →
    a ∈ ⋂ (b : β) (_ : b ∈ Finset.image (fun x => ↑x) T), Function.extend (fun x => ↑x) f (fun x => ∅) b
[PROOFSTEP]
simp (config := { proj := false }) only [Set.mem_iInter, Subtype.forall, Finset.set_biInter_finset_image]
[GOAL]
case intro.intro.intro.refine'_1.h.mp
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
⊢ (∀ (a_1 : β) (b : s a_1), { val := a_1, property := b } ∈ T → a ∈ f { val := a_1, property := b }) →
    ∀ (a_2 : β) (b : a_2 ∈ s),
      { val := a_2, property := b } ∈ T →
        a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := a_2, property := b }
[PROOFSTEP]
intro h1 b h_b h_b_in_T
[GOAL]
case intro.intro.intro.refine'_1.h.mp
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
h1 : ∀ (a_1 : β) (b : s a_1), { val := a_1, property := b } ∈ T → a ∈ f { val := a_1, property := b }
b : β
h_b : b ∈ s
h_b_in_T : { val := b, property := h_b } ∈ T
⊢ a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := b, property := h_b }
[PROOFSTEP]
have h2 := h1 b h_b h_b_in_T
[GOAL]
case intro.intro.intro.refine'_1.h.mp
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
h1 : ∀ (a_1 : β) (b : s a_1), { val := a_1, property := b } ∈ T → a ∈ f { val := a_1, property := b }
b : β
h_b : b ∈ s
h_b_in_T : { val := b, property := h_b } ∈ T
h2 : a ∈ f { val := b, property := h_b }
⊢ a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := b, property := h_b }
[PROOFSTEP]
revert h2
[GOAL]
case intro.intro.intro.refine'_1.h.mp
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
h1 : ∀ (a_1 : β) (b : s a_1), { val := a_1, property := b } ∈ T → a ∈ f { val := a_1, property := b }
b : β
h_b : b ∈ s
h_b_in_T : { val := b, property := h_b } ∈ T
⊢ a ∈ f { val := b, property := h_b } → a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := b, property := h_b }
[PROOFSTEP]
rw [Subtype.val_injective.extend_apply]
[GOAL]
case intro.intro.intro.refine'_1.h.mp
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
h1 : ∀ (a_1 : β) (b : s a_1), { val := a_1, property := b } ∈ T → a ∈ f { val := a_1, property := b }
b : β
h_b : b ∈ s
h_b_in_T : { val := b, property := h_b } ∈ T
⊢ a ∈ f { val := b, property := h_b } → a ∈ f { val := b, property := h_b }
[PROOFSTEP]
apply id
[GOAL]
case intro.intro.intro.refine'_1.h.mpr
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
⊢ a ∈ ⋂ (b : β) (_ : b ∈ Finset.image (fun x => ↑x) T), Function.extend (fun x => ↑x) f (fun x => ∅) b →
    a ∈ ⋂ (b : Subtype s) (_ : b ∈ T), f b
[PROOFSTEP]
simp (config := { proj := false }) only [Set.mem_iInter, Subtype.forall, Finset.set_biInter_finset_image]
[GOAL]
case intro.intro.intro.refine'_1.h.mpr
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
⊢ (∀ (a_1 : β) (b : a_1 ∈ s),
      { val := a_1, property := b } ∈ T →
        a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := a_1, property := b }) →
    ∀ (a_2 : β) (b : s a_2), { val := a_2, property := b } ∈ T → a ∈ f { val := a_2, property := b }
[PROOFSTEP]
intro h1 b h_b h_b_in_T
[GOAL]
case intro.intro.intro.refine'_1.h.mpr
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
h1 :
  ∀ (a_1 : β) (b : a_1 ∈ s),
    { val := a_1, property := b } ∈ T → a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := a_1, property := b }
b : β
h_b : s b
h_b_in_T : { val := b, property := h_b } ∈ T
⊢ a ∈ f { val := b, property := h_b }
[PROOFSTEP]
have h2 := h1 b h_b h_b_in_T
[GOAL]
case intro.intro.intro.refine'_1.h.mpr
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
h1 :
  ∀ (a_1 : β) (b : a_1 ∈ s),
    { val := a_1, property := b } ∈ T → a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := a_1, property := b }
b : β
h_b : s b
h_b_in_T : { val := b, property := h_b } ∈ T
h2 : a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := b, property := h_b }
⊢ a ∈ f { val := b, property := h_b }
[PROOFSTEP]
revert h2
[GOAL]
case intro.intro.intro.refine'_1.h.mpr
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
h1 :
  ∀ (a_1 : β) (b : a_1 ∈ s),
    { val := a_1, property := b } ∈ T → a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := a_1, property := b }
b : β
h_b : s b
h_b_in_T : { val := b, property := h_b } ∈ T
⊢ a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := b, property := h_b } → a ∈ f { val := b, property := h_b }
[PROOFSTEP]
rw [Subtype.val_injective.extend_apply]
[GOAL]
case intro.intro.intro.refine'_1.h.mpr
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
a : α
h1 :
  ∀ (a_1 : β) (b : a_1 ∈ s),
    { val := a_1, property := b } ∈ T → a ∈ Function.extend (fun x => ↑x) f (fun x => ∅) ↑{ val := a_1, property := b }
b : β
h_b : s b
h_b_in_T : { val := b, property := h_b } ∈ T
⊢ a ∈ f { val := b, property := h_b } → a ∈ f { val := b, property := h_b }
[PROOFSTEP]
apply id
[GOAL]
case intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
⊢ ∀ (b : β), b ∈ Finset.image (fun x => ↑x) T → Function.extend (fun x => ↑x) f (fun x => ∅) b ∈ g b
[PROOFSTEP]
intros b h_b
[GOAL]
case intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
b : β
h_b : b ∈ Finset.image (fun x => ↑x) T
⊢ Function.extend (fun x => ↑x) f (fun x => ∅) b ∈ g b
[PROOFSTEP]
simp_rw [Finset.mem_image, Subtype.exists, exists_and_right, exists_eq_right] at h_b 
[GOAL]
case intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
b : β
h_b : ∃ x, { val := b, property := (_ : b ∈ s) } ∈ T
⊢ Function.extend (fun x => ↑x) f (fun x => ∅) b ∈ g b
[PROOFSTEP]
cases' h_b with h_b_w h_b_h
[GOAL]
case intro.intro.intro.refine'_2.intro
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
b : β
h_b_w : b ∈ s
h_b_h : { val := b, property := (_ : b ∈ s) } ∈ T
⊢ Function.extend (fun x => ↑x) f (fun x => ∅) b ∈ g b
[PROOFSTEP]
have h_b_alt : b = (Subtype.mk b h_b_w).val := rfl
[GOAL]
case intro.intro.intro.refine'_2.intro
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
b : β
h_b_w : b ∈ s
h_b_h : { val := b, property := (_ : b ∈ s) } ∈ T
h_b_alt : b = ↑{ val := b, property := h_b_w }
⊢ Function.extend (fun x => ↑x) f (fun x => ∅) b ∈ g b
[PROOFSTEP]
rw [h_b_alt, Subtype.val_injective.extend_apply]
[GOAL]
case intro.intro.intro.refine'_2.intro
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
b : β
h_b_w : b ∈ s
h_b_h : { val := b, property := (_ : b ∈ s) } ∈ T
h_b_alt : b = ↑{ val := b, property := h_b_w }
⊢ f { val := b, property := h_b_w } ∈ g ↑{ val := b, property := h_b_w }
[PROOFSTEP]
apply h_t'
[GOAL]
case intro.intro.intro.refine'_2.intro.a
α : Type u_1
β : Type u_2
g : β → Set (Set α)
s : Set β
h_pi : ∀ (b : β), b ∈ s → IsPiSystem (g b)
T : Finset (Subtype s)
f : Subtype s → Set α
h_t' : ∀ (b : Subtype s), b ∈ T → f b ∈ (g ∘ Subtype.val) b
h_t : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : β) (_ : b ∈ s), g b)
this : ⋂ (b : Subtype s) (_ : b ∈ T), f b ∈ generatePiSystem (⋃ (b : Subtype s), (g ∘ Subtype.val) b)
b : β
h_b_w : b ∈ s
h_b_h : { val := b, property := (_ : b ∈ s) } ∈ T
h_b_alt : b = ↑{ val := b, property := h_b_w }
⊢ { val := b, property := h_b_w } ∈ T
[PROOFSTEP]
apply h_b_h
[GOAL]
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
⊢ piiUnionInter π {i} = π i ∪ {univ}
[PROOFSTEP]
ext1 s
[GOAL]
case h
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
⊢ s ∈ piiUnionInter π {i} ↔ s ∈ π i ∪ {univ}
[PROOFSTEP]
simp only [piiUnionInter, exists_prop, mem_union]
[GOAL]
case h
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ (x : ι), x ∈ t → f x ∈ π x) ∧ s = ⋂ (x : ι) (_ : x ∈ t), f x} ↔ s ∈ π i ∨ s ∈ {univ}
[PROOFSTEP]
refine' ⟨_, fun h => _⟩
[GOAL]
case h.refine'_1
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ (x : ι), x ∈ t → f x ∈ π x) ∧ s = ⋂ (x : ι) (_ : x ∈ t), f x} → s ∈ π i ∨ s ∈ {univ}
[PROOFSTEP]
rintro ⟨t, hti, f, hfπ, rfl⟩
[GOAL]
case h.refine'_1.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
hti : ↑t ⊆ {i}
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
⊢ ⋂ (x : ι) (_ : x ∈ t), f x ∈ π i ∨ ⋂ (x : ι) (_ : x ∈ t), f x ∈ {univ}
[PROOFSTEP]
simp only [subset_singleton_iff, Finset.mem_coe] at hti 
[GOAL]
case h.refine'_1.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
⊢ ⋂ (x : ι) (_ : x ∈ t), f x ∈ π i ∨ ⋂ (x : ι) (_ : x ∈ t), f x ∈ {univ}
[PROOFSTEP]
by_cases hi : i ∈ t
[GOAL]
case pos
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : i ∈ t
⊢ ⋂ (x : ι) (_ : x ∈ t), f x ∈ π i ∨ ⋂ (x : ι) (_ : x ∈ t), f x ∈ {univ}
[PROOFSTEP]
have ht_eq_i : t = { i } := by
  ext1 x
  rw [Finset.mem_singleton]
  exact ⟨fun h => hti x h, fun h => h.symm ▸ hi⟩
[GOAL]
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : i ∈ t
⊢ t = {i}
[PROOFSTEP]
ext1 x
[GOAL]
case a
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : i ∈ t
x : ι
⊢ x ∈ t ↔ x ∈ {i}
[PROOFSTEP]
rw [Finset.mem_singleton]
[GOAL]
case a
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : i ∈ t
x : ι
⊢ x ∈ t ↔ x = i
[PROOFSTEP]
exact ⟨fun h => hti x h, fun h => h.symm ▸ hi⟩
[GOAL]
case pos
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : i ∈ t
ht_eq_i : t = {i}
⊢ ⋂ (x : ι) (_ : x ∈ t), f x ∈ π i ∨ ⋂ (x : ι) (_ : x ∈ t), f x ∈ {univ}
[PROOFSTEP]
simp only [ht_eq_i, Finset.mem_singleton, iInter_iInter_eq_left]
[GOAL]
case pos
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : i ∈ t
ht_eq_i : t = {i}
⊢ f i ∈ π i ∨ f i ∈ {univ}
[PROOFSTEP]
exact Or.inl (hfπ i hi)
[GOAL]
case neg
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : ¬i ∈ t
⊢ ⋂ (x : ι) (_ : x ∈ t), f x ∈ π i ∨ ⋂ (x : ι) (_ : x ∈ t), f x ∈ {univ}
[PROOFSTEP]
have ht_empty : t = ∅ := by
  ext1 x
  simp only [Finset.not_mem_empty, iff_false_iff]
  exact fun hx =>
    hi
      (hti x hx ▸ hx)
        -- Porting note: `Finset.not_mem_empty` required
[GOAL]
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : ¬i ∈ t
⊢ t = ∅
[PROOFSTEP]
ext1 x
[GOAL]
case a
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : ¬i ∈ t
x : ι
⊢ x ∈ t ↔ x ∈ ∅
[PROOFSTEP]
simp only [Finset.not_mem_empty, iff_false_iff]
[GOAL]
case a
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : ¬i ∈ t
x : ι
⊢ ¬x ∈ t
[PROOFSTEP]
exact fun hx =>
  hi
    (hti x hx ▸ hx)
      -- Porting note: `Finset.not_mem_empty` required
[GOAL]
case neg
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
t : Finset ι
f : ι → Set α
hfπ : ∀ (x : ι), x ∈ t → f x ∈ π x
hti : ∀ (y : ι), y ∈ t → y = i
hi : ¬i ∈ t
ht_empty : t = ∅
⊢ ⋂ (x : ι) (_ : x ∈ t), f x ∈ π i ∨ ⋂ (x : ι) (_ : x ∈ t), f x ∈ {univ}
[PROOFSTEP]
simp [ht_empty, Finset.not_mem_empty, iInter_false, iInter_univ, Set.mem_singleton univ, or_true_iff]
[GOAL]
case h.refine'_2
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
h : s ∈ π i ∨ s ∈ {univ}
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ (x : ι), x ∈ t → f x ∈ π x) ∧ s = ⋂ (x : ι) (_ : x ∈ t), f x}
[PROOFSTEP]
cases' h with hs hs
[GOAL]
case h.refine'_2.inl
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ (x : ι), x ∈ t → f x ∈ π x) ∧ s = ⋂ (x : ι) (_ : x ∈ t), f x}
[PROOFSTEP]
refine' ⟨{ i }, _, fun _ => s, ⟨fun x hx => _, _⟩⟩
[GOAL]
case h.refine'_2.inl.refine'_1
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ ↑{i} ⊆ {i}
[PROOFSTEP]
rw [Finset.coe_singleton]
[GOAL]
case h.refine'_2.inl.refine'_2
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
x : ι
hx : x ∈ {i}
⊢ (fun x => s) x ∈ π x
[PROOFSTEP]
rw [Finset.mem_singleton] at hx 
[GOAL]
case h.refine'_2.inl.refine'_2
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
x : ι
hx : x = i
⊢ (fun x => s) x ∈ π x
[PROOFSTEP]
rwa [hx]
[GOAL]
case h.refine'_2.inl.refine'_3
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ π i
⊢ s = ⋂ (x : ι) (_ : x ∈ {i}), (fun x => s) x
[PROOFSTEP]
simp only [Finset.mem_singleton, iInter_iInter_eq_left]
[GOAL]
case h.refine'_2.inr
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ {univ}
⊢ s ∈ {s | ∃ t, ↑t ⊆ {i} ∧ ∃ f, (∀ (x : ι), x ∈ t → f x ∈ π x) ∧ s = ⋂ (x : ι) (_ : x ∈ t), f x}
[PROOFSTEP]
refine' ⟨∅, _⟩
[GOAL]
case h.refine'_2.inr
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
i : ι
s : Set α
hs : s ∈ {univ}
⊢ ↑∅ ⊆ {i} ∧ ∃ f, (∀ (x : ι), x ∈ ∅ → f x ∈ π x) ∧ s = ⋂ (x : ι) (_ : x ∈ ∅), f x
[PROOFSTEP]
simpa only [Finset.coe_empty, subset_singleton_iff, mem_empty_iff_false, IsEmpty.forall_iff, imp_true_iff,
  Finset.not_mem_empty, iInter_false, iInter_univ, true_and_iff, exists_const] using hs
[GOAL]
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
⊢ piiUnionInter (fun i => {s i}) S = {s' | ∃ t x, s' = ⋂ (i : ι) (_ : i ∈ t), s i}
[PROOFSTEP]
ext1 s'
[GOAL]
case h
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
s' : Set α
⊢ s' ∈ piiUnionInter (fun i => {s i}) S ↔ s' ∈ {s' | ∃ t x, s' = ⋂ (i : ι) (_ : i ∈ t), s i}
[PROOFSTEP]
simp_rw [piiUnionInter, Set.mem_singleton_iff, exists_prop, Set.mem_setOf_eq]
[GOAL]
case h
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
s' : Set α
⊢ (∃ t, ↑t ⊆ S ∧ ∃ f, (∀ (x : ι), x ∈ t → f x = s x) ∧ s' = ⋂ (x : ι) (_ : x ∈ t), f x) ↔
    ∃ t, ↑t ⊆ S ∧ s' = ⋂ (i : ι) (_ : i ∈ t), s i
[PROOFSTEP]
refine' ⟨fun h => _, fun ⟨t, htS, h_eq⟩ => ⟨t, htS, s, fun _ _ => rfl, h_eq⟩⟩
[GOAL]
case h
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
s' : Set α
h : ∃ t, ↑t ⊆ S ∧ ∃ f, (∀ (x : ι), x ∈ t → f x = s x) ∧ s' = ⋂ (x : ι) (_ : x ∈ t), f x
⊢ ∃ t, ↑t ⊆ S ∧ s' = ⋂ (i : ι) (_ : i ∈ t), s i
[PROOFSTEP]
obtain ⟨t, htS, f, hft_eq, rfl⟩ := h
[GOAL]
case h.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
t : Finset ι
htS : ↑t ⊆ S
f : ι → Set α
hft_eq : ∀ (x : ι), x ∈ t → f x = s x
⊢ ∃ t_1, ↑t_1 ⊆ S ∧ ⋂ (x : ι) (_ : x ∈ t), f x = ⋂ (i : ι) (_ : i ∈ t_1), s i
[PROOFSTEP]
refine' ⟨t, htS, _⟩
[GOAL]
case h.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
t : Finset ι
htS : ↑t ⊆ S
f : ι → Set α
hft_eq : ∀ (x : ι), x ∈ t → f x = s x
⊢ ⋂ (x : ι) (_ : x ∈ t), f x = ⋂ (i : ι) (_ : i ∈ t), s i
[PROOFSTEP]
congr! 3
[GOAL]
case h.intro.intro.intro.intro.h.e'_3.h.f
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
t : Finset ι
htS : ↑t ⊆ S
f : ι → Set α
hft_eq : ∀ (x : ι), x ∈ t → f x = s x
x✝¹ : ι
x✝ : x✝¹ ∈ t
⊢ f x✝¹ = s x✝¹
[PROOFSTEP]
apply hft_eq
[GOAL]
case h.intro.intro.intro.intro.h.e'_3.h.f.a
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
t : Finset ι
htS : ↑t ⊆ S
f : ι → Set α
hft_eq : ∀ (x : ι), x ∈ t → f x = s x
x✝¹ : ι
x✝ : x✝¹ ∈ t
⊢ x✝¹ ∈ t
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
⊢ generateFrom (piiUnionInter (fun k => {s k}) S) = generateFrom {t | ∃ k, k ∈ S ∧ s k = t}
[PROOFSTEP]
refine' le_antisymm (generateFrom_le _) (generateFrom_mono _)
[GOAL]
case refine'_1
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
⊢ ∀ (t : Set α), t ∈ piiUnionInter (fun k => {s k}) S → MeasurableSet t
[PROOFSTEP]
rintro _ ⟨I, hI, f, hf, rfl⟩
[GOAL]
case refine'_1.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
I : Finset ι
hI : ↑I ⊆ S
f : ι → Set α
hf : ∀ (x : ι), x ∈ I → f x ∈ (fun k => {s k}) x
⊢ MeasurableSet (⋂ (x : ι) (_ : x ∈ I), f x)
[PROOFSTEP]
refine' Finset.measurableSet_biInter _ fun m hm => measurableSet_generateFrom _
[GOAL]
case refine'_1.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
I : Finset ι
hI : ↑I ⊆ S
f : ι → Set α
hf : ∀ (x : ι), x ∈ I → f x ∈ (fun k => {s k}) x
m : ι
hm : m ∈ I
⊢ f m ∈ {t | ∃ k, k ∈ S ∧ s k = t}
[PROOFSTEP]
exact ⟨m, hI hm, (hf m hm).symm⟩
[GOAL]
case refine'_2
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
⊢ {t | ∃ k, k ∈ S ∧ s k = t} ⊆ piiUnionInter (fun k => {s k}) S
[PROOFSTEP]
rintro _ ⟨k, hk, rfl⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
⊢ s k ∈ piiUnionInter (fun k => {s k}) S
[PROOFSTEP]
refine' ⟨{ k }, fun m hm => _, s, fun i _ => _, _⟩
[GOAL]
case refine'_2.intro.intro.refine'_1
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
m : ι
hm : m ∈ ↑{k}
⊢ m ∈ S
[PROOFSTEP]
rw [Finset.mem_coe, Finset.mem_singleton] at hm 
[GOAL]
case refine'_2.intro.intro.refine'_1
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
m : ι
hm : m = k
⊢ m ∈ S
[PROOFSTEP]
rwa [hm]
[GOAL]
case refine'_2.intro.intro.refine'_2
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
i : ι
x✝ : i ∈ {k}
⊢ s i ∈ (fun k => {s k}) i
[PROOFSTEP]
exact Set.mem_singleton _
[GOAL]
case refine'_2.intro.intro.refine'_3
α : Type u_1
ι : Type u_2
s : ι → Set α
S : Set ι
k : ι
hk : k ∈ S
⊢ s k = ⋂ (x : ι) (_ : x ∈ {k}), s x
[PROOFSTEP]
simp only [Finset.mem_singleton, Set.iInter_iInter_eq_left]
[GOAL]
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
⊢ IsPiSystem (piiUnionInter π S)
[PROOFSTEP]
rintro t1 ⟨p1, hp1S, f1, hf1m, ht1_eq⟩ t2 ⟨p2, hp2S, f2, hf2m, ht2_eq⟩ h_nonempty
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
⊢ t1 ∩ t2 ∈ piiUnionInter π S
[PROOFSTEP]
simp_rw [piiUnionInter, Set.mem_setOf_eq]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
⊢ ∃ t x f x, t1 ∩ t2 = ⋂ (x : ι) (_ : x ∈ t), f x
[PROOFSTEP]
let g n := ite (n ∈ p1) (f1 n) Set.univ ∩ ite (n ∈ p2) (f2 n) Set.univ
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
⊢ ∃ t x f x, t1 ∩ t2 = ⋂ (x : ι) (_ : x ∈ t), f x
[PROOFSTEP]
have hp_union_ss : ↑(p1 ∪ p2) ⊆ S := by simp only [hp1S, hp2S, Finset.coe_union, union_subset_iff, and_self_iff]
[GOAL]
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
⊢ ↑(p1 ∪ p2) ⊆ S
[PROOFSTEP]
simp only [hp1S, hp2S, Finset.coe_union, union_subset_iff, and_self_iff]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
⊢ ∃ t x f x, t1 ∩ t2 = ⋂ (x : ι) (_ : x ∈ t), f x
[PROOFSTEP]
use p1 ∪ p2, hp_union_ss, g
[GOAL]
case h
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
⊢ ∃ x, t1 ∩ t2 = ⋂ (x : ι) (_ : x ∈ p1 ∪ p2), g x
[PROOFSTEP]
have h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i := by
  rw [ht1_eq, ht2_eq]
  simp_rw [← Set.inf_eq_inter]
  ext1 x
  simp only [inf_eq_inter, mem_inter_iff, mem_iInter, Finset.mem_union]
  refine' ⟨fun h i _ => _, fun h => ⟨fun i hi1 => _, fun i hi2 => _⟩⟩
  · split_ifs with h_1 h_2 h_2
    exacts [⟨h.1 i h_1, h.2 i h_2⟩, ⟨h.1 i h_1, Set.mem_univ _⟩, ⟨Set.mem_univ _, h.2 i h_2⟩,
      ⟨Set.mem_univ _, Set.mem_univ _⟩]
  · specialize h i (Or.inl hi1)
    rw [if_pos hi1] at h 
    exact h.1
  · specialize h i (Or.inr hi2)
    rw [if_pos hi2] at h 
    exact h.2
[GOAL]
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
⊢ t1 ∩ t2 = ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i
[PROOFSTEP]
rw [ht1_eq, ht2_eq]
[GOAL]
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
⊢ (⋂ (x : ι) (_ : x ∈ p1), f1 x) ∩ ⋂ (x : ι) (_ : x ∈ p2), f2 x = ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i
[PROOFSTEP]
simp_rw [← Set.inf_eq_inter]
[GOAL]
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
⊢ (⋂ (x : ι) (_ : x ∈ p1), f1 x) ⊓ ⋂ (x : ι) (_ : x ∈ p2), f2 x =
    ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), (if i ∈ p1 then f1 i else univ) ⊓ if i ∈ p2 then f2 i else univ
[PROOFSTEP]
ext1 x
[GOAL]
case h
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
x : α
⊢ x ∈ (⋂ (x : ι) (_ : x ∈ p1), f1 x) ⊓ ⋂ (x : ι) (_ : x ∈ p2), f2 x ↔
    x ∈ ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), (if i ∈ p1 then f1 i else univ) ⊓ if i ∈ p2 then f2 i else univ
[PROOFSTEP]
simp only [inf_eq_inter, mem_inter_iff, mem_iInter, Finset.mem_union]
[GOAL]
case h
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
x : α
⊢ ((∀ (i : ι), i ∈ p1 → x ∈ f1 i) ∧ ∀ (i : ι), i ∈ p2 → x ∈ f2 i) ↔
    ∀ (i : ι), i ∈ p1 ∨ i ∈ p2 → (x ∈ if i ∈ p1 then f1 i else univ) ∧ x ∈ if i ∈ p2 then f2 i else univ
[PROOFSTEP]
refine' ⟨fun h i _ => _, fun h => ⟨fun i hi1 => _, fun i hi2 => _⟩⟩
[GOAL]
case h.refine'_1
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
x : α
h : (∀ (i : ι), i ∈ p1 → x ∈ f1 i) ∧ ∀ (i : ι), i ∈ p2 → x ∈ f2 i
i : ι
x✝ : i ∈ p1 ∨ i ∈ p2
⊢ (x ∈ if i ∈ p1 then f1 i else univ) ∧ x ∈ if i ∈ p2 then f2 i else univ
[PROOFSTEP]
split_ifs with h_1 h_2 h_2
[GOAL]
case pos
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
x : α
h : (∀ (i : ι), i ∈ p1 → x ∈ f1 i) ∧ ∀ (i : ι), i ∈ p2 → x ∈ f2 i
i : ι
x✝ : i ∈ p1 ∨ i ∈ p2
h_1 : i ∈ p1
h_2 : i ∈ p2
⊢ x ∈ f1 i ∧ x ∈ f2 i
case neg
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
x : α
h : (∀ (i : ι), i ∈ p1 → x ∈ f1 i) ∧ ∀ (i : ι), i ∈ p2 → x ∈ f2 i
i : ι
x✝ : i ∈ p1 ∨ i ∈ p2
h_1 : i ∈ p1
h_2 : ¬i ∈ p2
⊢ x ∈ f1 i ∧ x ∈ univ
case pos
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
x : α
h : (∀ (i : ι), i ∈ p1 → x ∈ f1 i) ∧ ∀ (i : ι), i ∈ p2 → x ∈ f2 i
i : ι
x✝ : i ∈ p1 ∨ i ∈ p2
h_1 : ¬i ∈ p1
h_2 : i ∈ p2
⊢ x ∈ univ ∧ x ∈ f2 i
case neg
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
x : α
h : (∀ (i : ι), i ∈ p1 → x ∈ f1 i) ∧ ∀ (i : ι), i ∈ p2 → x ∈ f2 i
i : ι
x✝ : i ∈ p1 ∨ i ∈ p2
h_1 : ¬i ∈ p1
h_2 : ¬i ∈ p2
⊢ x ∈ univ ∧ x ∈ univ
[PROOFSTEP]
exacts [⟨h.1 i h_1, h.2 i h_2⟩, ⟨h.1 i h_1, Set.mem_univ _⟩, ⟨Set.mem_univ _, h.2 i h_2⟩,
  ⟨Set.mem_univ _, Set.mem_univ _⟩]
[GOAL]
case h.refine'_2
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
x : α
h : ∀ (i : ι), i ∈ p1 ∨ i ∈ p2 → (x ∈ if i ∈ p1 then f1 i else univ) ∧ x ∈ if i ∈ p2 then f2 i else univ
i : ι
hi1 : i ∈ p1
⊢ x ∈ f1 i
[PROOFSTEP]
specialize h i (Or.inl hi1)
[GOAL]
case h.refine'_2
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
x : α
i : ι
hi1 : i ∈ p1
h : (x ∈ if i ∈ p1 then f1 i else univ) ∧ x ∈ if i ∈ p2 then f2 i else univ
⊢ x ∈ f1 i
[PROOFSTEP]
rw [if_pos hi1] at h 
[GOAL]
case h.refine'_2
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
x : α
i : ι
hi1 : i ∈ p1
h : x ∈ f1 i ∧ x ∈ if i ∈ p2 then f2 i else univ
⊢ x ∈ f1 i
[PROOFSTEP]
exact h.1
[GOAL]
case h.refine'_3
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
x : α
h : ∀ (i : ι), i ∈ p1 ∨ i ∈ p2 → (x ∈ if i ∈ p1 then f1 i else univ) ∧ x ∈ if i ∈ p2 then f2 i else univ
i : ι
hi2 : i ∈ p2
⊢ x ∈ f2 i
[PROOFSTEP]
specialize h i (Or.inr hi2)
[GOAL]
case h.refine'_3
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
x : α
i : ι
hi2 : i ∈ p2
h : (x ∈ if i ∈ p1 then f1 i else univ) ∧ x ∈ if i ∈ p2 then f2 i else univ
⊢ x ∈ f2 i
[PROOFSTEP]
rw [if_pos hi2] at h 
[GOAL]
case h.refine'_3
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
x : α
i : ι
hi2 : i ∈ p2
h : (x ∈ if i ∈ p1 then f1 i else univ) ∧ x ∈ f2 i
⊢ x ∈ f2 i
[PROOFSTEP]
exact h.2
[GOAL]
case h
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i
⊢ ∃ x, t1 ∩ t2 = ⋂ (x : ι) (_ : x ∈ p1 ∪ p2), g x
[PROOFSTEP]
refine' ⟨fun n hn => _, h_inter_eq⟩
[GOAL]
case h
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i
n : ι
hn : n ∈ p1 ∪ p2
⊢ g n ∈ π n
[PROOFSTEP]
simp only []
[GOAL]
case h
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i
n : ι
hn : n ∈ p1 ∪ p2
⊢ ((if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ) ∈ π n
[PROOFSTEP]
split_ifs with hn1 hn2 h
[GOAL]
case pos
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
⊢ f1 n ∩ f2 n ∈ π n
[PROOFSTEP]
refine' hpi n (f1 n) (hf1m n hn1) (f2 n) (hf2m n hn2) (Set.nonempty_iff_ne_empty.2 fun h => _)
[GOAL]
case pos
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
h : f1 n ∩ f2 n = ∅
⊢ False
[PROOFSTEP]
rw [h_inter_eq] at h_nonempty 
[GOAL]
case pos
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
h_nonempty : Set.Nonempty (⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i)
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
h : f1 n ∩ f2 n = ∅
⊢ False
[PROOFSTEP]
suffices h_empty : ⋂ i ∈ p1 ∪ p2, g i = ∅
[GOAL]
case pos
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
h_nonempty : Set.Nonempty (⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i)
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
h : f1 n ∩ f2 n = ∅
h_empty : ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i = ∅
⊢ False
case h_empty
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
h_nonempty : Set.Nonempty (⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i)
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
h : f1 n ∩ f2 n = ∅
⊢ ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i = ∅
[PROOFSTEP]
exact (Set.not_nonempty_iff_eq_empty.mpr h_empty) h_nonempty
[GOAL]
case h_empty
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
h_nonempty : Set.Nonempty (⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i)
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
h : f1 n ∩ f2 n = ∅
⊢ ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i = ∅
[PROOFSTEP]
refine' le_antisymm (Set.iInter_subset_of_subset n _) (Set.empty_subset _)
[GOAL]
case h_empty
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
h_nonempty : Set.Nonempty (⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i)
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
h : f1 n ∩ f2 n = ∅
⊢ ⋂ (_ : n ∈ p1 ∪ p2), g n ⊆ ∅
[PROOFSTEP]
refine' Set.iInter_subset_of_subset hn _
[GOAL]
case h_empty
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
h_nonempty : Set.Nonempty (⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i)
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
h : f1 n ∩ f2 n = ∅
⊢ g n ⊆ ∅
[PROOFSTEP]
simp_rw [if_pos hn1, if_pos hn2]
[GOAL]
case h_empty
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
h_nonempty : Set.Nonempty (⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i)
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : n ∈ p2
h : f1 n ∩ f2 n = ∅
⊢ f1 n ∩ f2 n ⊆ ∅
[PROOFSTEP]
exact h.subset
[GOAL]
case neg
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : n ∈ p1
hn2 : ¬n ∈ p2
⊢ f1 n ∩ univ ∈ π n
[PROOFSTEP]
simp [hf1m n hn1]
[GOAL]
case pos
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : ¬n ∈ p1
h : n ∈ p2
⊢ univ ∩ f2 n ∈ π n
[PROOFSTEP]
simp [hf2m n h]
[GOAL]
case neg
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : ¬n ∈ p1
h : ¬n ∈ p2
⊢ univ ∩ univ ∈ π n
[PROOFSTEP]
exact absurd hn (by simp [hn1, h])
[GOAL]
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
t1 : Set α
p1 : Finset ι
hp1S : ↑p1 ⊆ S
f1 : ι → Set α
hf1m : ∀ (x : ι), x ∈ p1 → f1 x ∈ π x
ht1_eq : t1 = ⋂ (x : ι) (_ : x ∈ p1), f1 x
t2 : Set α
p2 : Finset ι
hp2S : ↑p2 ⊆ S
f2 : ι → Set α
hf2m : ∀ (x : ι), x ∈ p2 → f2 x ∈ π x
ht2_eq : t2 = ⋂ (x : ι) (_ : x ∈ p2), f2 x
h_nonempty : Set.Nonempty (t1 ∩ t2)
g : ι → Set α := fun n => (if n ∈ p1 then f1 n else univ) ∩ if n ∈ p2 then f2 n else univ
hp_union_ss : ↑(p1 ∪ p2) ⊆ S
h_inter_eq : t1 ∩ t2 = ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i
n : ι
hn : n ∈ p1 ∪ p2
hn1 : ¬n ∈ p1
h : ¬n ∈ p2
⊢ ¬n ∈ p1 ∪ p2
[PROOFSTEP]
simp [hn1, h]
[GOAL]
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
⊢ generateFrom (piiUnionInter π S) ≤ m
[PROOFSTEP]
refine' generateFrom_le _
[GOAL]
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
⊢ ∀ (t : Set α), t ∈ piiUnionInter π S → MeasurableSet t
[PROOFSTEP]
rintro t ⟨ht_p, _, ft, hft_mem_pi, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
ht_p : Finset ι
w✝ : ↑ht_p ⊆ S
ft : ι → Set α
hft_mem_pi : ∀ (x : ι), x ∈ ht_p → ft x ∈ π x
⊢ MeasurableSet (⋂ (x : ι) (_ : x ∈ ht_p), ft x)
[PROOFSTEP]
refine' Finset.measurableSet_biInter _ fun x hx_mem => (h x) _ _
[GOAL]
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
π : ι → Set (Set α)
h : ∀ (n : ι), generateFrom (π n) ≤ m
S : Set ι
ht_p : Finset ι
w✝ : ↑ht_p ⊆ S
ft : ι → Set α
hft_mem_pi : ∀ (x : ι), x ∈ ht_p → ft x ∈ π x
x : ι
hx_mem : x ∈ ht_p
⊢ MeasurableSet (ft x)
[PROOFSTEP]
exact measurableSet_generateFrom (hft_mem_pi x hx_mem)
[GOAL]
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
⊢ π i ⊆ piiUnionInter π S
[PROOFSTEP]
have h_ss : { i } ⊆ S := by
  intro j hj
  rw [mem_singleton_iff] at hj 
  rwa [hj]
[GOAL]
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
⊢ {i} ⊆ S
[PROOFSTEP]
intro j hj
[GOAL]
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
j : ι
hj : j ∈ {i}
⊢ j ∈ S
[PROOFSTEP]
rw [mem_singleton_iff] at hj 
[GOAL]
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
j : ι
hj : j = i
⊢ j ∈ S
[PROOFSTEP]
rwa [hj]
[GOAL]
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ piiUnionInter π S
[PROOFSTEP]
refine' Subset.trans _ (piiUnionInter_mono_right h_ss)
[GOAL]
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ piiUnionInter π {i}
[PROOFSTEP]
rw [piiUnionInter_singleton]
[GOAL]
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
S : Set ι
i : ι
his : i ∈ S
h_ss : {i} ⊆ S
⊢ π i ⊆ π i ∪ {univ}
[PROOFSTEP]
exact subset_union_left _ _
[GOAL]
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
t : Set α
ht : t ∈ piiUnionInter (fun n => {s | MeasurableSet s}) S
⊢ MeasurableSet t
[PROOFSTEP]
rcases ht with ⟨pt, hpt, ft, ht_m, rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ (x : ι), x ∈ pt → ft x ∈ (fun n => {s | MeasurableSet s}) x
⊢ MeasurableSet (⋂ (x : ι) (_ : x ∈ pt), ft x)
[PROOFSTEP]
refine' pt.measurableSet_biInter fun i hi => _
[GOAL]
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ (x : ι), x ∈ pt → ft x ∈ (fun n => {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
⊢ MeasurableSet (ft i)
[PROOFSTEP]
suffices h_le : m i ≤ ⨆ i ∈ S, m i
[GOAL]
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ (x : ι), x ∈ pt → ft x ∈ (fun n => {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
h_le : m i ≤ ⨆ (i : ι) (_ : i ∈ S), m i
⊢ MeasurableSet (ft i)
case h_le
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ (x : ι), x ∈ pt → ft x ∈ (fun n => {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
⊢ m i ≤ ⨆ (i : ι) (_ : i ∈ S), m i
[PROOFSTEP]
exact h_le (ft i) (ht_m i hi)
[GOAL]
case h_le
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ (x : ι), x ∈ pt → ft x ∈ (fun n => {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
⊢ m i ≤ ⨆ (i : ι) (_ : i ∈ S), m i
[PROOFSTEP]
have hi' : i ∈ S := hpt hi
[GOAL]
case h_le
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
pt : Finset ι
hpt : ↑pt ⊆ S
ft : ι → Set α
ht_m : ∀ (x : ι), x ∈ pt → ft x ∈ (fun n => {s | MeasurableSet s}) x
i : ι
hi : i ∈ pt
hi' : i ∈ S
⊢ m i ≤ ⨆ (i : ι) (_ : i ∈ S), m i
[PROOFSTEP]
exact le_iSup₂ (f := fun i (_ : i ∈ S) => m i) i hi'
[GOAL]
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S) = ⨆ (i : ι) (_ : i ∈ S), m i
[PROOFSTEP]
refine' le_antisymm _ _
[GOAL]
case refine'_1
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S) ≤ ⨆ (i : ι) (_ : i ∈ S), m i
[PROOFSTEP]
rw [← @generateFrom_measurableSet α (⨆ i ∈ S, m i)]
[GOAL]
case refine'_1
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
⊢ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S) ≤ generateFrom {s | MeasurableSet s}
[PROOFSTEP]
exact generateFrom_mono (measurableSet_iSup_of_mem_piiUnionInter m S)
[GOAL]
case refine'_2
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
⊢ ⨆ (i : ι) (_ : i ∈ S), m i ≤ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S)
[PROOFSTEP]
refine' iSup₂_le fun i hi => _
[GOAL]
case refine'_2
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
i : ι
hi : i ∈ S
⊢ m i ≤ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S)
[PROOFSTEP]
rw [← @generateFrom_measurableSet α (m i)]
[GOAL]
case refine'_2
α : Type u_1
ι : Type u_2
m : ι → MeasurableSpace α
S : Set ι
i : ι
hi : i ∈ S
⊢ generateFrom {s | MeasurableSet s} ≤ generateFrom (piiUnionInter (fun n => {s | MeasurableSet s}) S)
[PROOFSTEP]
exact generateFrom_mono (mem_piiUnionInter_of_measurableSet m hi)
[GOAL]
α : Type u_1
s₁ : Set α → Prop
has_empty✝¹ : s₁ ∅
has_compl✝¹ : ∀ {a : Set α}, s₁ a → s₁ aᶜ
has_iUnion_nat✝¹ : ∀ {f : ℕ → Set α}, Pairwise (Disjoint on f) → (∀ (i : ℕ), s₁ (f i)) → s₁ (⋃ (i : ℕ), f i)
s₂ : Set α → Prop
has_empty✝ : s₂ ∅
has_compl✝ : ∀ {a : Set α}, s₂ a → s₂ aᶜ
has_iUnion_nat✝ : ∀ {f : ℕ → Set α}, Pairwise (Disjoint on f) → (∀ (i : ℕ), s₂ (f i)) → s₂ (⋃ (i : ℕ), f i)
h :
  ∀ (s : Set α),
    Has { Has := s₁, has_empty := has_empty✝¹, has_compl := has_compl✝¹, has_iUnion_nat := has_iUnion_nat✝¹ } s ↔
      Has { Has := s₂, has_empty := has_empty✝, has_compl := has_compl✝, has_iUnion_nat := has_iUnion_nat✝ } s
⊢ { Has := s₁, has_empty := has_empty✝¹, has_compl := has_compl✝¹, has_iUnion_nat := has_iUnion_nat✝¹ } =
    { Has := s₂, has_empty := has_empty✝, has_compl := has_compl✝, has_iUnion_nat := has_iUnion_nat✝ }
[PROOFSTEP]
have : s₁ = s₂ := funext fun x => propext <| h x
[GOAL]
α : Type u_1
s₁ : Set α → Prop
has_empty✝¹ : s₁ ∅
has_compl✝¹ : ∀ {a : Set α}, s₁ a → s₁ aᶜ
has_iUnion_nat✝¹ : ∀ {f : ℕ → Set α}, Pairwise (Disjoint on f) → (∀ (i : ℕ), s₁ (f i)) → s₁ (⋃ (i : ℕ), f i)
s₂ : Set α → Prop
has_empty✝ : s₂ ∅
has_compl✝ : ∀ {a : Set α}, s₂ a → s₂ aᶜ
has_iUnion_nat✝ : ∀ {f : ℕ → Set α}, Pairwise (Disjoint on f) → (∀ (i : ℕ), s₂ (f i)) → s₂ (⋃ (i : ℕ), f i)
h :
  ∀ (s : Set α),
    Has { Has := s₁, has_empty := has_empty✝¹, has_compl := has_compl✝¹, has_iUnion_nat := has_iUnion_nat✝¹ } s ↔
      Has { Has := s₂, has_empty := has_empty✝, has_compl := has_compl✝, has_iUnion_nat := has_iUnion_nat✝ } s
this : s₁ = s₂
⊢ { Has := s₁, has_empty := has_empty✝¹, has_compl := has_compl✝¹, has_iUnion_nat := has_iUnion_nat✝¹ } =
    { Has := s₂, has_empty := has_empty✝, has_compl := has_compl✝, has_iUnion_nat := has_iUnion_nat✝ }
[PROOFSTEP]
subst this
[GOAL]
α : Type u_1
s₁ : Set α → Prop
has_empty✝¹ : s₁ ∅
has_compl✝¹ : ∀ {a : Set α}, s₁ a → s₁ aᶜ
has_iUnion_nat✝¹ : ∀ {f : ℕ → Set α}, Pairwise (Disjoint on f) → (∀ (i : ℕ), s₁ (f i)) → s₁ (⋃ (i : ℕ), f i)
has_empty✝ : s₁ ∅
has_compl✝ : ∀ {a : Set α}, s₁ a → s₁ aᶜ
has_iUnion_nat✝ : ∀ {f : ℕ → Set α}, Pairwise (Disjoint on f) → (∀ (i : ℕ), s₁ (f i)) → s₁ (⋃ (i : ℕ), f i)
h :
  ∀ (s : Set α),
    Has { Has := s₁, has_empty := has_empty✝¹, has_compl := has_compl✝¹, has_iUnion_nat := has_iUnion_nat✝¹ } s ↔
      Has { Has := s₁, has_empty := has_empty✝, has_compl := has_compl✝, has_iUnion_nat := has_iUnion_nat✝ } s
⊢ { Has := s₁, has_empty := has_empty✝¹, has_compl := has_compl✝¹, has_iUnion_nat := has_iUnion_nat✝¹ } =
    { Has := s₁, has_empty := has_empty✝, has_compl := has_compl✝, has_iUnion_nat := has_iUnion_nat✝ }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
d : DynkinSystem α
a : Set α
h : Has d aᶜ
⊢ Has d a
[PROOFSTEP]
simpa using d.has_compl h
[GOAL]
α : Type u_1
d : DynkinSystem α
⊢ Has d univ
[PROOFSTEP]
simpa using d.has_compl d.has_empty
[GOAL]
α : Type u_1
d : DynkinSystem α
β : Type u_2
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
h : ∀ (i : β), Has d (f i)
⊢ Has d (⋃ (i : β), f i)
[PROOFSTEP]
cases nonempty_encodable β
[GOAL]
case intro
α : Type u_1
d : DynkinSystem α
β : Type u_2
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
h : ∀ (i : β), Has d (f i)
val✝ : Encodable β
⊢ Has d (⋃ (i : β), f i)
[PROOFSTEP]
rw [← Encodable.iUnion_decode₂]
[GOAL]
case intro
α : Type u_1
d : DynkinSystem α
β : Type u_2
inst✝ : Countable β
f : β → Set α
hd : Pairwise (Disjoint on f)
h : ∀ (i : β), Has d (f i)
val✝ : Encodable β
⊢ Has d (⋃ (i : ℕ) (b : β) (_ : b ∈ Encodable.decode₂ β i), f b)
[PROOFSTEP]
exact d.has_iUnion_nat (Encodable.iUnion_decode₂_disjoint_on hd) fun n => Encodable.iUnion_decode₂_cases d.has_empty h
[GOAL]
α : Type u_1
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : Has d s₁
h₂ : Has d s₂
h : Disjoint s₁ s₂
⊢ Has d (s₁ ∪ s₂)
[PROOFSTEP]
rw [union_eq_iUnion]
[GOAL]
α : Type u_1
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : Has d s₁
h₂ : Has d s₂
h : Disjoint s₁ s₂
⊢ Has d (⋃ (b : Bool), bif b then s₁ else s₂)
[PROOFSTEP]
exact d.has_iUnion (pairwise_disjoint_on_bool.2 h) (Bool.forall_bool.2 ⟨h₂, h₁⟩)
[GOAL]
α : Type u_1
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : Has d s₁
h₂ : Has d s₂
h : s₂ ⊆ s₁
⊢ Has d (s₁ \ s₂)
[PROOFSTEP]
apply d.has_compl_iff.1
[GOAL]
α : Type u_1
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : Has d s₁
h₂ : Has d s₂
h : s₂ ⊆ s₁
⊢ Has d (s₁ \ s₂)ᶜ
[PROOFSTEP]
simp [diff_eq, compl_inter]
[GOAL]
α : Type u_1
d : DynkinSystem α
s₁ s₂ : Set α
h₁ : Has d s₁
h₂ : Has d s₂
h : s₂ ⊆ s₁
⊢ Has d (s₁ᶜ ∪ s₂)
[PROOFSTEP]
exact d.has_union (d.has_compl h₁) h₂ (disjoint_compl_left.mono_right h)
[GOAL]
α : Type u_1
d : DynkinSystem α
C : Set (Set α)
s : Set α
⊢ GenerateHas C sᶜ ↔ GenerateHas C s
[PROOFSTEP]
refine' ⟨_, GenerateHas.compl⟩
[GOAL]
α : Type u_1
d : DynkinSystem α
C : Set (Set α)
s : Set α
⊢ GenerateHas C sᶜ → GenerateHas C s
[PROOFSTEP]
intro h
[GOAL]
α : Type u_1
d : DynkinSystem α
C : Set (Set α)
s : Set α
h : GenerateHas C sᶜ
⊢ GenerateHas C s
[PROOFSTEP]
convert GenerateHas.compl h
[GOAL]
case h.e'_3
α : Type u_1
d : DynkinSystem α
C : Set (Set α)
s : Set α
h : GenerateHas C sᶜ
⊢ s = sᶜᶜ
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
d : DynkinSystem α
h_inter : ∀ (s₁ s₂ : Set α), Has d s₁ → Has d s₂ → Has d (s₁ ∩ s₂)
f : ℕ → Set α
hf : ∀ (i : ℕ), Has d (f i)
⊢ Has d (⋃ (i : ℕ), f i)
[PROOFSTEP]
rw [← iUnion_disjointed]
[GOAL]
α : Type u_1
d : DynkinSystem α
h_inter : ∀ (s₁ s₂ : Set α), Has d s₁ → Has d s₂ → Has d (s₁ ∩ s₂)
f : ℕ → Set α
hf : ∀ (i : ℕ), Has d (f i)
⊢ Has d (⋃ (n : ℕ), disjointed (fun i => f i) n)
[PROOFSTEP]
exact
  d.has_iUnion (disjoint_disjointed _) fun n =>
    disjointedRec (fun (t : Set α) i h => h_inter _ _ h <| d.has_compl <| hf i) (hf n)
[GOAL]
α : Type u_1
d : DynkinSystem α
s : Set α
h : Has d s
⊢ (fun t => Has d (t ∩ s)) ∅
[PROOFSTEP]
simp [d.has_empty]
[GOAL]
α : Type u_1
d : DynkinSystem α
s : Set α
h : Has d s
t : Set α
hts : (fun t => Has d (t ∩ s)) t
⊢ (fun t => Has d (t ∩ s)) tᶜ
[PROOFSTEP]
simp only []
[GOAL]
α : Type u_1
d : DynkinSystem α
s : Set α
h : Has d s
t : Set α
hts : (fun t => Has d (t ∩ s)) t
⊢ Has d (tᶜ ∩ s)
[PROOFSTEP]
have : tᶜ ∩ s = (t ∩ s)ᶜ \ sᶜ := Set.ext fun x => by by_cases h : x ∈ s <;> simp [h]
[GOAL]
α : Type u_1
d : DynkinSystem α
s : Set α
h : Has d s
t : Set α
hts : (fun t => Has d (t ∩ s)) t
x : α
⊢ x ∈ tᶜ ∩ s ↔ x ∈ (t ∩ s)ᶜ \ sᶜ
[PROOFSTEP]
by_cases h : x ∈ s
[GOAL]
case pos
α : Type u_1
d : DynkinSystem α
s : Set α
h✝ : Has d s
t : Set α
hts : (fun t => Has d (t ∩ s)) t
x : α
h : x ∈ s
⊢ x ∈ tᶜ ∩ s ↔ x ∈ (t ∩ s)ᶜ \ sᶜ
[PROOFSTEP]
simp [h]
[GOAL]
case neg
α : Type u_1
d : DynkinSystem α
s : Set α
h✝ : Has d s
t : Set α
hts : (fun t => Has d (t ∩ s)) t
x : α
h : ¬x ∈ s
⊢ x ∈ tᶜ ∩ s ↔ x ∈ (t ∩ s)ᶜ \ sᶜ
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
d : DynkinSystem α
s : Set α
h : Has d s
t : Set α
hts : (fun t => Has d (t ∩ s)) t
this : tᶜ ∩ s = (t ∩ s)ᶜ \ sᶜ
⊢ Has d (tᶜ ∩ s)
[PROOFSTEP]
rw [this]
[GOAL]
α : Type u_1
d : DynkinSystem α
s : Set α
h : Has d s
t : Set α
hts : (fun t => Has d (t ∩ s)) t
this : tᶜ ∩ s = (t ∩ s)ᶜ \ sᶜ
⊢ Has d ((t ∩ s)ᶜ \ sᶜ)
[PROOFSTEP]
exact d.has_diff (d.has_compl hts) (d.has_compl h) (compl_subset_compl.mpr <| inter_subset_right _ _)
[GOAL]
α : Type u_1
d : DynkinSystem α
s : Set α
h : Has d s
f : ℕ → Set α
hd : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), (fun t => Has d (t ∩ s)) (f i)
⊢ (fun t => Has d (t ∩ s)) (⋃ (i : ℕ), f i)
[PROOFSTEP]
simp only []
[GOAL]
α : Type u_1
d : DynkinSystem α
s : Set α
h : Has d s
f : ℕ → Set α
hd : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), (fun t => Has d (t ∩ s)) (f i)
⊢ Has d ((⋃ (i : ℕ), f i) ∩ s)
[PROOFSTEP]
rw [iUnion_inter]
[GOAL]
α : Type u_1
d : DynkinSystem α
s : Set α
h : Has d s
f : ℕ → Set α
hd : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), (fun t => Has d (t ∩ s)) (f i)
⊢ Has d (⋃ (i : ℕ), f i ∩ s)
[PROOFSTEP]
refine' d.has_iUnion_nat _ hf
[GOAL]
α : Type u_1
d : DynkinSystem α
s : Set α
h : Has d s
f : ℕ → Set α
hd : Pairwise (Disjoint on f)
hf : ∀ (i : ℕ), (fun t => Has d (t ∩ s)) (f i)
⊢ Pairwise (Disjoint on fun i => f i ∩ s)
[PROOFSTEP]
exact hd.mono fun i j => Disjoint.mono (inter_subset_left _ _) (inter_subset_left _ _)
[GOAL]
α : Type u_1
d : DynkinSystem α
s : Set (Set α)
hs : IsPiSystem s
t₁ t₂ : Set α
ht₁ : Has (generate s) t₁
ht₂ : Has (generate s) t₂
s₁ : Set α
hs₁ : s₁ ∈ s
this✝¹ : Has (generate s) s₁
this✝ : generate s ≤ restrictOn (generate s) this✝¹
this : Has (generate s) (t₂ ∩ s₁)
⊢ Has (generate s) (s₁ ∩ t₂)
[PROOFSTEP]
rwa [inter_comm]
[GOAL]
α : Type u_1
d : DynkinSystem α
s : Set (Set α)
hs : IsPiSystem s
⊢ ofMeasurableSpace
      (toMeasurableSpace (generate s)
        (_ : ∀ (t₁ t₂ : Set α), Has (generate s) t₁ → Has (generate s) t₂ → Has (generate s) (t₁ ∩ t₂))) ≤
    ofMeasurableSpace (generateFrom s)
[PROOFSTEP]
rw [ofMeasurableSpace_toMeasurableSpace]
[GOAL]
α : Type u_1
d : DynkinSystem α
s : Set (Set α)
hs : IsPiSystem s
⊢ generate s ≤ ofMeasurableSpace (generateFrom s)
[PROOFSTEP]
exact generate_le _ fun t ht => measurableSet_generateFrom ht
[GOAL]
α : Type u_1
C : Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : C ∅
h_basic : ∀ (t : Set α), t ∈ s → C t
h_compl : ∀ (t : Set α), MeasurableSet t → C t → C tᶜ
h_union :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ (i : ℕ), f i)
⊢ MeasurableSet = DynkinSystem.GenerateHas s
[PROOFSTEP]
rw [h_eq, DynkinSystem.generateFrom_eq h_inter]
[GOAL]
α : Type u_1
C : Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : C ∅
h_basic : ∀ (t : Set α), t ∈ s → C t
h_compl : ∀ (t : Set α), MeasurableSet t → C t → C tᶜ
h_union :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ (i : ℕ), f i)
⊢ MeasurableSet = DynkinSystem.GenerateHas s
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
C : Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : C ∅
h_basic : ∀ (t : Set α), t ∈ s → C t
h_compl : ∀ (t : Set α), MeasurableSet t → C t → C tᶜ
h_union :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ (i : ℕ), f i)
eq : MeasurableSet = DynkinSystem.GenerateHas s
t : Set α
ht : MeasurableSet t
⊢ DynkinSystem.GenerateHas s t
[PROOFSTEP]
rwa [eq] at ht 
[GOAL]
α : Type u_1
C : Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : C ∅
h_basic : ∀ (t : Set α), t ∈ s → C t
h_compl : ∀ (t : Set α), MeasurableSet t → C t → C tᶜ
h_union :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ (i : ℕ), f i)
eq : MeasurableSet = DynkinSystem.GenerateHas s
t✝ : Set α
ht✝ : MeasurableSet t✝
this : DynkinSystem.GenerateHas s t✝
t : Set α
ht : DynkinSystem.GenerateHas s t
⊢ MeasurableSet t
[PROOFSTEP]
rw [eq]
[GOAL]
α : Type u_1
C : Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : C ∅
h_basic : ∀ (t : Set α), t ∈ s → C t
h_compl : ∀ (t : Set α), MeasurableSet t → C t → C tᶜ
h_union :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ (i : ℕ), f i)
eq : MeasurableSet = DynkinSystem.GenerateHas s
t✝ : Set α
ht✝ : MeasurableSet t✝
this : DynkinSystem.GenerateHas s t✝
t : Set α
ht : DynkinSystem.GenerateHas s t
⊢ DynkinSystem.GenerateHas s t
[PROOFSTEP]
exact ht
[GOAL]
α : Type u_1
C : Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : C ∅
h_basic : ∀ (t : Set α), t ∈ s → C t
h_compl : ∀ (t : Set α), MeasurableSet t → C t → C tᶜ
h_union :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ (i : ℕ), f i)
eq : MeasurableSet = DynkinSystem.GenerateHas s
t : Set α
ht✝ : MeasurableSet t
this : DynkinSystem.GenerateHas s t
f : ℕ → Set α
hf : Pairwise (Disjoint on f)
ht : ∀ (i : ℕ), DynkinSystem.GenerateHas s (f i)
i : ℕ
⊢ MeasurableSet (f i)
[PROOFSTEP]
rw [eq]
[GOAL]
α : Type u_1
C : Set α → Prop
s : Set (Set α)
m : MeasurableSpace α
h_eq : m = generateFrom s
h_inter : IsPiSystem s
h_empty : C ∅
h_basic : ∀ (t : Set α), t ∈ s → C t
h_compl : ∀ (t : Set α), MeasurableSet t → C t → C tᶜ
h_union :
  ∀ (f : ℕ → Set α),
    Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), C (f i)) → C (⋃ (i : ℕ), f i)
eq : MeasurableSet = DynkinSystem.GenerateHas s
t : Set α
ht✝ : MeasurableSet t
this : DynkinSystem.GenerateHas s t
f : ℕ → Set α
hf : Pairwise (Disjoint on f)
ht : ∀ (i : ℕ), DynkinSystem.GenerateHas s (f i)
i : ℕ
⊢ DynkinSystem.GenerateHas s (f i)
[PROOFSTEP]
exact ht _
