-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem isCompactElement_iff_le_of_directed_sSup_le (k : α) :
    IsCompactElement k ↔
      ∀ s : Set α, s.Nonempty → DirectedOn (· ≤ ·) s → k ≤ sSup s → ∃ x : α, x ∈ s ∧ k ≤ x

Proof state:
case mpr
α : 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, ↑t ⊆ s ∧ x = t.sup id}
dir_US : DirectedOn (fun x1 x2 => x1 ≤ x2) S
sup_S : sSup s ≤ sSup S
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id

Tactic:
have Sne : S.Nonempty := by
  suffices ⊥ ∈ S from Set.nonempty_of_mem this
  use ∅
  simp only [Set.empty_subset, Finset.coe_empty, Finset.sup_empty, eq_self_iff_true,
    and_self_iff]

Result:
case mpr
α : 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, ↑t ⊆ s ∧ x = t.sup id}
dir_US : DirectedOn (fun x1 x2 => x1 ≤ x2) S
sup_S : sSup s ≤ sSup S
Sne : S.Nonempty
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id

Proof state:
case h
α : 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, ↑t ⊆ s ∧ x = t.sup id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = d.sup id
⊢ ↑(c ∪ d) ⊆ s ∧ x ⊔ y = (c ∪ d).sup id

Tactic:
constructor

Result:
case h.left
α : 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, ↑t ⊆ s ∧ x = t.sup id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = d.sup id
⊢ ↑(c ∪ d) ⊆ s

case h.right
α : 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, ↑t ⊆ s ∧ x = t.sup id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = d.sup id
⊢ x ⊔ y = (c ∪ d).sup id

Proof state:
case intro.intro
α : 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, ↑t ⊆ s ∧ x = t.sup id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = d.sup id
⊢ ∃ z ∈ S, (fun x1 x2 => x1 ≤ x2) x z ∧ (fun x1 x2 => x1 ≤ x2) y z

Tactic:
use x ⊔ y

Result:
case h
α : 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, ↑t ⊆ s ∧ x = t.sup id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = c.sup id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = d.sup id
⊢ x ⊔ y ∈ S ∧ (fun x1 x2 => x1 ≤ x2) x (x ⊔ y) ∧ (fun x1 x2 => x1 ≤ x2) y (x ⊔ y)

Proof state:
α : 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, ↑t ⊆ 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 ⊆ s
htsup : j = t.sup id
⊢ k ≤ t.sup id

Tactic:
rwa [← htsup]

Result:
no goals

Proof state:
case mp.intro
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
s : Set α
hne : s.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hsup : k ≤ sSup s
t : Finset α
ht : ↑t ⊆ s ∧ k ≤ t.sup id
⊢ ∃ x ∈ s, k ≤ x

Tactic:
have t_below_s : ∀ x ∈ t, ∃ y ∈ s, x ≤ y := fun x hxt => ⟨x, ht.left hxt, le_rfl⟩

Result:
case mp.intro
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
s : Set α
hne : s.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) s
hsup : k ≤ sSup s
t : Finset α
ht : ↑t ⊆ s ∧ k ≤ t.sup id
t_below_s : ∀ x ∈ t, ∃ y ∈ s, x ≤ y
⊢ ∃ x ∈ s, k ≤ x

Proof state:
case mpr.intro.intro
α : 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, ↑t ⊆ 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, ↑t ⊆ s ∧ k ≤ t.sup id

Tactic:
obtain ⟨t, ⟨htS, htsup⟩⟩ := hjS

Result:
case mpr.intro.intro.intro.intro
α : 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, ↑t ⊆ 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 ⊆ s
htsup : j = t.sup id
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ t.sup id