awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
hs : IsCofinal s
hf : Monotone f
hf' : IsCofinal (range f)
a : β
b : α
hb : a ≤ f b
obtain : ∀ (c : α) (hc : c ∈ s) (hc' : b ≤ c), ∃ y ∈ f '' s, a ≤ y
⊢ ∃ y ∈ f '' s, a ≤ y

Tactic:
obtain ⟨c, hc, hc'⟩ := hs b
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
hs : IsCofinal s
hf : Monotone f
hf' : IsCofinal (range f)
a : β
b : α
hb : a ≤ f b
c : α
hc : c ∈ s
hc' : b ≤ c
⊢ ∃ y ∈ f '' s, a ≤ y

Tactic:
⟨_, mem_image_of_mem f hc, hb.trans (hf hc')⟩

Premises used: Set.mem_image_of_mem, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
hs : IsCofinal s
hf : Monotone f
hf' : IsCofinal (range f)
a : β
b : α
hb : a ≤ f b
c : α
hc : c ∈ s
hc' : b ≤ c
⊢ ∃ y ∈ f '' s, a ≤ y

Tactic:
exact ⟨_, mem_image_of_mem f hc, hb.trans (hf hc')⟩
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : Preorder α
s : Set α
t : Set (↑s : Type u_1)
hs : IsCofinal s
ht : IsCofinal t
⊢ IsCofinal.{u_1} (α := α) (range (ι := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))

Tactic:
simpa
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : β → α
g : α → β
h : GaloisConnection f g
⊢ IsCofinal (range g)

Tactic:
fun a ↦ ⟨_, mem_range_self _, le_u_l h a⟩

Premises used: Set.mem_range_self, GaloisConnection.le_u_l, And.intro, Exists.intro, IsCofinal
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : β → α
g : α → β
h : GaloisConnection f g
s : Set α
hs : IsCofinal s
⊢ IsCofinal (g '' s)

Tactic:
hs.image h.monotone_u h.isCofinal_range

Premises used: GaloisConnection.monotone_u, GaloisConnection.isCofinal_range, IsCofinal.image
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
s : Set α
hs : IsCofinal s
⊢ IsCofinal.{u_2} (α := β) ((⇑e : (a : α) → β) '' s)

Tactic:
e.symm.to_galoisConnection.map_isCofinal hs

Premises used: GaloisConnection.map_isCofinal, OrderIso.to_galoisConnection, OrderIso.symm
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
s : Set α
hs : IsCofinal.{u_2} (α := β) ((⇑e : (a : α) → β) '' s)
⊢ IsCofinal s

Tactic:
simpa using e.symm.map_isCofinal hs

Premises used: OrderIso.map_isCofinal, OrderIso.symm
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ IsCofinal s ↔ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ s, Iic i) univ

Tactic:
simp [IsCofinal, eq_univ_iff_forall]

Premises used: Set.eq_univ_iff_forall, IsCofinal
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
s : Set α
hs : IsCofinal s
simp_rw : ∀ (x : α), ∃ i ∈ s, x ∈ Iio i
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ s, Iio i) univ

Tactic:
simp_rw [eq_univ_iff_forall, mem_iUnion, exists_prop]

Premises used: Set.eq_univ_iff_forall, Set.mem_iUnion, exists_prop
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
s : Set α
hs : IsCofinal s
x : α
obtain : ∀ (y : α) (hy : x < y), ∃ i ∈ s, x ∈ Iio i
⊢ ∃ i ∈ s, x ∈ Iio i

Tactic:
obtain ⟨y, hy⟩ := exists_gt x

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
s : Set α
hs : IsCofinal s
x y : α
hy : x < y
obtain : ∀ (z : α) (hz : z ∈ s) (hz' : y ≤ z), ∃ i ∈ s, x ∈ Iio i
⊢ ∃ i ∈ s, x ∈ Iio i

Tactic:
obtain ⟨z, hz, hz'⟩ := hs y
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
s : Set α
hs : IsCofinal s
x y : α
hy : x < y
z : α
hz : z ∈ s
hz' : y ≤ z
⊢ ∃ i ∈ s, x ∈ Iio i

Tactic:
⟨z, hz, hy.trans_le hz'⟩

Premises used: LT.lt.trans_le, And.intro, Exists.intro
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
s : Set α
hs : IsCofinal s
x y : α
hy : x < y
z : α
hz : z ∈ s
hz' : y ≤ z
⊢ ∃ i ∈ s, x ∈ Iio i

Tactic:
exact ⟨z, hz, hy.trans_le hz'⟩
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
s : Set α
hs : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ s, Iio i) univ
rw : Subset.{u_1} (α := Set α) (⋃ i ∈ s, Iio i) (⋃ i ∈ s, Iic i)
⊢ IsCofinal s

Tactic:
rw [isCofinal_iff_iUnion_Iic_eq_univ, ← univ_subset_iff, ← hs]

Premises used: Set.univ_subset_iff, isCofinal_iff_iUnion_Iic_eq_univ
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
s : Set α
hs : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ s, Iio i) univ
h : ∀ i ∈ s, Iio i ⊆ Iic i
⊢ Subset.{u_1} (α := Set α) (⋃ i ∈ s, Iio i) (⋃ i ∈ s, Iic i)

