[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
s : Set α
⊢ DirectedOn r s ↔ Directed r Subtype.val
[PROOFSTEP]
simp [Directed, DirectedOn]
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
s : Set α
⊢ (∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → ∃ z, z ∈ s ∧ r x z ∧ r y z) ↔
    ∀ (a : α), a ∈ s → ∀ (a_1 : α), a_1 ∈ s → ∃ a_2, r a a_2 ∧ a_2 ∈ s ∧ r a_1 a_2
[PROOFSTEP]
refine' ball_congr fun x _ => by simp [And.comm, and_assoc]
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
s : Set α
x : α
x✝ : x ∈ s
⊢ (∀ (y : α), y ∈ s → ∃ z, z ∈ s ∧ r x z ∧ r y z) ↔ ∀ (a : α), a ∈ s → ∃ a_1, r x a_1 ∧ a_1 ∈ s ∧ r a a_1
[PROOFSTEP]
simp [And.comm, and_assoc]
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
f : ι → α
⊢ Directed r f ↔ DirectedOn r (Set.range f)
[PROOFSTEP]
simp_rw [Directed, DirectedOn, Set.forall_range_iff, Set.exists_range_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
s : Set β
f : β → α
⊢ DirectedOn r (f '' s) ↔ DirectedOn (f ⁻¹'o r) s
[PROOFSTEP]
simp only [DirectedOn, Set.mem_image, exists_exists_and_eq_and, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
  Order.Preimage]
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x x_1 => x ≤ x_1) f
he : Injective e
⊢ Directed (fun x x_1 => x ≤ x_1) (extend e f ⊥)
[PROOFSTEP]
intro a b
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x x_1 => x ≤ x_1) f
he : Injective e
a b : β
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) (extend e f ⊥ a) (extend e f ⊥ z) ∧ (fun x x_1 => x ≤ x_1) (extend e f ⊥ b) (extend e f ⊥ z)
[PROOFSTEP]
rcases(em (∃ i, e i = a)).symm with (ha | ⟨i, rfl⟩)
[GOAL]
case inl
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x x_1 => x ≤ x_1) f
he : Injective e
a b : β
ha : ¬∃ i, e i = a
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) (extend e f ⊥ a) (extend e f ⊥ z) ∧ (fun x x_1 => x ≤ x_1) (extend e f ⊥ b) (extend e f ⊥ z)
[PROOFSTEP]
use b
[GOAL]
case h
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x x_1 => x ≤ x_1) f
he : Injective e
a b : β
ha : ¬∃ i, e i = a
⊢ (fun x x_1 => x ≤ x_1) (extend e f ⊥ a) (extend e f ⊥ b) ∧ (fun x x_1 => x ≤ x_1) (extend e f ⊥ b) (extend e f ⊥ b)
[PROOFSTEP]
simp [Function.extend_apply' _ _ _ ha]
[GOAL]
case inr.intro
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x x_1 => x ≤ x_1) f
he : Injective e
b : β
i : ι
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x x_1 => x ≤ x_1) (extend e f ⊥ b) (extend e f ⊥ z)
[PROOFSTEP]
rcases(em (∃ i, e i = b)).symm with (hb | ⟨j, rfl⟩)
[GOAL]
case inr.intro.inl
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x x_1 => x ≤ x_1) f
he : Injective e
b : β
i : ι
hb : ¬∃ i, e i = b
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x x_1 => x ≤ x_1) (extend e f ⊥ b) (extend e f ⊥ z)
[PROOFSTEP]
use e i
[GOAL]
case h
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x x_1 => x ≤ x_1) f
he : Injective e
b : β
i : ι
hb : ¬∃ i, e i = b
⊢ (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e i)) (extend e f ⊥ (e i)) ∧
    (fun x x_1 => x ≤ x_1) (extend e f ⊥ b) (extend e f ⊥ (e i))
[PROOFSTEP]
simp [Function.extend_apply' _ _ _ hb]
[GOAL]
case inr.intro.inr.intro
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x x_1 => x ≤ x_1) f
he : Injective e
i j : ι
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e j)) (extend e f ⊥ z)
[PROOFSTEP]
rcases hf i j with ⟨k, hi, hj⟩
[GOAL]
case inr.intro.inr.intro.intro.intro
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x x_1 => x ≤ x_1) f
he : Injective e
i j k : ι
hi : f i ≤ f k
hj : f j ≤ f k
⊢ ∃ z,
    (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e j)) (extend e f ⊥ z)
