-- Mathlib/MeasureTheory/PiSystem.lean
theorem isPiSystem_iUnion_of_directed_le {α ι} (p : ι → Set (Set α))
    (hp_pi : ∀ n, IsPiSystem (p n)) (hp_directed : Directed (· ≤ ·) p) :
    IsPiSystem (⋃ n, p n)

Proof state:
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 => x1 ≤ x2) p
t1 : Set α
ht1 : ∃ i, t1 ∈ p i
t2 : Set α
ht2 : ∃ i, t2 ∈ p i
h : (t1 ∩ t2).Nonempty
⊢ ∃ i, t1 ∩ t2 ∈ p i

Tactic:
obtain ⟨n, ht1⟩ := ht1

Result:
case intro
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 => x1 ≤ x2) p
t1 t2 : Set α
ht2 : ∃ i, t2 ∈ p i
h : (t1 ∩ t2).Nonempty
n : ι
ht1 : t1 ∈ p n
⊢ ∃ i, t1 ∩ t2 ∈ p i

Proof state:
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 => x1 ≤ x2) p
⊢ IsPiSystem (⋃ n, p n)

Tactic:
intro t1 ht1 t2 ht2 h

Result:
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 => x1 ≤ x2) p
t1 : Set α
ht1 : t1 ∈ ⋃ n, p n
t2 : Set α
ht2 : t2 ∈ ⋃ n, p n
h : (t1 ∩ t2).Nonempty
⊢ t1 ∩ t2 ∈ ⋃ n, p n

Proof state:
case intro
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 => x1 ≤ x2) p
t1 t2 : Set α
ht2 : ∃ i, t2 ∈ p i
h : (t1 ∩ t2).Nonempty
n : ι
ht1 : t1 ∈ p n
⊢ ∃ i, t1 ∩ t2 ∈ p i

Tactic:
obtain ⟨m, ht2⟩ := ht2

Result:
case intro.intro
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 => x1 ≤ x2) p
t1 t2 : Set α
h : (t1 ∩ t2).Nonempty
n : ι
ht1 : t1 ∈ p n
m : ι
ht2 : t2 ∈ p m
⊢ ∃ i, t1 ∩ t2 ∈ p i

Proof state:
case intro.intro.intro.intro
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 => x1 ≤ x2) p
t1 t2 : Set α
h : (t1 ∩ t2).Nonempty
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

Tactic:
exact ⟨k, hp_pi k t1 (hpnk ht1) t2 (hpmk ht2) h⟩

Result:
no goals

Proof state:
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 => x1 ≤ x2) p
t1 : Set α
ht1 : t1 ∈ ⋃ n, p n
t2 : Set α
ht2 : t2 ∈ ⋃ n, p n
h : (t1 ∩ t2).Nonempty
⊢ t1 ∩ t2 ∈ ⋃ n, p n

Tactic:
rw [Set.mem_iUnion] at ht1 ht2 ⊢

Result:
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 => x1 ≤ x2) p
t1 : Set α
ht1 : ∃ i, t1 ∈ p i
t2 : Set α
ht2 : ∃ i, t2 ∈ p i
h : (t1 ∩ t2).Nonempty
⊢ ∃ i, t1 ∩ t2 ∈ p i

Proof state:
case intro.intro
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 => x1 ≤ x2) p
t1 t2 : Set α
h : (t1 ∩ t2).Nonempty
n : ι
ht1 : t1 ∈ p n
m : ι
ht2 : t2 ∈ p m
⊢ ∃ i, t1 ∩ t2 ∈ p i

Tactic:
obtain ⟨k, hpnk, hpmk⟩ : ∃ k, p n ≤ p k ∧ p m ≤ p k := hp_directed n m

Result:
case intro.intro.intro.intro
α : Type u_3
ι : Sort u_4
p : ι → Set (Set α)
hp_pi : ∀ (n : ι), IsPiSystem (p n)
hp_directed : Directed (fun x1 x2 => x1 ≤ x2) p
t1 t2 : Set α
h : (t1 ∩ t2).Nonempty
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