α : 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
α : 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)
intro t1 ht1 t2 ht2 h
α : 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
α : 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
rw [Set.mem_iUnion] at ht1 ht2⊢
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
α : 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
cases' ht1 with n ht1
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
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
cases' ht2 with m ht2
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
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
obtain ⟨k, hpnk, hpmk⟩ : ∃ k, p n ≤ p k ∧ p m ≤ p k := hp_directed n m
no goals
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
exact ⟨k, hp_pi k t1 (hpnk ht1) t2 (hpmk ht2) h⟩