awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Set β
h : DirectedOn r (f '' s)
x : β
hx : x ∈ s
y : β
hy : y ∈ s
obtain : ∀ (z : β) (hz : z ∈ s) (hz' : r (f x) (f z) ∧ r (f y) (f z)), ∃ z ∈ s, (r on f) x z ∧ (r on f) y z
⊢ ∃ z ∈ s, (r on f) x z ∧ (r on f) y z

Tactic:
obtain ⟨_, ⟨z, hz, rfl⟩, hz'⟩ := h (f x) (Set.mem_image_of_mem f hx) (f y)
    (Set.mem_image_of_mem f hy)

Premises used: Set.mem_image_of_mem, rfl
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
f : β → α
s : Set β
h : DirectedOn r (f '' s)
x : β
hx : x ∈ s
y : β
hy : y ∈ s
z : β
hz : z ∈ s
hz' : r (f x) (f z) ∧ r (f y) (f z)
⊢ ∃ z ∈ s, (r on f) x z ∧ (r on f) y z

Tactic:
grind
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
inst : SemilatticeSup α
S : Set α
H : ∀ ⦃i j : α⦄, i ∈ S → j ∈ S → i ⊔ j ∈ S
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) S

Tactic:
fun a ha b hb =>
  ⟨a ⊔ b, H ha hb, le_sup_left, le_sup_right⟩

Premises used: le_sup_left, DirectedOn, le_sup_right, Max.max, And.intro, Exists.intro
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst : Preorder α
inst_1 : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
he : Injective e
a b : β
inl :
  ∀ (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)
inr :
  ∀ (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)
⊢ ∃ (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⟩)

Premises used: Exists, em, Or.symm, Eq, rfl
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst : Preorder α
inst_1 : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
he : Injective e
a b : β
ha : ¬∃ (i : ι), e i = a
h :
  (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)
⊢ ∃ (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
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst : Preorder α
inst_1 : 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]

Premises used: Function.extend_apply'
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst : Preorder α
inst_1 : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
he : Injective e
b : β
i : ι
inr :
  ∀ (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)
inr₁ :
  ∀ (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)
⊢ ∃ (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⟩)

Premises used: Exists, em, Or.symm, Eq, rfl
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst : Preorder α
inst_1 : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
he : Injective e
b : β
i : ι
hb : ¬∃ (i : ι), e i = b
h :
  (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))
⊢ ∃ (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
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst : Preorder α
inst_1 : 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]

Premises used: Function.extend_apply'
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst : Preorder α
inst_1 : OrderBot α
e : ι → β
f : ι → α
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
he : Injective e
i j : ι
inr :
  ∀ (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)
⊢ ∃ (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⟩
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst : Preorder α
inst_1 : 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
h :
  (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))
⊢ ∃ (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
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
inst : Preorder α
inst_1 : 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]

Premises used: Function.Injective.extend_apply, true_and
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
inst : SemilatticeInf α
S : Set α
H : ∀ ⦃i j : α⦄, i ∈ S → j ∈ S → i ⊓ j ∈ S
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≥ x2) S

Tactic:
directedOn_of_sup_mem (α := αᵒᵈ) H

Premises used: directedOn_of_sup_mem, OrderDual
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
ι : Sort u_3
r : α → α → Prop
inst : Total r
f : ι → α
⊢ Directed r f

Tactic:
fun i j =>
  Or.casesOn (total_of r (f i) (f j)) (fun h => ⟨j, h, refl _⟩) fun h => ⟨i, refl _, h⟩

Premises used: Directed, total_of, Or.casesOn
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
inst : Total r
s : Set α
⊢ DirectedOn r s

Tactic:
fun a ha b hb =>
  Or.casesOn (total_of r a b) (fun h => ⟨b, hb, h, refl _⟩) fun h => ⟨a, ha, refl _, h⟩

Premises used: DirectedOn, total_of, Or.casesOn
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
Std.Total.directedOn s

Premises used: Std.Total.directedOn
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
inst : IsDirected α r
a b : α
⊢ ∃ (c : α), r a c ∧ r b c

Tactic:
IsDirected.directed _ _

Premises used: IsDirected.directed
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
inst : IsDirected α r
inst_1 : IsTrans α r
a b c : α
⊢ ∃ (d : α), r a d ∧ r b d ∧ r c d

Tactic:
have ⟨e, hae, hbe⟩ := directed_of r a b
  have ⟨f, hef, hcf⟩ := directed_of r e c
  ⟨f, Trans.trans hae hef, Trans.trans hbe hef, hcf⟩

