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.insert y s ∧ r y z ∧ r y z

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.insert x s ∧ r x z ∧ r y z

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.insert y s ∧ r x z ∧ r y z

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.insert a s ∧ r x z ∧ r y z
α : 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.insert a s)
rintro x (rfl | hx) y (rfl | hy)
no goals
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.insert y s ∧ r y z ∧ r y z
exact ⟨y, Set.mem_insert _ _, h _, h _⟩
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.insert x s ∧ r x z ∧ r y z
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.insert x s ∧ r x z ∧ r y z
obtain ⟨w, hws, hwr⟩ := ha y hy
no goals
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.insert x s ∧ r x z ∧ r y z
exact ⟨w, Set.mem_insert_of_mem _ hws, hwr⟩
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.insert y s ∧ r x z ∧ r y z
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.insert y s ∧ r x z ∧ r y z
obtain ⟨w, hws, hwr⟩ := ha x hx
no goals
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.insert y s ∧ r x z ∧ r y z
exact ⟨w, Set.mem_insert_of_mem _ hws, hwr.symm⟩
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.insert a s ∧ r x z ∧ r y z
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.insert a s ∧ r x z ∧ r y z
obtain ⟨w, hws, hwr⟩ := hd x hx y hy
no goals
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.insert a s ∧ r x z ∧ r y z
exact ⟨w, Set.mem_insert_of_mem _ hws, hwr⟩