α : Type u_1
β : Type ?u.72615
γ : Type ?u.72618
ι : Sort u_2
ι' : Sort ?u.72624
ι₂ : Sort ?u.72627
κ : ι → Sort ?u.72632
κ₁ : ι → Sort ?u.72637
κ₂ : ι → Sort ?u.72642
κ' : ι' → Sort ?u.72647
r : α → α → Prop
f : ι → Set α
hd : Directed (fun x x_1 => x ⊆ x_1) f
h : ∀ (x : ι), DirectedOn r (f x)
⊢ ∀ (x : α) (x_1 : ι), x ∈ f x_1 → ∀ (y : α) (x_2 : ι), y ∈ f x_2 → ∃ z, (∃ i, z ∈ f i) ∧ r x z ∧ r y z
α : Type u_1
β : Type ?u.72615
γ : Type ?u.72618
ι : Sort u_2
ι' : Sort ?u.72624
ι₂ : Sort ?u.72627
κ : ι → Sort ?u.72632
κ₁ : ι → Sort ?u.72637
κ₂ : ι → Sort ?u.72642
κ' : ι' → Sort ?u.72647
r : α → α → Prop
f : ι → Set α
hd : Directed (fun x x_1 => x ⊆ x_1) f
h : ∀ (x : ι), DirectedOn r (f x)
⊢ DirectedOn r (⋃ (x : ι), f x)
simp only [DirectedOn, exists_prop, mem_iUnion, exists_imp]
no goals
α : Type u_1
β : Type ?u.72615
γ : Type ?u.72618
ι : Sort u_2
ι' : Sort ?u.72624
ι₂ : Sort ?u.72627
κ : ι → Sort ?u.72632
κ₁ : ι → Sort ?u.72637
κ₂ : ι → Sort ?u.72642
κ' : ι' → Sort ?u.72647
r : α → α → Prop
f : ι → Set α
hd : Directed (fun x x_1 => x ⊆ x_1) f
h : ∀ (x : ι), DirectedOn r (f x)
⊢ ∀ (x : α) (x_1 : ι), x ∈ f x_1 → ∀ (y : α) (x_2 : ι), y ∈ f x_2 → ∃ z, (∃ i, z ∈ f i) ∧ r x z ∧ r y z
exact fun a₁ b₁ fb₁ a₂ b₂ fb₂ =>
  let ⟨z, zb₁, zb₂⟩ := hd b₁ b₂
  let ⟨x, xf, xa₁, xa₂⟩ := h z a₁ (zb₁ fb₁) a₂ (zb₂ fb₂)
  ⟨x, ⟨z, xf⟩, xa₁, xa₂⟩