Premises used: Trans.trans, Exists, _private.0.directed_of₃.match_1, And, And.intro, Exists.intro, directed_of, _private.0.directed_of₃.match_2
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
ι : Sort u_3
r : α → α → Prop
f : ι → α
⊢ IsDirected ι (r on f) ↔ Directed r f

Tactic:
⟨(·.directed), (⟨·⟩)⟩

Premises used: IsDirected.mk, Iff.intro, IsDirected.directed
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
inst : IsDirected α r
⊢ Directed r id

Tactic:
directed_of r

Premises used: Directed, directed_of
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
⊢ Directed r id ↔ IsDirected α r

Tactic:
isDirected_onFun.symm

Premises used: isDirected_onFun, Iff.symm
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
inst : IsDirected α r
⊢ DirectedOn r Set.univ

Tactic:
fun a _ b _ =>
  let ⟨c, hc⟩ := directed_of r a b
  ⟨c, trivial, hc⟩

Premises used: _private.0.directedOn_univ.match_1, trivial, Set.univ, DirectedOn, Membership.mem, Exists, And, And.intro, Exists.intro, directed_of
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
⊢ DirectedOn r Set.univ ↔ IsDirected α r

Tactic:
⟨fun h =>
    ⟨fun a b =>
      let ⟨c, _, hc⟩ := h a trivial b trivial
      ⟨c, hc⟩⟩,
    @directedOn_univ _ _⟩

Premises used: trivial, _private.0.directedOn_univ_iff.match_1, Exists, IsDirected.mk, And, Iff.intro, Exists.intro, directedOn_univ
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
κ : Sort u_4
r r' s : α → α → Prop
inst : Total r
⊢ IsDirected α r

Tactic:
directed_id_iff.1 <| Std.Total.directed _

Premises used: Std.Total.directed, directed_id_iff, Iff.mp
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r s : α → α → Prop
inst : IsDirected α r
h : ∀ ⦃a b : α⦄, r a b → s a b
⊢ IsDirected α s

Tactic:
⟨fun a b =>
    let ⟨c, ha, hb⟩ := IsDirected.directed a b
    ⟨c, h ha, h hb⟩⟩

Premises used: Exists, IsDirected.mk, And, And.intro, Exists.intro, _private.0.directed_of₃.match_2, IsDirected.directed
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
inst : LE α
inst_1 : IsDirectedOrder α
a b : α
⊢ ∃ (c : α), a ≤ c ∧ b ≤ c

Tactic:
directed_of (· ≤ ·) a b

Premises used: LE.le, directed_of
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_3
κ : Sort u_4
r r' s : α → α → Prop
inst : LE α
inst_1 : IsDirectedOrder α
⊢ IsCodirectedOrder.{u_1} αᵒᵈ

Tactic:
assumption
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : IsDirectedOrder α
f : α → β
r : β → β → Prop
H : ∀ ⦃i j : α⦄, i ≤ j → r (f i) (f j)
⊢ Directed r f

Tactic:
directed_id.mono_comp _ H

Premises used: Directed.mono_comp, directed_id
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Preorder β
f : α → β
⊢ Monotone f → Directed (fun (x1 x2 : β) ↦ x1 ≤ x2) f

Tactic:
directed_of_isDirected_le

Premises used: Monotone, directed_of_isDirected_le
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : IsCodirectedOrder α
inst_2 : Preorder β
f : α → β
hf : Antitone f
⊢ Directed (fun (x1 x2 : β) ↦ x1 ≤ x2) f

Tactic:
directed_of_isDirected_ge hf

