-- Mathlib/Order/Directed.lean
theorem DirectedOn.insert (h : Reflexive r) (a : α) {s : Set α} (hd : DirectedOn r s)
    (ha : ∀ b ∈ s, ∃ c ∈ s, a ≼ c ∧ b ≼ c) : DirectedOn r (insert a s)

Proof state:
case inl.inr
α : Type u
r : α → α → Prop
h : Reflexive r
s : Set α
hd : DirectedOn r s
x : α
ha : ∀ b ∈ s, ∃ c ∈ s, r x c ∧ r b c
y : α
hy : y ∈ s
⊢ ∃ z ∈ insert x s, r x z ∧ r y z

Tactic:
obtain ⟨w, hws, hwr⟩ := ha y hy

Result:
case inl.inr.intro.intro
α : Type u
r : α → α → Prop
h : Reflexive r
s : Set α
hd : DirectedOn r s
x : α
ha : ∀ b ∈ s, ∃ c ∈ s, r x c ∧ r b c
y : α
hy : y ∈ s
w : α
hws : w ∈ s
hwr : r x w ∧ r y w
⊢ ∃ z ∈ insert x s, r x z ∧ r y z

Proof state:
case inr.inl
α : Type u
r : α → α → Prop
h : Reflexive r
s : Set α
hd : DirectedOn r s
x : α
hx : x ∈ s
y : α
ha : ∀ b ∈ s, ∃ c ∈ s, r y c ∧ r b c
⊢ ∃ z ∈ insert y s, r x z ∧ r y z

Tactic:
obtain ⟨w, hws, hwr⟩ := ha x hx

Result:
case inr.inl.intro.intro
α : Type u
r : α → α → Prop
h : Reflexive r
s : Set α
hd : DirectedOn r s
x : α
hx : x ∈ s
y : α
ha : ∀ b ∈ s, ∃ c ∈ s, r y c ∧ r b c
w : α
hws : w ∈ s
hwr : r y w ∧ r x w
⊢ ∃ z ∈ insert y s, r x z ∧ r y z

Proof state:
case inl.inl
α : Type u
r : α → α → Prop
h : Reflexive r
s : Set α
hd : DirectedOn r s
y : α
ha : ∀ b ∈ s, ∃ c ∈ s, r y c ∧ r b c
⊢ ∃ z ∈ insert y s, r y z ∧ r y z

Tactic:
exact ⟨y, Set.mem_insert _ _, h _, h _⟩

Result:
no goals

Proof state:
case inr.inr
α : Type u
r : α → α → Prop
h : Reflexive r
a : α
s : Set α
hd : DirectedOn r s
ha : ∀ b ∈ s, ∃ c ∈ s, r a c ∧ r b c
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ∃ z ∈ insert a s, r x z ∧ r y z

Tactic:
obtain ⟨w, hws, hwr⟩ := hd x hx y hy

Result:
case inr.inr.intro.intro
α : Type u
r : α → α → Prop
h : Reflexive r
a : α
s : Set α
hd : DirectedOn r s
ha : ∀ b ∈ s, ∃ 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 ∈ insert a s, r x z ∧ r y z

Proof state:
case inr.inr.intro.intro
α : Type u
r : α → α → Prop
h : Reflexive r
a : α
s : Set α
hd : DirectedOn r s
ha : ∀ b ∈ s, ∃ 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 ∈ insert a s, r x z ∧ r y z

Tactic:
exact ⟨w, Set.mem_insert_of_mem _ hws, hwr⟩

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
h : Reflexive r
a : α
s : Set α
hd : DirectedOn r s
ha : ∀ b ∈ s, ∃ c ∈ s, r a c ∧ r b c
⊢ DirectedOn r (insert a s)

Tactic:
rintro x (rfl | hx) y (rfl | hy)

Result:
case inl.inl
α : Type u
r : α → α → Prop
h : Reflexive r
s : Set α
hd : DirectedOn r s
y : α
ha : ∀ b ∈ s, ∃ c ∈ s, r y c ∧ r b c
⊢ ∃ z ∈ insert y s, r y z ∧ r y z

case inl.inr
α : Type u
r : α → α → Prop
h : Reflexive r
s : Set α
hd : DirectedOn r s
x : α
ha : ∀ b ∈ s, ∃ c ∈ s, r x c ∧ r b c
y : α
hy : y ∈ s
⊢ ∃ z ∈ insert x s, r x z ∧ r y z

case inr.inl
α : Type u
r : α → α → Prop
h : Reflexive r
s : Set α
hd : DirectedOn r s
x : α
hx : x ∈ s
y : α
ha : ∀ b ∈ s, ∃ c ∈ s, r y c ∧ r b c
⊢ ∃ z ∈ insert y s, r x z ∧ r y z

case inr.inr
α : Type u
r : α → α → Prop
h : Reflexive r
a : α
s : Set α
hd : DirectedOn r s
ha : ∀ b ∈ s, ∃ c ∈ s, r a c ∧ r b c
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ∃ z ∈ insert a s, r x z ∧ r y z

Proof state:
case inl.inr.intro.intro
α : Type u
r : α → α → Prop
h : Reflexive r
s : Set α
hd : DirectedOn r s
x : α
ha : ∀ b ∈ s, ∃ c ∈ s, r x c ∧ r b c
y : α
hy : y ∈ s
w : α
hws : w ∈ s
hwr : r x w ∧ r y w
⊢ ∃ z ∈ insert x s, r x z ∧ r y z

Tactic:
exact ⟨w, Set.mem_insert_of_mem _ hws, hwr⟩

Result:
no goals

Proof state:
case inr.inl.intro.intro
α : Type u
r : α → α → Prop
h : Reflexive r
s : Set α
hd : DirectedOn r s
x : α
hx : x ∈ s
y : α
ha : ∀ b ∈ s, ∃ c ∈ s, r y c ∧ r b c
w : α
hws : w ∈ s
hwr : r y w ∧ r x w
⊢ ∃ z ∈ insert y s, r x z ∧ r y z

Tactic:
exact ⟨w, Set.mem_insert_of_mem _ hws, hwr.symm⟩

Result:
no goals