Tactic:
gcongr
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
s : Set α
hs : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ s, Iio i) univ
i : α
i_1 : i ∈ s
⊢ Iio i ⊆ Iic i

Tactic:
Iio_subset_Iic_self

Premises used: Set.Iio_subset_Iic_self
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
s : Set α
hs : Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ s, Iio i) univ
i : α
i_1 : i ∈ s
⊢ Iio i ⊆ Iic i

Tactic:
exact Iio_subset_Iic_self

Premises used: Set.Iio_subset_Iic_self
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
a : α
ha : IsMax a
hs : IsCofinal s
obtain : ∀ (b : α) (hb : b ∈ s) (hb' : a ≤ b), a ∈ s
⊢ a ∈ s

Tactic:
obtain ⟨b, hb, hb'⟩ := hs a
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : PartialOrder α
s : Set α
a : α
ha : IsMax a
hs : IsCofinal s
b : α
hb : b ∈ s
hb' : a ≤ b
rwa rwa₁ rwa₂ rwa₃ : ∀ (hb : a ∈ s) (hb' : a ≤ b), a ∈ s
⊢ a ∈ s

Tactic:
rwa [ha.eq_of_ge hb'] at hb

Premises used: IsMax.eq_of_ge
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
s : Set α
hs : IsCofinal s
⊢ ⊤ ∈ s

Tactic:
hs.mem_of_isMax isMax_top

Premises used: isMax_top, IsCofinal.mem_of_isMax
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
s : Set α
⊢ IsCofinal s ↔ ⊤ ∈ s

Tactic:
⟨IsCofinal.top_mem, fun hs _ ↦ ⟨⊤, hs, le_top⟩⟩

Premises used: IsCofinal.top_mem, le_top, And.intro, Iff.intro, Exists.intro, Top.top
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
⊢ ¬IsCofinal s ↔ ∃ (x : α), ∀ y ∈ s, y < x

Tactic:
simp [IsCofinal]

Premises used: IsCofinal
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
h : ¬IsCofinal s
⊢ ∃ (x : α), ∀ y ∈ s, y < x

Tactic:
rw [not_isCofinal_iff] at h

Premises used: not_isCofinal_iff
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
h : ∃ (x : α), ∀ y ∈ s, y < x
obtain : ∀ (x : α) (h : ∀ y ∈ s, y < x), BddAbove s
⊢ BddAbove s

Tactic:
obtain ⟨x, h⟩ := h
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : α
h : ∀ y ∈ s, y < x
⊢ BddAbove s

Tactic:
⟨x, fun y hy ↦ (h y hy).le⟩

Premises used: LT.lt.le, BddAbove, Set.Nonempty, Exists.intro
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
x : α
h : ∀ y ∈ s, y < x
⊢ BddAbove s

Tactic:
exact ⟨x, fun y hy ↦ (h y hy).le⟩
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
h : ¬BddAbove s
contrapose : ∀ (h : ¬IsCofinal s), BddAbove s
⊢ IsCofinal s

Tactic:
contrapose h
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
h : ¬IsCofinal s
⊢ BddAbove s

Tactic:
.of_not_isCofinal h

Premises used: BddAbove.of_not_isCofinal
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
h : ¬IsCofinal s
⊢ BddAbove s

Tactic:
exact .of_not_isCofinal h
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : NoMaxOrder α
s : Set α
mpr : BddAbove s → ¬IsCofinal s
⊢ ¬IsCofinal s ↔ BddAbove s

Tactic:
use .of_not_isCofinal
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : NoMaxOrder α
s : Set α
mpr : BddAbove s → ∃ (x : α), ∀ y ∈ s, y < x
⊢ BddAbove s → ¬IsCofinal s

Tactic:
rw [not_isCofinal_iff]

Premises used: not_isCofinal_iff
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : NoMaxOrder α
s : Set α
x : α
h : x ∈ upperBounds s
mpr : ∀ (z : α) (hz : x < z), ∃ (x : α), ∀ y ∈ s, y < x
⊢ ∃ (x : α), ∀ y ∈ s, y < x

Tactic:
obtain ⟨z, hz⟩ := exists_gt x

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : NoMaxOrder α
s : Set α
x : α
h : x ∈ upperBounds s
z : α
hz : x < z
⊢ ∃ (x : α), ∀ y ∈ s, y < x

Tactic:
⟨z, fun y hy ↦ (h hy).trans_lt hz⟩

Premises used: Exists.intro, LE.le.trans_lt
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : NoMaxOrder α
s : Set α
x : α
h : x ∈ upperBounds s
z : α
hz : x < z
⊢ ∃ (x : α), ∀ y ∈ s, y < x

Tactic:
exact ⟨z, fun y hy ↦ (h hy).trans_lt hz⟩
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : NoMaxOrder α
s : Set α
⊢ ¬BddAbove s ↔ IsCofinal s

Tactic:
not_iff_comm.1 not_isCofinal_iff_bddAbove

Premises used: not_isCofinal_iff_bddAbove, Iff.mp, not_iff_comm
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a : α
obtain :
  ∀ (b : α) (hb : b ∈ Ici a) (hb' : ∀ x ∈ Ici a, ¬r x b),
    ∃ (y : α), Membership.mem (γ := Set α) {a : α | ∀ (b : α), r b a → b < a} y ∧ a ≤ y
⊢ ∃ (y : α), Membership.mem (γ := Set α) {a : α | ∀ (b : α), r b a → b < a} y ∧ a ≤ y

Tactic:
obtain ⟨b, hb, hb'⟩ := h.wf.has_min (Set.Ici a) Set.nonempty_Ici

Premises used: Set.Ici, IsWellFounded.wf, WellFounded.has_min, Set.nonempty_Ici
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a b : α
hb : b ∈ Ici a
hb' : ∀ x ∈ Ici a, ¬r x b
⊢ ∃ (y : α), Membership.mem (γ := Set α) {a : α | ∀ (b : α), r b a → b < a} y ∧ a ≤ y

Tactic:
⟨b, fun c hc ↦ ?_, hb⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a b : α
hb : b ∈ Ici a
hb' : ∀ x ∈ Ici a, ¬r x b
refine : ∀ (c : α) (hc : r c b), c < b
⊢ ∃ (y : α), Membership.mem (γ := Set α) {a : α | ∀ (b : α), r b a → b < a} y ∧ a ≤ y

Tactic:
refine ⟨b, fun c hc ↦ ?_, hb⟩
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a b : α
hb : b ∈ Ici a
hb' : ∀ x ∈ Ici a, ¬r x b
c : α
hc : r c b
by_contra! : ∀ (hc' : b ≤ c), False
⊢ c < b

Tactic:
by_contra! hc'
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a b : α
hb : b ∈ Ici a
hb' : ∀ x ∈ Ici a, ¬r x b
c : α
hc : r c b
hc' : b ≤ c
⊢ False

Tactic:
hb' c (hb.trans hc') hc

Premises used: LE.le.trans
-- Module: Mathlib.Order.Cofinal
Goal:
α : Type u_1
inst : LinearOrder α
r : α → α → Prop
h : IsWellFounded α r
a b : α
hb : b ∈ Ici a
hb' : ∀ x ∈ Ici a, ¬r x b
c : α
hc : r c b
hc' : b ≤ c
⊢ False

Tactic:
exact hb' c (hb.trans hc') hc

Premises used: LE.le.trans
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
mp :
  IsCompactElement k →
    ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
mpr :
  (∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x) →
    IsCompactElement k
⊢ IsCompactElement k ↔
    ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x

Tactic:
constructor
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : IsCompactElement k
s : Set α
hs : s.Nonempty
hs' : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
h_le : k ≤ sSup s
⊢ ∃ x ∈ s, k ≤ x

Tactic:
hk s (sSup s) hs hs' (isLUB_sSup s) h_le

Premises used: CompleteLattice.isLUB_sSup, SupSet.sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : IsCompactElement k
s : Set α
hs : s.Nonempty
hs' : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
h_le : k ≤ sSup s
⊢ ∃ x ∈ s, k ≤ x

Tactic:
exact hk s (sSup s) hs hs' (isLUB_sSup s) h_le

Premises used: CompleteLattice.isLUB_sSup, SupSet.sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
u : α
hs : s.Nonempty
hs' : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hu : IsLUB s u
h_le : k ≤ u
⊢ sSup s = u

Tactic:
rw [isLUB_iff_sSup_eq] at hu

Premises used: isLUB_iff_sSup_eq
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
u : α
hs : s.Nonempty
hs' : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hu : IsLUB s u
h_le : k ≤ u
hu₁ : sSup s = u
⊢ k ≤ u

Tactic:
rw [isLUB_iff_sSup_eq] at hu

Premises used: isLUB_iff_sSup_eq
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
u : α
hs : s.Nonempty
hs' : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hu : sSup s = u
h_le : k ≤ u
⊢ k ≤ sSup s

Tactic:
rw [← hu] at h_le
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
u : α
hs : s.Nonempty
hs' : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hu : sSup s = u
h_le : k ≤ sSup s
⊢ ∃ x ∈ s, k ≤ x

Tactic:
h s hs hs' h_le
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
u : α
hs : s.Nonempty
hs' : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hu : sSup s = u
h_le : k ≤ sSup s
⊢ ∃ x ∈ s, k ≤ x

Tactic:
exact h s hs hs' h_le
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
rw :
  (∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x) ↔
    ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
⊢ IsCompactElement k ↔ ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id

Tactic:
rw [isCompactElement_iff_le_of_directed_sSup_le]

Premises used: CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
mp :
  (∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x) →
    ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
mpr :
  (∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id) →
    ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
⊢ (∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x) ↔
    ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id

Tactic:
constructor
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ x = t.sup id}
x : α
c : Finset α
hc : (↑c : Set α) ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : (↑d : Set α) ⊆ s ∧ y = d.sup id
h : x ⊔ y ∈ S ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) x (x ⊔ y) ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y (x ⊔ y)
⊢ ∃ z ∈ S, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z

Tactic:
use x ⊔ y
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ x = t.sup id}
x : α
c : Finset α
hc : (↑c : Set α) ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : (↑d : Set α) ⊆ s ∧ y = d.sup id
h : x ⊔ y ∈ S
h₁ : (fun (x1 x2 : α) ↦ x1 ≤ x2) x (x ⊔ y) ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y (x ⊔ y)
⊢ x ⊔ y ∈ S ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) x (x ⊔ y) ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y (x ⊔ y)

