-- Mathlib/Data/Set/Pairwise/Lattice.lean
theorem pairwise_iUnion {f : κ → Set α} (h : Directed (· ⊆ ·) f) :
    (⋃ n, f n).Pairwise r ↔ ∀ n, (f n).Pairwise r

Proof state:
case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : i ∈ ⋃ n, f n
j : α
hj : j ∈ ⋃ n, f n
hij : i ≠ j
⊢ r i j

Tactic:
rcases mem_iUnion.1 hi with ⟨m, hm⟩

Result:
case mpr.intro
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : i ∈ ⋃ n, f n
j : α
hj : j ∈ ⋃ n, f n
hij : i ≠ j
m : κ
hm : i ∈ f m
⊢ r i j

Proof state:
case mpr.intro
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : i ∈ ⋃ n, f n
j : α
hj : j ∈ ⋃ n, f n
hij : i ≠ j
m : κ
hm : i ∈ f m
⊢ r i j

Tactic:
rcases mem_iUnion.1 hj with ⟨n, hn⟩

Result:
case mpr.intro.intro
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : i ∈ ⋃ n, f n
j : α
hj : j ∈ ⋃ n, f n
hij : i ≠ j
m : κ
hm : i ∈ f m
n : κ
hn : j ∈ f n
⊢ r i j

Proof state:
case mpr.intro.intro
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : i ∈ ⋃ n, f n
j : α
hj : j ∈ ⋃ n, f n
hij : i ≠ j
m : κ
hm : i ∈ f m
n : κ
hn : j ∈ f n
⊢ r i j

Tactic:
rcases h m n with ⟨p, mp, np⟩

Result:
case mpr.intro.intro.intro.intro
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : i ∈ ⋃ n, f n
j : α
hj : j ∈ ⋃ n, f n
hij : i ≠ j
m : κ
hm : i ∈ f m
n : κ
hn : j ∈ f n
p : κ
mp : f m ⊆ f p
np : f n ⊆ f p
⊢ r i j

Proof state:
case mp
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
H : (⋃ n, f n).Pairwise r
n : κ
⊢ (f n).Pairwise r

Tactic:
exact Pairwise.mono (subset_iUnion _ _) H

Result:
no goals

Proof state:
case mp
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
⊢ (⋃ n, f n).Pairwise r → ∀ (n : κ), (f n).Pairwise r

Tactic:
intro H n

Result:
case mp
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
H : (⋃ n, f n).Pairwise r
n : κ
⊢ (f n).Pairwise r

Proof state:
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
⊢ (⋃ n, f n).Pairwise r ↔ ∀ (n : κ), (f n).Pairwise r

Tactic:
constructor

Result:
case mp
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
⊢ (⋃ n, f n).Pairwise r → ∀ (n : κ), (f n).Pairwise r

case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
⊢ (∀ (n : κ), (f n).Pairwise r) → (⋃ n, f n).Pairwise r

Proof state:
case mpr.intro.intro.intro.intro
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : i ∈ ⋃ n, f n
j : α
hj : j ∈ ⋃ n, f n
hij : i ≠ j
m : κ
hm : i ∈ f m
n : κ
hn : j ∈ f n
p : κ
mp : f m ⊆ f p
np : f n ⊆ f p
⊢ r i j

Tactic:
exact H p (mp hm) (np hn) hij

Result:
no goals

Proof state:
case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
⊢ (∀ (n : κ), (f n).Pairwise r) → (⋃ n, f n).Pairwise r

Tactic:
intro H i hi j hj hij

Result:
case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
h : Directed (fun x1 x2 => x1 ⊆ x2) f
H : ∀ (n : κ), (f n).Pairwise r
i : α
hi : i ∈ ⋃ n, f n
j : α
hj : j ∈ ⋃ n, f n
hij : i ≠ j
⊢ r i j