awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 ∈ S
have h : (↑(c ∪ d) : Set α) ⊆ s ∧ x ⊔ y = (c ∪ d).sup id
Tactic: use c ∪ d
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 ∧ x ⊔ y = (c ∪ d).sup id
have h : (↑(c ∪ d) : Set α) ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ (↑(c ∪ d) : Set α) ⊆ s ∧ x ⊔ y = (c ∪ d).sup id
have h₁ : x ⊔ y = (c ∪ d).sup id
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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}
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
have dir_US : 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]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
have h : s ⊆ S
Tactic: apply sSup_le_sSup
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 ∈ S
have h : (↑{x} : Set α) ⊆ s ∧ x = Finset.sup {x} id
Tactic: use {x}
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
have sup_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]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
have suffices : ⊥ ∈ S
Tactic: suffices ⊥ ∈ S from Set.nonempty_of_mem this
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
have h : (↑∅ : Set α) ⊆ s ∧ Eq.{u_2 + 1} (α := α) ⊥ (Finset.sup ∅ id)
Tactic: use ∅
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
have Sne : S.Nonempty
Tactic: have Sne : S.Nonempty := by
        suffices ⊥ ∈ S from Set.nonempty_of_mem this
        use ∅
        simp
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
have mp : ∀ (j : α) (hjS : j ∈ S) (hjk : k ≤ j), ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
Tactic: obtain ⟨j, ⟨hjS, hjk⟩⟩ := hk S Sne dir_US (le_trans hsup sup_S)
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
have mp : ∀ (t : Finset α) (htS : (↑t : Set α) ⊆ s) (htsup : j = t.sup id), ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
Tactic: obtain ⟨t, ⟨htS, htsup⟩⟩ := hjS
Cleared hypotheses: hjS
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
have h : (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
Tactic: use t
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ ∃ x ∈ s, k ≤ x
have mpr : ∀ (t : Finset α) (ht : (↑t : Set α) ⊆ s ∧ k ≤ t.sup id), ∃ x ∈ s, k ≤ x
Tactic: obtain ⟨t, ht⟩ := hk s hsup
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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 ∈ s, k ≤ x
have t_below_s : ∀ 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⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 ∈ s, k ≤ x
have mpr : ∀ (x : α) (hxs : x ∈ s) (hsupx : t.sup id ≤ x), ∃ x ∈ s, k ≤ x
Tactic: obtain ⟨x, ⟨hxs, hsupx⟩⟩ := Finset.sup_le_of_le_directed s hne hdir t t_below_s
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u_2
inst : CompleteLattice α
k : α
⊢ IsCompactElement k ↔ ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
have 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
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⟩⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ IsCompactElement k ↔ ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
have 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
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⟩⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ IsCompactElement k ↔ ∀ (s : Set α), k ≤ sSup s → ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
have 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
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⟩⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u
inst : CompleteLattice α
k : α
⊢ IsCompactElement k ↔ ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s
have 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
Tactic: rw [isCompactElement_iff_exists_le_sSup_of_le_sSup]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u
inst : CompleteLattice α
k : α
⊢ (∀ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ (∀ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 ι), k ≤ t.sup s
have mp : ∀ (t : Finset α) (ht : (↑t : Set α) ⊆ range s) (ht' : k ≤ t.sup id), ∃ (t : Finset ι), k ≤ t.sup s
Tactic: obtain ⟨t, ht, ht'⟩ := H (Set.range s) hs
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (hypothesis)
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
⊢ ∃ (t : Finset ι), k ≤ t.sup s
have this : ∀ (x : ↥t), ∃ (i : ι), s i = (↑x : α)
Tactic: have : ∀ x : t, ∃ i, s i = x := fun x => ht x.prop
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 : α)
⊢ ∃ (t : Finset ι), k ≤ t.sup s
have mp : ∀ (f : (x : ↥t) → ι) (hf : ∀ (x : ↥t), s (f x) = (↑x : α)), ∃ (t : Finset ι), k ≤ t.sup s
Tactic: choose f hf using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
have mp : t.sup id ≤ (Finset.image f Finset.univ).sup s
Tactic: refine ⟨Finset.univ.image f, ht'.trans ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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.sup id ≤ (Finset.image f Finset.univ).sup s
have mp : ∀ b ∈ t, id b ≤ (Finset.image f Finset.univ).sup s
Tactic: rw [Finset.sup_le_iff]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ id b ≤ (Finset.image f Finset.univ).sup s
have mp : s (f (Subtype.mk (p := fun (x : α) ↦ x ∈ t) b hb)) ≤ (Finset.image f Finset.univ).sup s
Tactic: rw [← show s (f ⟨b, hb⟩) = id b from hf _]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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
⊢ k ≤ iSup (ι := (↑s : Type u)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
have delta : k ≤ sSup (range (ι := (↑s : Type u)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)))
Tactic: delta iSup
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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 α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
have 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
Tactic: obtain ⟨t, ht⟩ :=
        H s Subtype.val
          (by
            delta iSup
            rwa [Subtype.range_coe])
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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))
⊢ ∃ (t : Finset α), (↑t : Set α) ⊆ s ∧ k ≤ t.sup id
have mpr : t.sup (Subtype.val (p := fun (x : α) ↦ x ∈ s)) ≤ (Finset.image (Subtype.val (p := fun (x : α) ↦ x ∈ s)) t).sup id
Tactic: refine ⟨t.image Subtype.val, by simp, ht.trans ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
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))
⊢ t.sup (Subtype.val (p := fun (x : α) ↦ x ∈ s)) ≤ (Finset.image (Subtype.val (p := fun (x : α) ↦ x ∈ s)) t).sup id
have mpr : ∀ b ∈ t, (↑b : α) ≤ (Finset.image (Subtype.val (p := fun (x : α) ↦ x ∈ s)) t).sup id
Tactic: rw [Finset.sup_le_iff]
-- Lean 4 proof step from Mathlib.Order.CompactlyGenerated.Basic (goal)
Goal:
α : Type u
inst : CompleteLattice α
k : α
⊢ IsCompactElement k ↔ ∀ (ι : Type u) (s : ι → α), k ≤ iSup s → ∃ (t : Finset ι), k ≤ t.sup s
have 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
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)