awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
Sne : S.Nonempty
mp : ∀ (j : α) (hjS : j ∈ S) (hjk : k ≤ j), ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id

Tactic:
obtain ⟨j, ⟨hjS, hjk⟩⟩ := hk S Sne dir_US (le_trans hsup sup_S)

Premises used: le_trans
-- 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
Sne : S.Nonempty
j : α
hjS : j ∈ S
hjk : k ≤ j
mp : ∀ (t : Finset α) (htS : (↑t : Set α) ⊆ s) (htsup : j = t.sup id), ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id

Tactic:
obtain ⟨t, ⟨htS, htsup⟩⟩ := hjS
-- 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
Sne : S.Nonempty
j : α
hjk : k ≤ j
t : Finset α
htS : (↑t : Set α) ⊆ s
htsup : j = t.sup id
h : (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id

Tactic:
use t
-- 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
Sne : S.Nonempty
j : α
hjk : k ≤ j
t : Finset α
htS : (↑t : Set α) ⊆ s
htsup : j = t.sup id
rwa rwa₁ rwa₂ rwa₃ : k ≤ j
⊢ k ≤ t.sup id

Tactic:
rwa [← htsup]
-- 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
Sne : S.Nonempty
j : α
hjk : k ≤ j
t : Finset α
htS : (↑t : Set α) ⊆ s
htsup : j = t.sup id
⊢ (↑t : Set α) ⊆ s ∧ k ≤ t.sup id

Tactic:
exact ⟨htS, by rwa [← htsup]⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
s : Set α
hne : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hsup : k ≤ sSup s
mpr : ∀ (t : Finset α) (ht : (↑t : Set α) ⊆ s ∧ k ≤ t.sup id), ∃ x ∈ s, k ≤ x
⊢ ∃ x ∈ s, k ≤ x

Tactic:
obtain ⟨t, ht⟩ := hk s hsup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
s : Set α
hne : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hsup : k ≤ sSup s
t : Finset α
ht : (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
⊢ ∀ x ∈ t, ∃ y ∈ s, x ≤ y

Tactic:
have t_below_s : ∀ x ∈ t, ∃ y ∈ s, x ≤ y := fun x hxt => ⟨x, ht.left hxt, le_rfl⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
s : Set α
hne : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hsup : k ≤ sSup s
t : Finset α
ht : (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
t_below_s : ∀ x ∈ t, ∃ y ∈ s, x ≤ y
mpr : ∀ (x : α) (hxs : x ∈ s) (hsupx : t.sup id ≤ x), ∃ x ∈ s, k ≤ x
⊢ ∃ x ∈ s, k ≤ x

Tactic:
obtain ⟨x, ⟨hxs, hsupx⟩⟩ := Finset.sup_le_of_le_directed s hne hdir t t_below_s

Premises used: Finset.sup_le_of_le_directed
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
s : Set α
hne : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hsup : k ≤ sSup s
t : Finset α
ht : (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
t_below_s : ∀ x ∈ t, ∃ y ∈ s, x ≤ y
x : α
hxs : x ∈ s
hsupx : t.sup id ≤ x
⊢ ∃ x ∈ s, k ≤ x

Tactic:
⟨x, ⟨hxs, le_trans ht.right hsupx⟩⟩

Premises used: And.right, And.intro, Exists.intro, le_trans
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
s : Set α
hne : s.Nonempty
hdir : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hsup : k ≤ sSup s
t : Finset α
ht : (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
t_below_s : ∀ x ∈ t, ∃ y ∈ s, x ≤ y
x : α
hxs : x ∈ s
hsupx : t.sup id ≤ x
⊢ ∃ x ∈ s, k ≤ x

Tactic:
exact ⟨x, ⟨hxs, le_trans ht.right hsupx⟩⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
rw rw₁ 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
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 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
⊢ IsCompactElement k ↔ ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id

Tactic:
classical
    rw [isCompactElement_iff_le_of_directed_sSup_le]
    constructor
    · intro hk s hsup
      -- Consider the set of finite joins of elements of the (plain) set s.
      let S : Set α := { x | ∃ t : Finset α, ↑t ⊆ s ∧ x = t.sup id }
      -- S is directed, nonempty, and still has sup above k.
      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]
      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]
      have Sne : S.Nonempty := by
        suffices ⊥ ∈ S from Set.nonempty_of_mem this
        use ∅
        simp
      -- Now apply the defn of compact and finish.
      obtain ⟨j, ⟨hjS, hjk⟩⟩ := hk S Sne dir_US (le_trans hsup sup_S)
      obtain ⟨t, ⟨htS, htsup⟩⟩ := hjS
      use t
      exact ⟨htS, by rwa [← htsup]⟩
    · intro hk s hne hdir hsup
      obtain ⟨t, ht⟩ := hk s hsup
      -- certainly every element of t is below something in s, since ↑t ⊆ s.
      have t_below_s : ∀ x ∈ t, ∃ y ∈ s, x ≤ y := fun x hxt => ⟨x, ht.left hxt, le_rfl⟩
      obtain ⟨x, ⟨hxs, hsupx⟩⟩ := Finset.sup_le_of_le_directed s hne hdir t t_below_s
      exact ⟨x, ⟨hxs, le_trans ht.right hsupx⟩⟩

Premises used: CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u
inst : CompleteLattice α
k : α
rw :
  (∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id) ↔
    ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s
⊢ IsCompactElement k ↔ ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s

Tactic:
rw [isCompactElement_iff_exists_le_sSup_of_le_sSup]

Premises used: CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u
inst : CompleteLattice α
k : α
mp :
  (∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id) →
    ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s
mpr :
  (∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s) →
    ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
⊢ (∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id) ↔
    ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s

Tactic:
constructor
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u
inst : CompleteLattice α
k : α
H : ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
ι : Type u
s : ι → α
hs : k ≤ iSup s
mp : ∀ (t : Finset α) (ht : (↑t : Set α) ⊆ range s) (ht' : k ≤ t.sup id), ∃ (t : Finset ι), k ≤ t.sup s
⊢ ∃ (t : Finset ι), k ≤ t.sup s

Tactic:
obtain ⟨t, ht, ht'⟩ := H (Set.range s) hs

Premises used: Set.range
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u
inst : CompleteLattice α
k : α
H : ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : (↑t : Set α) ⊆ range s
ht' : k ≤ t.sup id
⊢ ∀ (x : ↥t), ∃ (i : ι), s i = (↑x : α)

Tactic:
have : ∀ x : t, ∃ i, s i = x := fun x => ht x.prop
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u
inst : CompleteLattice α
k : α
H : ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : (↑t : Set α) ⊆ range s
ht' : k ≤ t.sup id
this : ∀ (x : ↥t), ∃ (i : ι), s i = (↑x : α)
mp : ∀ (f : (x : ↥t) → ι) (hf : ∀ (x : ↥t), s (f x) = (↑x : α)), ∃ (t : Finset ι), k ≤ t.sup s
⊢ ∃ (t : Finset ι), k ≤ t.sup s

Tactic:
choose f hf using this
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u
inst : CompleteLattice α
k : α
H : ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : (↑t : Set α) ⊆ range s
ht' : k ≤ t.sup id
f : (x : ↥t) → ι
hf : ∀ (x : ↥t), s (f x) = (↑x : α)
⊢ ∃ (t : Finset ι), k ≤ t.sup s

Tactic:
⟨Finset.univ.image f, ht'.trans ?_⟩

Premises used: Finset.univ, Exists.intro, LE.le.trans, Finset.image
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u
inst : CompleteLattice α
k : α
H : ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : (↑t : Set α) ⊆ range s
ht' : k ≤ t.sup id
f : (x : ↥t) → ι
hf : ∀ (x : ↥t), s (f x) = (↑x : α)
mp : t.sup id ≤ (Finset.image f Finset.univ).sup s
⊢ ∃ (t : Finset ι), k ≤ t.sup s

Tactic:
refine ⟨Finset.univ.image f, ht'.trans ?_⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u
inst : CompleteLattice α
k : α
H : ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : (↑t : Set α) ⊆ range s
ht' : k ≤ t.sup id
f : (x : ↥t) → ι
hf : ∀ (x : ↥t), s (f x) = (↑x : α)
mp : ∀ b ∈ t, id b ≤ (Finset.image f Finset.univ).sup s
⊢ t.sup id ≤ (Finset.image f Finset.univ).sup s

Tactic:
rw [Finset.sup_le_iff]

Premises used: Finset.sup_le_iff
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u
inst : CompleteLattice α
k : α
H : ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : (↑t : Set α) ⊆ range s
ht' : k ≤ t.sup id
f : (x : ↥t) → ι
hf : ∀ (x : ↥t), s (f x) = (↑x : α)
b : α
hb : b ∈ t
mp : s (f (Subtype.mk (p := fun (x : α) ↦ x ∈ t) b hb)) ≤ (Finset.image f Finset.univ).sup s
⊢ id b ≤ (Finset.image f Finset.univ).sup s

Tactic:
rw [← show s (f ⟨b, hb⟩) = id b from hf _]

Premises used: Subtype.mk
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u
inst : CompleteLattice α
k : α
H : ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : (↑t : Set α) ⊆ range s
ht' : k ≤ t.sup id
f : (x : ↥t) → ι
hf : ∀ (x : ↥t), s (f x) = (↑x : α)
b : α
hb : b ∈ t
⊢ s (f (Subtype.mk (p := fun (x : α) ↦ x ∈ t) b hb)) ≤ (Finset.image f Finset.univ).sup s

Tactic:
Finset.le_sup (Finset.mem_image_of_mem f <| Finset.mem_univ (Subtype.mk b hb))

Premises used: Finset.mem_univ, Subtype.mk, Finset.mem_image_of_mem, Finset.le_sup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u
inst : CompleteLattice α
k : α
H : ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
ι : Type u
s : ι → α
hs : k ≤ iSup s
t : Finset α
ht : (↑t : Set α) ⊆ range s
ht' : k ≤ t.sup id
f : (x : ↥t) → ι
hf : ∀ (x : ↥t), s (f x) = (↑x : α)
b : α
hb : b ∈ t
⊢ s (f (Subtype.mk (p := fun (x : α) ↦ x ∈ t) b hb)) ≤ (Finset.image f Finset.univ).sup s

Tactic:
exact Finset.le_sup (Finset.mem_image_of_mem f <| Finset.mem_univ (Subtype.mk b hb))

Premises used: Finset.mem_univ, Subtype.mk, Finset.mem_image_of_mem, Finset.le_sup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u
inst : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s
s : Set α
hs : k ≤ sSup s
delta : k ≤ sSup (range (ι := (↑s : Type u)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))
⊢ k ≤ iSup (ι := (↑s : Type u)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
delta iSup

Premises used: iSup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u
inst : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s
s : Set α
hs rwa rwa₁ rwa₂ rwa₃ : k ≤ sSup s
⊢ k ≤ sSup (range (ι := (↑s : Type u)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))

Tactic:
rwa [Subtype.range_coe]

Premises used: Subtype.range_coe
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u
inst : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s
s : Set α
hs : k ≤ sSup s
mpr :
  ∀ (t : Finset (↑s : Type u)) (ht : k ≤ t.sup (Subtype.val (p := fun (x : α) ↦ x ∈ s))),
    ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id

Tactic:
obtain ⟨t, ht⟩ :=
        H s Subtype.val
          (by
            delta iSup
            rwa [Subtype.range_coe])

Premises used: Set.Elem, Subtype.val
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u
inst : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s
s : Set α
hs : k ≤ sSup s
t : Finset (↑s : Type u)
ht : k ≤ t.sup (Subtype.val (p := fun (x : α) ↦ x ∈ s))
⊢ (↑(Finset.image (Subtype.val (p := fun (x : α) ↦ x ∈ s)) t) : Set α) ⊆ s

Tactic:
simp
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u
inst : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s
s : Set α
hs : k ≤ sSup s
t : Finset (↑s : Type u)
ht : k ≤ t.sup (Subtype.val (p := fun (x : α) ↦ x ∈ s))
mpr : t.sup (Subtype.val (p := fun (x : α) ↦ x ∈ s)) ≤ (Finset.image (Subtype.val (p := fun (x : α) ↦ x ∈ s)) t).sup id
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id

Tactic:
refine ⟨t.image Subtype.val, by simp, ht.trans ?_⟩
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u
inst : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s
s : Set α
hs : k ≤ sSup s
t : Finset (↑s : Type u)
ht : k ≤ t.sup (Subtype.val (p := fun (x : α) ↦ x ∈ s))
mpr : ∀ b ∈ t, (↑b : α) ≤ (Finset.image (Subtype.val (p := fun (x : α) ↦ x ∈ s)) t).sup id
⊢ t.sup (Subtype.val (p := fun (x : α) ↦ x ∈ s)) ≤ (Finset.image (Subtype.val (p := fun (x : α) ↦ x ∈ s)) t).sup id

Tactic:
rw [Finset.sup_le_iff]

Premises used: Finset.sup_le_iff
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u
inst : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s
s : Set α
hs : k ≤ sSup s
t : Finset (↑s : Type u)
ht : k ≤ t.sup (Subtype.val (p := fun (x : α) ↦ x ∈ s))
⊢ ∀ b ∈ t, (↑b : α) ≤ (Finset.image (Subtype.val (p := fun (x : α) ↦ x ∈ s)) t).sup id

Tactic:
fun x hx => @Finset.le_sup _ _ _ _ _ id _ (Finset.mem_image_of_mem Subtype.val hx)

Premises used: Finset.mem_image_of_mem, Subtype.val, Finset.le_sup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u
inst : CompleteLattice α
k : α
H : ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s
s : Set α
hs : k ≤ sSup s
t : Finset (↑s : Type u)
ht : k ≤ t.sup (Subtype.val (p := fun (x : α) ↦ x ∈ s))
⊢ ∀ b ∈ t, (↑b : α) ≤ (Finset.image (Subtype.val (p := fun (x : α) ↦ x ∈ s)) t).sup id

Tactic:
exact fun x hx => @Finset.le_sup _ _ _ _ _ id _ (Finset.mem_image_of_mem Subtype.val hx)

Premises used: Finset.mem_image_of_mem, Subtype.val, Finset.le_sup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u
inst : CompleteLattice α
k : α
rw rw₁ rw₂ :
  (∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id) ↔
    ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s
mp :
  (∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id) →
    ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s
mpr mpr₁ :
  (∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s) →
    ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
⊢ IsCompactElement k ↔ ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s

Tactic:
classical
    rw [isCompactElement_iff_exists_le_sSup_of_le_sSup]
    constructor
    · intro H ι s hs
      obtain ⟨t, ht, ht'⟩ := H (Set.range s) hs
      have : ∀ x : t, ∃ i, s i = x := fun x => ht x.prop
      choose f hf using this
      refine ⟨Finset.univ.image f, ht'.trans ?_⟩
      rw [Finset.sup_le_iff]
      intro b hb
      rw [← show s (f ⟨b, hb⟩) = id b from hf _]
      exact Finset.le_sup (Finset.mem_image_of_mem f <| Finset.mem_univ (Subtype.mk b hb))
    · intro H s hs
      obtain ⟨t, ht⟩ :=
        H s Subtype.val
          (by
            delta iSup
            rwa [Subtype.range_coe])
      refine ⟨t.image Subtype.val, by simp, ht.trans ?_⟩
      rw [Finset.sup_le_iff]
      exact fun x hx => @Finset.le_sup _ _ _ _ _ id _ (Finset.mem_image_of_mem Subtype.val hx)

Premises used: Finset.sup_le_iff, CompleteLattice.isCompactElement_iff_exists_le_sSup_of_le_sSup, Finset.mem_image_of_mem, Subtype.val, Finset.le_sup
-- Module: Mathlib.Order.CompactlyGenerated.Basic
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ (i : ι), f i
rw :
  ∀ (hk : ∀ (s : Set α), s.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s → k ≤ sSup s → ∃ x ∈ s, k ≤ x)
    {ι : Type u_3} (f : ι → α) (h : k ≤ ⨆ (i : ι), f i), ∃ (s : Finset ι), k ≤ ⨆ i ∈ s, f i
⊢ ∃ (s : Finset ι), k ≤ ⨆ i ∈ s, f i

Tactic:
rw [isCompactElement_iff_le_of_directed_sSup_le] at hk

Premises used: CompleteLattice.isCompactElement_iff_le_of_directed_sSup_le
-- 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
ι : Type u_3
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun (s : Finset ι) ↦ ⨆ i ∈ s, f i
s t : Finset ι
⊢ ∃ z ∈ range g, (fun (x1 x2 : α) ↦ x1 ≤ x2) (g s) z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) (g t) z

Tactic:
⟨g (s ∪ t), ⟨s ∪ t, rfl⟩, iSup_le_iSup_of_subset Finset.subset_union_left,
          iSup_le_iSup_of_subset Finset.subset_union_right⟩

Premises used: Finset.subset_union_left, And.intro, Exists.intro, iSup_le_iSup_of_subset, Union.union, Finset.subset_union_right, rfl
-- 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
ι : Type u_3
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun (s : Finset ι) ↦ ⨆ i ∈ s, f i
s t : Finset ι
⊢ ∃ z ∈ range g, (fun (x1 x2 : α) ↦ x1 ≤ x2) (g s) z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) (g t) z

Tactic:
exact
        ⟨g (s ∪ t), ⟨s ∪ t, rfl⟩, iSup_le_iSup_of_subset Finset.subset_union_left,
          iSup_le_iSup_of_subset Finset.subset_union_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
ι : Type u_3
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun (s : Finset ι) ↦ ⨆ i ∈ s, f i
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (range g)

Tactic:
have h1 : DirectedOn (· ≤ ·) (Set.range g) := by
      rintro - ⟨s, rfl⟩ - ⟨t, rfl⟩
      exact
        ⟨g (s ∪ t), ⟨s ∪ t, rfl⟩, iSup_le_iSup_of_subset Finset.subset_union_left,
          iSup_le_iSup_of_subset Finset.subset_union_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
ι : Type u_3
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun (s : Finset ι) ↦ ⨆ i ∈ s, f i
h1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (range g)
⊢ k ≤ sSup (range g)

Tactic:
have h2 : k ≤ sSup (Set.range g) :=
      h.trans
        (iSup_le fun i =>
          le_sSup_of_le ⟨{i}, rfl⟩
            (le_iSup_of_le i (le_iSup_of_le (Finset.mem_singleton_self i) le_rfl)))
-- 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
ι : Type u_3
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun (s : Finset ι) ↦ ⨆ i ∈ s, f i
h1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (range g)
h2 : k ≤ sSup (range g)
obtain : ∀ (s : Finset ι) (hs : k ≤ g s), ∃ (s : Finset ι), k ≤ ⨆ i ∈ s, f i
⊢ ∃ (s : Finset ι), k ≤ ⨆ i ∈ s, f i

Tactic:
obtain ⟨-, ⟨s, rfl⟩, hs⟩ := hk (Set.range g) (Set.range_nonempty g) h1 h2

Premises used: Set.range_nonempty, Set.range, rfl
-- 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
ι : Type u_3
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun (s : Finset ι) ↦ ⨆ i ∈ s, f i
h1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (range g)
h2 : k ≤ sSup (range g)
s : Finset ι
hs : k ≤ g s
⊢ ∃ (s : Finset ι), k ≤ ⨆ i ∈ s, f i

Tactic:
⟨s, hs⟩

Premises used: Exists.intro
-- 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
ι : Type u_3
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun (s : Finset ι) ↦ ⨆ i ∈ s, f i
h1 : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (range g)
h2 : k ≤ sSup (range g)
s : Finset ι
hs : k ≤ g s
⊢ ∃ (s : Finset ι), k ≤ ⨆ i ∈ s, f i

Tactic:
exact ⟨s, hs⟩