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
α : Type u_1
ι : Type u_2
π : ι → Set (Set α)
hpi : ∀ (x : ι), IsPiSystem (π x)
S : Set ι
⊢ IsPiSystem (piiUnionInter π S)
rintro t1 ⟨p1, hp1S, f1, hf1m, ht1_eq⟩ t2 ⟨p2, hp2S, f2, hf2m, ht2_eq⟩ h_nonempty
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
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
simp_rw [piiUnionInter, Set.mem_setOf_eq]
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
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
let g n := ite (n ∈ p1) (f1 n) Set.univ ∩ ite (n ∈ p2) (f2 n) Set.univ
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
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
have hp_union_ss : ↑(p1 ∪ p2) ⊆ S := by
  simp only [hp1S, hp2S, Finset.coe_union, union_subset_iff, and_self_iff]
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
⊢ ∃ x, t1 ∩ t2 = ⋂ (x : ι) (_ : x ∈ p1 ∪ p2), g x
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
use p1 ∪ p2, hp_union_ss, g
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
h_inter_eq : t1 ∩ t2 = ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i
n : ι
hn : n ∈ p1 ∪ p2
⊢ g n ∈ π n
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
h_inter_eq : t1 ∩ t2 = ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i
⊢ ∃ x, t1 ∩ t2 = ⋂ (x : ι) (_ : x ∈ p1 ∪ p2), g x
refine' ⟨fun n hn => _, h_inter_eq⟩
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
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
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
h_inter_eq : t1 ∩ t2 = ⋂ (i : ι) (_ : i ∈ p1 ∪ p2), g i
n : ι
hn : n ∈ p1 ∪ p2
⊢ g n ∈ π n
simp only []
case intro.intro.intro.intro.intro.intro.intro.intro.inl.inl
α : 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

case intro.intro.intro.intro.intro.intro.intro.intro.inl.inr
α : 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

case intro.intro.intro.intro.intro.intro.intro.intro.inr.inl
α : 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

case intro.intro.intro.intro.intro.intro.intro.intro.inr.inr
α : 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
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
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
split_ifs with hn1 hn2 h
no goals
α : 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
simp only [hp1S, hp2S, Finset.coe_union, union_subset_iff, and_self_iff]
α : 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
α : 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
rw [ht1_eq, ht2_eq]
α : 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
α : 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
simp_rw [← Set.inf_eq_inter]
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
α : 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
ext1 x
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
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
simp only [inf_eq_inter, mem_inter_iff, mem_iInter, Finset.mem_union]
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

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

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
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
refine' ⟨fun h i _ => _, fun h => ⟨fun i hi1 => _, fun i hi2 => _⟩⟩
case h.refine'_1.inl.inl
α : 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 h.refine'_1.inl.inr
α : 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 h.refine'_1.inr.inl
α : 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 h.refine'_1.inr.inr
α : 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
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
split_ifs with h_1 h_2 h_2
no goals
case h.refine'_1.inl.inl
α : 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 h.refine'_1.inl.inr
α : 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 h.refine'_1.inr.inl
α : 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 h.refine'_1.inr.inr
α : 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
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 _⟩]
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
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
specialize h i (Or.inl hi1)
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
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
rw [if_pos hi1] at h
no goals
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
exact h.1
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
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
specialize h i (Or.inr hi2)
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
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
rw [if_pos hi2] at h
no goals
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
exact h.2
case intro.intro.intro.intro.intro.intro.intro.intro.inl.inl
α : 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
case intro.intro.intro.intro.intro.intro.intro.intro.inl.inl
α : 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
refine' hpi n (f1 n) (hf1m n hn1) (f2 n) (hf2m n hn2) (Set.nonempty_iff_ne_empty.2 fun h => _)
case intro.intro.intro.intro.intro.intro.intro.intro.inl.inl
α : 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
case intro.intro.intro.intro.intro.intro.intro.intro.inl.inl
α : 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
rw [h_inter_eq] at h_nonempty
case intro.intro.intro.intro.intro.intro.intro.intro.inl.inl
α : 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) = ∅
case intro.intro.intro.intro.intro.intro.intro.intro.inl.inl
α : 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
suffices h_empty : (⋂ i ∈ p1 ∪ p2, g i) = ∅
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) = ∅
case intro.intro.intro.intro.intro.intro.intro.intro.inl.inl
α : 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) = ∅
exact (Set.not_nonempty_iff_eq_empty.mpr h_empty) h_nonempty
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) ⊆ ∅
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) = ∅
refine' le_antisymm (Set.iInter_subset_of_subset n _) (Set.empty_subset _)
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 ⊆ ∅
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) ⊆ ∅
refine' Set.iInter_subset_of_subset hn _
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 ⊆ ∅
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 ⊆ ∅
simp_rw [if_pos hn1, if_pos hn2]
no goals
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 ⊆ ∅
exact h.subset
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.inl.inr
α : 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
simp [hf1m n hn1]
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.inr.inl
α : 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
simp [hf2m n h]
no goals
case intro.intro.intro.intro.intro.intro.intro.intro.inr.inr
α : 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
exact absurd hn (by simp [hn1, h])
no goals
α : 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
simp [hn1, h]