-- Mathlib/Order/Directed.lean
theorem Directed.extend_bot [Preorder α] [OrderBot α] {e : ι → β} {f : ι → α}
    (hf : Directed (· ≤ ·) f) (he : Function.Injective e) :
    Directed (· ≤ ·) (Function.extend e f ⊥)

Proof state:
case inr.intro.inr.intro.intro.intro
α : Type u
β : Type v
ι : Sort w
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 => x1 ≤ x2) f
he : Injective e
i j k : ι
hi : f i ≤ f k
hj : f j ≤ f k
⊢ ∃ z,
    (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ (e j)) (extend e f ⊥ z)

Tactic:
use e k

Result:
case h
α : Type u
β : Type v
ι : Sort w
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 => x1 ≤ x2) f
he : Injective e
i j k : ι
hi : f i ≤ f k
hj : f j ≤ f k
⊢ (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ (e k)) ∧
    (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ (e j)) (extend e f ⊥ (e k))

Proof state:
case inr.intro.inr.intro
α : Type u
β : Type v
ι : Sort w
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 => x1 ≤ x2) f
he : Injective e
i j : ι
⊢ ∃ z,
    (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ (e j)) (extend e f ⊥ z)

Tactic:
rcases hf i j with ⟨k, hi, hj⟩

Result:
case inr.intro.inr.intro.intro.intro
α : Type u
β : Type v
ι : Sort w
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 => x1 ≤ x2) f
he : Injective e
i j k : ι
hi : f i ≤ f k
hj : f j ≤ f k
⊢ ∃ z,
    (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ (e j)) (extend e f ⊥ z)

Proof state:
α : Type u
β : Type v
ι : Sort w
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 => x1 ≤ x2) f
he : Injective e
a b : β
⊢ ∃ z,
    (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ a) (extend e f ⊥ z) ∧ (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)

Tactic:
rcases (em (∃ i, e i = a)).symm with (ha | ⟨i, rfl⟩)

Result:
case inl
α : Type u
β : Type v
ι : Sort w
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 => x1 ≤ x2) f
he : Injective e
a b : β
ha : ¬∃ i, e i = a
⊢ ∃ z,
    (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ a) (extend e f ⊥ z) ∧ (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)

case inr.intro
α : Type u
β : Type v
ι : Sort w
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 => x1 ≤ x2) f
he : Injective e
b : β
i : ι
⊢ ∃ z,
    (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)

Proof state:
case inl
α : Type u
β : Type v
ι : Sort w
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 => x1 ≤ x2) f
he : Injective e
a b : β
ha : ¬∃ i, e i = a
⊢ ∃ z,
    (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ a) (extend e f ⊥ z) ∧ (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)

Tactic:
use b

Result:
case h
α : Type u
β : Type v
ι : Sort w
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 => x1 ≤ x2) f
he : Injective e
a b : β
ha : ¬∃ i, e i = a
⊢ (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ a) (extend e f ⊥ b) ∧ (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ b)

Proof state:
case inr.intro.inl
α : Type u
β : Type v
ι : Sort w
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 => x1 ≤ x2) f
he : Injective e
b : β
i : ι
hb : ¬∃ i, e i = b
⊢ ∃ z,
    (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)

Tactic:
use e i

Result:
case h
α : Type u
β : Type v
ι : Sort w
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 => x1 ≤ x2) f
he : Injective e
b : β
i : ι
hb : ¬∃ i, e i = b
⊢ (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ (e i)) ∧
    (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ (e i))

Proof state:
case h
α : Type u
β : Type v
ι : Sort w
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 => x1 ≤ x2) f
he : Injective e
a b : β
ha : ¬∃ i, e i = a
⊢ (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ a) (extend e f ⊥ b) ∧ (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ b)

Tactic:
simp [Function.extend_apply' _ _ _ ha]

Result:
no goals

Proof state:
α : Type u
β : Type v
ι : Sort w
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 => x1 ≤ x2) f
he : Injective e
⊢ Directed (fun x1 x2 => x1 ≤ x2) (extend e f ⊥)

Tactic:
intro a b

Result:
α : Type u
β : Type v
ι : Sort w
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 => x1 ≤ x2) f
he : Injective e
a b : β
⊢ ∃ z,
    (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ a) (extend e f ⊥ z) ∧ (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)

Proof state:
case inr.intro
α : Type u
β : Type v
ι : Sort w
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 => x1 ≤ x2) f
he : Injective e
b : β
i : ι
⊢ ∃ z,
    (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)

Tactic:
rcases (em (∃ i, e i = b)).symm with (hb | ⟨j, rfl⟩)

Result:
case inr.intro.inl
α : Type u
β : Type v
ι : Sort w
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 => x1 ≤ x2) f
he : Injective e
b : β
i : ι
hb : ¬∃ i, e i = b
⊢ ∃ z,
    (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ z)

case inr.intro.inr.intro
α : Type u
β : Type v
ι : Sort w
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 => x1 ≤ x2) f
he : Injective e
i j : ι
⊢ ∃ z,
    (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ z) ∧
      (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ (e j)) (extend e f ⊥ z)

Proof state:
case h
α : Type u
β : Type v
ι : Sort w
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 => x1 ≤ x2) f
he : Injective e
i j k : ι
hi : f i ≤ f k
hj : f j ≤ f k
⊢ (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ (e k)) ∧
    (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ (e j)) (extend e f ⊥ (e k))

Tactic:
simp only [he.extend_apply, *, true_and]

Result:
no goals

Proof state:
case h
α : Type u
β : Type v
ι : Sort w
inst✝¹ : Preorder α
inst✝ : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun x1 x2 => x1 ≤ x2) f
he : Injective e
b : β
i : ι
hb : ¬∃ i, e i = b
⊢ (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ (e i)) (extend e f ⊥ (e i)) ∧
    (fun x1 x2 => x1 ≤ x2) (extend e f ⊥ b) (extend e f ⊥ (e i))

Tactic:
simp [Function.extend_apply' _ _ _ hb]

Result:
no goals