Tactic:
constructor
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ x = t.sup id}
x : α
c : Finset α
hc : (↑c : Set α) ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : (↑d : Set α) ⊆ s ∧ y = d.sup id
h : (↑(c ∪ d) : Set α) ⊆ s ∧ x ⊔ y = (c ∪ d).sup id
⊢ x ⊔ y ∈ S

Tactic:
use c ∪ d
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ x = t.sup id}
x : α
c : Finset α
hc : (↑c : Set α) ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : (↑d : Set α) ⊆ s ∧ y = d.sup id
h : (↑(c ∪ d) : Set α) ⊆ s
h₁ : x ⊔ y = (c ∪ d).sup id
⊢ (↑(c ∪ d) : Set α) ⊆ s ∧ x ⊔ y = (c ∪ d).sup id

Tactic:
constructor
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ x = t.sup id}
x : α
c : Finset α
hc : (↑c : Set α) ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : (↑d : Set α) ⊆ s ∧ y = d.sup id
⊢ (↑(c ∪ d) : Set α) ⊆ s

Tactic:
simp only [hc.left, hd.left, Set.union_subset_iff, Finset.coe_union, and_self_iff]

Premises used: Set.union_subset_iff, And.left, and_self_iff, Finset.coe_union
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ x = t.sup id}
x : α
c : Finset α
hc : (↑c : Set α) ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : (↑d : Set α) ⊆ s ∧ y = d.sup id
⊢ x ⊔ y = (c ∪ d).sup id