Premises used: directed_of_isDirected_ge
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
inst : LE α
s : Set α
rw :
  Directed (ι := { x : α // x ∈ s }) (fun (x1 x2 : α) ↦ x1 ≤ x2) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) ↔
    IsDirected.{u_1 + 1} (↑s : Type u_1) fun (x1 x2 : (↑s : Type u_1)) ↦ x1 ≤ x2
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s ↔ IsDirectedOrder.{u_1} (↑s : Type u_1)

Tactic:
rw [directedOn_iff_directed, IsDirectedOrder]

Premises used: directedOn_iff_directed, IsDirectedOrder
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
inst : LE α
s : Set α
⊢ Directed (ι := { x : α // x ∈ s }) (fun (x1 x2 : α) ↦ x1 ≤ x2) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) ↔
    IsDirected.{u_1 + 1} (↑s : Type u_1) fun (x1 x2 : (↑s : Type u_1)) ↦ x1 ≤ x2

Tactic:
⟨fun h ↦ ⟨h⟩, fun ⟨h⟩ ↦ h⟩

Premises used: Directed, LE.le, IsDirected.mk, _private.0.directedOn_iff_isDirectedOrder.match_1, Iff.intro, Subtype.val
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
inst : LE α
s : Set α
⊢ Directed (ι := { x : α // x ∈ s }) (fun (x1 x2 : α) ↦ x1 ≤ x2) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) ↔
    IsDirected.{u_1 + 1} (↑s : Type u_1) fun (x1 x2 : (↑s : Type u_1)) ↦ x1 ≤ x2

Tactic:
exact ⟨fun h ↦ ⟨h⟩, fun ⟨h⟩ ↦ h⟩
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl 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:
⟨y, Set.mem_insert _ _, refl _, refl _⟩

Premises used: And.intro, Exists.intro, Set.mem_insert, refl
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl 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 _ _, refl _, refl _⟩
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl r
s : Set α
hd : DirectedOn r s
x : α
ha : ∀ b ∈ s, ∃ c ∈ s, r x c ∧ r b c
y : α
hy : y ∈ s
inl : ∀ (w : α) (hws : w ∈ s) (hwr : r x w ∧ r y w), ∃ z ∈ insert x s, r x z ∧ r y z
⊢ ∃ z ∈ insert x s, r x z ∧ r y z

Tactic:
obtain ⟨w, hws, hwr⟩ := ha y hy
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl 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:
⟨w, Set.mem_insert_of_mem _ hws, hwr⟩

Premises used: Set.mem_insert_of_mem, And.intro, Exists.intro
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl 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⟩
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl r
s : Set α
hd : DirectedOn r s
x : α
hx : x ∈ s
y : α
ha : ∀ b ∈ s, ∃ c ∈ s, r y c ∧ r b c
inr : ∀ (w : α) (hws : w ∈ s) (hwr : r y w ∧ r x w), ∃ z ∈ insert y s, r x z ∧ r y z
⊢ ∃ z ∈ insert y s, r x z ∧ r y z

Tactic:
obtain ⟨w, hws, hwr⟩ := ha x hx
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl 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:
⟨w, Set.mem_insert_of_mem _ hws, hwr.symm⟩

Premises used: Set.mem_insert_of_mem, And.intro, Exists.intro, And.symm
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl 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⟩
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl 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
inr : ∀ (w : α) (hws : w ∈ s) (hwr : r x w ∧ r y w), ∃ z ∈ insert a s, r x z ∧ r y z
⊢ ∃ z ∈ insert a s, r x z ∧ r y z

Tactic:
obtain ⟨w, hws, hwr⟩ := hd x hx y hy
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl 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:
⟨w, Set.mem_insert_of_mem _ hws, hwr⟩

Premises used: Set.mem_insert_of_mem, And.intro, Exists.intro
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl 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⟩
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl r
a : α
⊢ DirectedOn r {a}

Tactic:
fun x hx _ hy => ⟨x, hx, refl _, hx.symm ▸ hy.symm ▸ refl _⟩

Premises used: DirectedOn, Eq.rec, And.intro, Exists.intro, Eq.symm, refl
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl r
a b : α
hab : r a b
⊢ DirectedOn r {a, b}

Tactic:
(directedOn_singleton _).insert _ fun c hc => ⟨c, hc, hc.symm ▸ hab, refl _⟩

Premises used: Eq.rec, And.intro, Exists.intro, DirectedOn.insert, directedOn_singleton, Eq.symm, refl
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl r
a b : α
hab : r a b
rw : DirectedOn r {a, b}
⊢ DirectedOn r {b, a}

Tactic:
rw [Set.pair_comm]

Premises used: Set.pair_comm
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
r : α → α → Prop
inst : Std.Refl r
a b : α
hab : r a b
⊢ DirectedOn r {a, b}

Tactic:
apply directedOn_pair hab

Premises used: directedOn_pair
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
inst : Preorder α
a : α
inst_1 : IsDirectedOrder α
h : IsMax a
⊢ IsTop a

Tactic:
fun b ↦
  let ⟨_, hca, hcb⟩ := exists_ge_ge a b
  hcb.trans (h hca)

Premises used: LE.le, _private.0.IsMax.isTop.match_1, exists_ge_ge, LE.le.trans, IsTop
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
m : α
hm : m ∈ s
hmax : ∀ a ∈ s, m ≤ a → a ≤ m
⊢ ∀ a ∈ s, a ≤ m

Tactic:
fun a as ↦
  let ⟨x, xs, xm, xa⟩ := hd m hm a as
  xa.trans (hmax x xs xm)

Premises used: LE.le, _private.0.DirectedOn.is_top_of_is_max.match_1, LE.le.trans
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
inst : Preorder α
inst_1 : IsDirectedOrder α
a : α
⊢ IsTop a ∨ ∃ (b : α), a < b

Tactic:
(em (IsMax a)).imp IsMax.isTop not_isMax_iff.mp

Premises used: IsMax.isTop, em, Iff.mp, not_isMax_iff, Or.imp, IsMax
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
inst : Preorder α
a : α
inst_1 : IsDirectedOrder α
⊢ IsTop a ↔ IsMax a

Tactic:
⟨IsTop.isMax, IsMax.isTop⟩

Premises used: IsMax.isTop, IsTop.isMax, Iff.intro
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Preorder β
f g : α → β
hf : Monotone f
hg : Antitone g
h : f ≤ g
m n : α
obtain : ∀ (k : α) (hkm : m ≤ k) (hkn : n ≤ k), f m ≤ g n
⊢ f m ≤ g n

Tactic:
obtain ⟨k, hkm, hkn⟩ := exists_ge_ge m n

Premises used: exists_ge_ge
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Preorder β
f g : α → β
hf : Monotone f
hg : Antitone g
h : f ≤ g
m n k : α
hkm : m ≤ k
hkn : n ≤ k
⊢ f m ≤ f k

Tactic:
hf hkm
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Preorder β
f g : α → β
hf : Monotone f
hg : Antitone g
h : f ≤ g
m n k : α
hkm : m ≤ k
hkn : n ≤ k
⊢ f k ≤ g k

Tactic:
h _
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Preorder β
f g : α → β
hf : Monotone f
hg : Antitone g
h : f ≤ g
m n k : α
hkm : m ≤ k
hkn : n ≤ k
⊢ g k ≤ g n

Tactic:
hg hkn
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : IsDirectedOrder α
inst_2 : Preorder β
f g : α → β
hf : Monotone f
hg : Antitone g
h : f ≤ g
m n k : α
hkm : m ≤ k
hkn : n ≤ k
⊢ f m ≤ g n

Tactic:
calc
    f m ≤ f k := hf hkm
    _ ≤ g k := h _
    _ ≤ g n := hg hkn
-- Module: Mathlib.Order.Directed
Goal:
β : Type u_2
inst : PartialOrder β
inst_1 : Nontrivial β
inst_2 : IsCodirectedOrder β
rcases : ∀ (a b : β) (hne : a ≠ b), ∃ (a : β) (b : β), a < b
⊢ ∃ (a : β) (b : β), a < b

Tactic:
rcases exists_pair_ne β with ⟨a, b, hne⟩

Premises used: exists_pair_ne
-- Module: Mathlib.Order.Directed
Goal:
β : Type u_2
inst : PartialOrder β
inst_1 : Nontrivial β
inst_2 : IsCodirectedOrder β
a b : β
hne : a ≠ b
inl : ∀ (ha : IsBot a), ∃ (a : β) (b : β), a < b
inr : ∀ (c : β) (hc : c < a), ∃ (a : β) (b : β), a < b
⊢ ∃ (a : β) (b : β), a < b

Tactic:
rcases isBot_or_exists_lt a with (ha | ⟨c, hc⟩)

Premises used: isBot_or_exists_lt
-- Module: Mathlib.Order.Directed
Goal:
β : Type u_2
inst : PartialOrder β
inst_1 : Nontrivial β
inst_2 : IsCodirectedOrder β
a b : β
hne : a ≠ b
ha : IsBot a
⊢ ∃ (a : β) (b : β), a < b

Tactic:
⟨a, b, (ha b).lt_of_ne hne⟩

Premises used: LE.le.lt_of_ne, Exists.intro
-- Module: Mathlib.Order.Directed
Goal:
β : Type u_2
inst : PartialOrder β
inst_1 : Nontrivial β
inst_2 : IsCodirectedOrder β
a b : β
hne : a ≠ b
c : β
hc : c < a
⊢ ∃ (a : β) (b : β), a < b

Tactic:
⟨_, _, hc⟩

Premises used: Exists.intro
-- Module: Mathlib.Order.Directed
Goal:
β : Type u_2
inst : PartialOrder β
inst_1 : Nontrivial β
inst_2 : IsCodirectedOrder β
a b : β
hne : a ≠ b
ha : IsBot a
⊢ ∃ (a : β) (b : β), a < b

Tactic:
exacts [⟨a, b, (ha b).lt_of_ne hne⟩, ⟨_, _, hc⟩]
-- Module: Mathlib.Order.Directed
Goal:
β : Type u_2
inst : PartialOrder β
inst_1 : Nontrivial β
inst_2 : IsDirectedOrder β
b : β
hb : IsMax b
hb' : IsMin b
obtain : ∀ (a c : β) (hac : c < a), False
⊢ False

Tactic:
obtain ⟨a, c, hac⟩ := exists_lt_of_directed_le β

Premises used: exists_lt_of_directed_le
-- Module: Mathlib.Order.Directed
Goal:
β : Type u_2
inst : PartialOrder β
inst_1 : Nontrivial β
inst_2 : IsDirectedOrder β
b : β
hb : IsMax b
hb' : IsMin b
a c : β
hac : c < a
⊢ a ≤ b

Tactic:
have := hb.isTop a
-- Module: Mathlib.Order.Directed
Goal:
β : Type u_2
inst : PartialOrder β
inst_1 : Nontrivial β
inst_2 : IsDirectedOrder β
b : β
hb : IsMax b
hb' : IsMin b
a c : β
hac : c < a
this : a ≤ b
⊢ c < b

Tactic:
obtain rfl := (hb' <| this).antisymm this

Premises used: LE.le.antisymm, rfl
-- Module: Mathlib.Order.Directed
Goal:
β : Type u_2
inst : PartialOrder β
inst_1 : Nontrivial β
inst_2 : IsDirectedOrder β
b : β
hb : IsMax b
hb' : IsMin b
a c : β
hac : c < a
this : a ≤ b
hac₁ : c < b
⊢ b ≤ b

Tactic:
obtain rfl := (hb' <| this).antisymm this

Premises used: LE.le.antisymm, rfl
-- Module: Mathlib.Order.Directed
Goal:
β : Type u_2
inst : PartialOrder β
inst_1 : Nontrivial β
inst_2 : IsDirectedOrder β
b : β
hb : IsMax b
hb' : IsMin b
c : β
hac : c < b
this : b ≤ b
⊢ False

Tactic:
hb'.not_lt hac

Premises used: IsMin.not_lt
-- Module: Mathlib.Order.Directed
Goal:
β : Type u_2
inst : PartialOrder β
inst_1 : Nontrivial β
inst_2 : IsDirectedOrder β
b : β
hb : IsMax b
hb' : IsMin b
c : β
hac : c < b
this : b ≤ b
⊢ False

Tactic:
exact hb'.not_lt hac

Premises used: IsMin.not_lt
-- Module: Mathlib.Order.Directed
Goal:
β : Type u_2
inst : PartialOrder β
inst_1 : Nontrivial β
inst_2 : IsDirectedOrder β
b : β
hb : IsMin b
⊢ ¬IsMax b

Tactic:
fun hb' ↦ hb'.toDual.not_isMax hb.toDual

Premises used: IsMin.not_isMax, IsMax.toDual, IsMin.toDual, Not
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
inst_1 : Preorder α
f : α → β
inst_2 : IsDirectedOrder α
hf : Monotone f
hf' : Antitone f
a b : α
⊢ ∀ (m n : α), f m ≤ f n

Tactic:
have := hf.forall_le_of_antitone hf' le_rfl
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
inst_1 : Preorder α
f : α → β
inst_2 : IsDirectedOrder α
hf : Monotone f
hf' : Antitone f
a b : α
this : ∀ (m n : α), f m ≤ f n
⊢ f a = f b

Tactic:
le_antisymm (this a b) (this b a)

Premises used: le_antisymm
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
inst_1 : Preorder α
f : α → β
inst_2 : IsDirectedOrder α
hf : Monotone f
hf' : Antitone f
a b : α
this : ∀ (m n : α), f m ≤ f n
⊢ f a = f b

Tactic:
exact le_antisymm (this a b) (this b a)

Premises used: le_antisymm
-- Module: Mathlib.Order.Directed
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder β
inst_1 : Preorder α
f : α → β
s : Set α
hf : MonotoneOn f s
hf' : AntitoneOn f s
hs : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
obtain : ∀ (c : α) (hc : c ∈ s) (hac : a ≤ c) (hbc : b ≤ c), f a = f b
⊢ f a = f b

Tactic:
obtain ⟨c, hc, hac, hbc⟩ := hs _ ha _ hb