[PROOFSTEP]
use e k
[GOAL]
case h
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x x_1 => x ≤ x_1) f
he : Injective e
i j k : ι
hi : f i ≤ f k
hj : f j ≤ f k
⊢ (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e i)) (extend e f ⊥ (e k)) ∧
    (fun x x_1 => x ≤ x_1) (extend e f ⊥ (e j)) (extend e f ⊥ (e k))
[PROOFSTEP]
simp only [he.extend_apply, *, true_and_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝ : IsDirected α r
⊢ Directed r id
[PROOFSTEP]
convert directed_of r
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝ : IsTotal α r
⊢ IsDirected α r
[PROOFSTEP]
rw [← directed_id_iff]
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝ : IsTotal α r
⊢ Directed r id
[PROOFSTEP]
exact IsTotal.directed _
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : LE α
inst✝ : IsDirected α fun x x_1 => x ≤ x_1
⊢ IsDirected αᵒᵈ fun x x_1 => x ≥ x_1
[PROOFSTEP]
assumption
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : LE α
inst✝ : IsDirected α fun x x_1 => x ≥ x_1
⊢ IsDirected αᵒᵈ fun x x_1 => x ≤ x_1
[PROOFSTEP]
assumption
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
h : Reflexive r
a : α
s : Set α
hd : DirectedOn r s
ha : ∀ (b : α), b ∈ s → ∃ c, c ∈ s ∧ r a c ∧ r b c
⊢ DirectedOn r (insert a s)
[PROOFSTEP]
rintro x (rfl | hx) y (rfl | hy)
[GOAL]
case inl.inl
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
h : Reflexive r
s : Set α
hd : DirectedOn r s
y : α
ha : ∀ (b : α), b ∈ s → ∃ c, c ∈ s ∧ r y c ∧ r b c
⊢ ∃ z, z ∈ insert y s ∧ r y z ∧ r y z
[PROOFSTEP]
exact ⟨y, Set.mem_insert _ _, h _, h _⟩
[GOAL]
case inl.inr
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
h : Reflexive r
s : Set α
hd : DirectedOn r s
x : α
ha : ∀ (b : α), b ∈ s → ∃ c, c ∈ s ∧ r x c ∧ r b c
y : α
hy : y ∈ s
⊢ ∃ z, z ∈ insert x s ∧ r x z ∧ r y z
[PROOFSTEP]
obtain ⟨w, hws, hwr⟩ := ha y hy
[GOAL]
case inl.inr.intro.intro
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
h : Reflexive r
s : Set α
hd : DirectedOn r s
x : α
ha : ∀ (b : α), b ∈ s → ∃ c, c ∈ s ∧ r x c ∧ r b c
y : α
hy : y ∈ s
w : α
hws : w ∈ s
hwr : r x w ∧ r y w
⊢ ∃ z, z ∈ insert x s ∧ r x z ∧ r y z
[PROOFSTEP]
exact ⟨w, Set.mem_insert_of_mem _ hws, hwr⟩
[GOAL]
case inr.inl
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
h : Reflexive r
s : Set α
hd : DirectedOn r s
x : α
hx : x ∈ s
y : α
ha : ∀ (b : α), b ∈ s → ∃ c, c ∈ s ∧ r y c ∧ r b c
⊢ ∃ z, z ∈ insert y s ∧ r x z ∧ r y z
[PROOFSTEP]
obtain ⟨w, hws, hwr⟩ := ha x hx
[GOAL]
case inr.inl.intro.intro
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
h : Reflexive r
s : Set α
hd : DirectedOn r s
x : α
hx : x ∈ s
y : α
ha : ∀ (b : α), b ∈ s → ∃ c, c ∈ s ∧ r y c ∧ r b c
w : α
hws : w ∈ s
hwr : r y w ∧ r x w
⊢ ∃ z, z ∈ insert y s ∧ r x z ∧ r y z
[PROOFSTEP]
exact ⟨w, Set.mem_insert_of_mem _ hws, hwr.symm⟩
[GOAL]
case inr.inr
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
h : Reflexive r
a : α
s : Set α
hd : DirectedOn r s
ha : ∀ (b : α), b ∈ s → ∃ c, c ∈ s ∧ r a c ∧ r b c
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ∃ z, z ∈ insert a s ∧ r x z ∧ r y z
[PROOFSTEP]
obtain ⟨w, hws, hwr⟩ := hd x hx y hy
[GOAL]
case inr.inr.intro.intro
α : Type u
β : Type v
ι : Sort w
r r' s✝ : α → α → Prop
h : Reflexive r
a : α
s : Set α
hd : DirectedOn r s
ha : ∀ (b : α), b ∈ s → ∃ c, c ∈ s ∧ r a c ∧ r b c
x : α
hx : x ∈ s
y : α
hy : y ∈ s
w : α
hws : w ∈ s
hwr : r x w ∧ r y w
⊢ ∃ z, z ∈ insert a s ∧ r x z ∧ r y z
[PROOFSTEP]
exact ⟨w, Set.mem_insert_of_mem _ hws, hwr⟩
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
h : Reflexive r
a b : α
hab : r a b
⊢ DirectedOn r {b, a}
[PROOFSTEP]
rw [Set.pair_comm]
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
h : Reflexive r
a b : α
hab : r a b
⊢ DirectedOn r {a, b}
[PROOFSTEP]
apply directedOn_pair h hab
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝³ : Preorder α
a : α
inst✝² : PartialOrder β
inst✝¹ : IsDirected β fun x x_1 => x ≥ x_1
inst✝ : Nontrivial β
⊢ ∃ a b, a < b
[PROOFSTEP]
rcases exists_pair_ne β with ⟨a, b, hne⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝³ : Preorder α
a✝ : α
inst✝² : PartialOrder β
inst✝¹ : IsDirected β fun x x_1 => x ≥ x_1
inst✝ : Nontrivial β
a b : β
hne : a ≠ b
⊢ ∃ a b, a < b
[PROOFSTEP]
rcases isBot_or_exists_lt a with (ha | ⟨c, hc⟩)
[GOAL]
case intro.intro.inl
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝³ : Preorder α
a✝ : α
inst✝² : PartialOrder β
inst✝¹ : IsDirected β fun x x_1 => x ≥ x_1
inst✝ : Nontrivial β
a b : β
hne : a ≠ b
ha : IsBot a
⊢ ∃ a b, a < b
case intro.intro.inr.intro
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝³ : Preorder α
a✝ : α
inst✝² : PartialOrder β
inst✝¹ : IsDirected β fun x x_1 => x ≥ x_1
inst✝ : Nontrivial β
a b : β
hne : a ≠ b
c : β
hc : c < a
⊢ ∃ a b, a < b
[PROOFSTEP]
exacts [⟨a, b, (ha b).lt_of_ne hne⟩, ⟨_, _, hc⟩]
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
⊢ Monotone f
[PROOFSTEP]
intro a b hab
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ f a ≤ f b
[PROOFSTEP]
have e1 : IsLUB (f '' { a, b }) (f b) := by
  apply h
  · exact Set.insert_nonempty _ _
  · exact directedOn_pair le_refl hab
  · rw [IsLUB, upperBounds_insert, upperBounds_singleton,
      Set.inter_eq_self_of_subset_right (Set.Ici_subset_Ici.mpr hab)]
    exact isLeast_Ici
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ IsLUB (f '' {a, b}) (f b)
[PROOFSTEP]
apply h
[GOAL]
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ Set.Nonempty {a, b}
[PROOFSTEP]
exact Set.insert_nonempty _ _
[GOAL]
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ DirectedOn (fun x x_1 => x ≤ x_1) {a, b}
[PROOFSTEP]
exact directedOn_pair le_refl hab
[GOAL]
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ IsLUB {a, b} b
[PROOFSTEP]
rw [IsLUB, upperBounds_insert, upperBounds_singleton, Set.inter_eq_self_of_subset_right (Set.Ici_subset_Ici.mpr hab)]
[GOAL]
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
⊢ IsLeast (Set.Ici b) b
[PROOFSTEP]
exact isLeast_Ici
[GOAL]
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
e1 : IsLUB (f '' {a, b}) (f b)
⊢ f a ≤ f b
[PROOFSTEP]
apply e1.1
[GOAL]
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
e1 : IsLUB (f '' {a, b}) (f b)
⊢ f a ∈ f '' {a, b}
[PROOFSTEP]
rw [Set.image_pair]
[GOAL]
case a
α : Type u
β : Type v
ι : Sort w
r r' s : α → α → Prop
inst✝¹ : Preorder α
a✝ : α
inst✝ : Preorder β
f : α → β
h : ScottContinuous f
a b : α
hab : a ≤ b
e1 : IsLUB (f '' {a, b}) (f b)
⊢ f a ∈ {f a, f b}
[PROOFSTEP]
exact Set.mem_insert _ _