Tactic:
simp only [hc.right, hd.right, Finset.sup_union]

Premises used: Finset.sup_union, And.right
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ x = t.sup id}
x : α
c : Finset α
hc : (↑c : Set α) ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : (↑d : Set α) ⊆ s ∧ y = d.sup id
⊢ (fun (x1 x2 : α) ↦ x1 ≤ x2) x (x ⊔ y) ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y (x ⊔ y)

Tactic:
simp only [and_self_iff, le_sup_left, le_sup_right]

Premises used: le_sup_left, le_sup_right, and_self_iff
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ x = t.sup id}
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) S

Tactic:
have dir_US : DirectedOn (· ≤ ·) S := by
        rintro x ⟨c, hc⟩ y ⟨d, hd⟩
        use x ⊔ y
        constructor
        · use c ∪ d
          constructor
          · simp only [hc.left, hd.left, Set.union_subset_iff, Finset.coe_union, and_self_iff]
          · simp only [hc.right, hd.right, Finset.sup_union]
        simp only [and_self_iff, le_sup_left, le_sup_right]
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ x = t.sup id}
dir_US : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) S
h : s ⊆ S
⊢ sSup s ≤ sSup S

Tactic:
apply sSup_le_sSup

Premises used: sSup_le_sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ x = t.sup id}
dir_US : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) S
x : α
hx : x ∈ s
h : (↑{x} : Set α) ⊆ s ∧ x = Finset.sup {x} id
⊢ x ∈ S

Tactic:
use {x}
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ x = t.sup id}
dir_US : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) S
x : α
hx : x ∈ s
⊢ (↑{x} : Set α) ⊆ s ∧ x = Finset.sup {x} id

Tactic:
simpa only [and_true, id, Finset.coe_singleton, eq_self_iff_true,
          Finset.sup_singleton, Set.singleton_subset_iff]

Premises used: Set.singleton_subset_iff, Finset.coe_singleton, and_true, Finset.sup_singleton, id, eq_self_iff_true
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ x = t.sup id}
dir_US : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) S
⊢ sSup s ≤ sSup S

Tactic:
have sup_S : sSup s ≤ sSup S := by
        apply sSup_le_sSup
        intro x hx
        use {x}
        simpa only [and_true, id, Finset.coe_singleton, eq_self_iff_true,
          Finset.sup_singleton, Set.singleton_subset_iff]
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ x = t.sup id}
dir_US : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) S
sup_S : sSup s ≤ sSup S
suffices : ⊥ ∈ S
⊢ S.Nonempty

Tactic:
suffices ⊥ ∈ S from Set.nonempty_of_mem this
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ x = t.sup id}
dir_US : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) S
sup_S : sSup s ≤ sSup S
h : (↑∅ : Set α) ⊆ s ∧ Eq.{u_2 + 1} (α := α) ⊥ (Finset.sup ∅ id)
⊢ ⊥ ∈ S

Tactic:
use ∅
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ x = t.sup id}
dir_US : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) S
sup_S : sSup s ≤ sSup S
⊢ (↑∅ : Set α) ⊆ s ∧ Eq.{u_2 + 1} (α := α) ⊥ (Finset.sup ∅ id)

Tactic:
simp
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x : α | ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ x = t.sup id}
dir_US : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) S
sup_S : sSup s ≤ sSup S
⊢ S.Nonempty

Tactic:
have Sne : S.Nonempty := by
        suffices ⊥ ∈ S from Set.nonempty_of_mem this
        use ∅
        simp