case mp
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
⊢ IsCompactElement k →
    ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x

case mpr
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
⊢ (∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x) →
    IsCompactElement k
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
⊢ IsCompactElement k ↔
    ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
constructor
case mp
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : IsCompactElement k
s : Set α
hne : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hsup : k ≤ sSup s
⊢ ∃ x, x ∈ s ∧ k ≤ x
case mp
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
⊢ IsCompactElement k →
    ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
intro hk s hne hdir hsup
case mp.intro
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : IsCompactElement k
s : Set α
hne : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hsup : k ≤ sSup s
t : Finset α
ht : ↑t ⊆ s ∧ k ≤ Finset.sup t id
⊢ ∃ x, x ∈ s ∧ k ≤ x
case mp
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : IsCompactElement k
s : Set α
hne : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hsup : k ≤ sSup s
⊢ ∃ x, x ∈ s ∧ k ≤ x
obtain ⟨t, ht⟩ := hk s hsup
case mp.intro
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : IsCompactElement k
s : Set α
hne : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hsup : k ≤ sSup s
t : Finset α
ht : ↑t ⊆ s ∧ k ≤ Finset.sup t id
t_below_s : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ x ≤ y
⊢ ∃ x, x ∈ s ∧ k ≤ x
case mp.intro
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : IsCompactElement k
s : Set α
hne : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hsup : k ≤ sSup s
t : Finset α
ht : ↑t ⊆ s ∧ k ≤ Finset.sup t id
⊢ ∃ x, x ∈ s ∧ k ≤ x
have t_below_s : ∀ x ∈ t, ∃ y ∈ s, x ≤ y := fun x hxt => ⟨x, ht.left hxt, le_rfl⟩
case mp.intro.intro.intro
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : IsCompactElement k
s : Set α
hne : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hsup : k ≤ sSup s
t : Finset α
ht : ↑t ⊆ s ∧ k ≤ Finset.sup t id
t_below_s : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ x ≤ y
x : α
hxs : x ∈ s
hsupx : Finset.sup t id ≤ x
⊢ ∃ x, x ∈ s ∧ k ≤ x
case mp.intro
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : IsCompactElement k
s : Set α
hne : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hsup : k ≤ sSup s
t : Finset α
ht : ↑t ⊆ s ∧ k ≤ Finset.sup t id
t_below_s : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ x ≤ y
⊢ ∃ x, x ∈ s ∧ k ≤ x
obtain ⟨x, ⟨hxs, hsupx⟩⟩ := Finset.sup_le_of_le_directed s hne hdir t t_below_s
no goals
case mp.intro.intro.intro
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : IsCompactElement k
s : Set α
hne : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hsup : k ≤ sSup s
t : Finset α
ht : ↑t ⊆ s ∧ k ≤ Finset.sup t id
t_below_s : ∀ (x : α), x ∈ t → ∃ y, y ∈ s ∧ x ≤ y
x : α
hxs : x ∈ s
hsupx : Finset.sup t id ≤ x
⊢ ∃ x, x ∈ s ∧ k ≤ x
exact ⟨x, ⟨hxs, le_trans ht.right hsupx⟩⟩
case mpr
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
case mpr
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
⊢ (∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x) →
    IsCompactElement k
intro hk s hsup
case mpr
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
case mpr
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
let S : Set α := { x | ∃ t : Finset α, ↑t ⊆ s ∧ x = t.sup id }
case mpr
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
case mpr
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
have sup_S : sSup s ≤ sSup S := by
  apply sSup_le_sSup
  intro x hx
  use {x}
  simpa only [and_true_iff, id.def, Finset.coe_singleton, eq_self_iff_true,
    Finset.sup_singleton, Set.singleton_subset_iff]
case mpr
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
Sne : Set.Nonempty S
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
case mpr
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
have Sne : S.Nonempty := by
  suffices : ⊥ ∈ S
  exact Set.nonempty_of_mem this
  use ∅
  simp only [Set.empty_subset, Finset.coe_empty, Finset.sup_empty, eq_self_iff_true,
    and_self_iff]
case mpr.intro.intro
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
Sne : Set.Nonempty S
j : α
hjS : j ∈ S
hjk : k ≤ j
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
case mpr
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
Sne : Set.Nonempty S
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
obtain ⟨j, ⟨hjS, hjk⟩⟩ := hk S Sne dir_US (le_trans hsup sup_S)
case mpr.intro.intro.intro.intro
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
Sne : Set.Nonempty S
j : α
hjk : k ≤ j
t : Finset α
htS : ↑t ⊆ s
htsup : j = Finset.sup t id
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
case mpr.intro.intro
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
Sne : Set.Nonempty S
j : α
hjS : j ∈ S
hjk : k ≤ j
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
obtain ⟨t, ⟨htS, htsup⟩⟩ := hjS
case mpr.intro.intro.intro.intro
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
Sne : Set.Nonempty S
j : α
hjk : k ≤ j
t : Finset α
htS : ↑t ⊆ s
htsup : j = Finset.sup t id
⊢ ↑t ⊆ s ∧ k ≤ Finset.sup t id
case mpr.intro.intro.intro.intro
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
Sne : Set.Nonempty S
j : α
hjk : k ≤ j
t : Finset α
htS : ↑t ⊆ s
htsup : j = Finset.sup t id
⊢ ∃ t, ↑t ⊆ s ∧ k ≤ Finset.sup t id
use t
no goals
case mpr.intro.intro.intro.intro
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
Sne : Set.Nonempty S
j : α
hjk : k ≤ j
t : Finset α
htS : ↑t ⊆ s
htsup : j = Finset.sup t id
⊢ ↑t ⊆ s ∧ k ≤ Finset.sup t id
exact ⟨htS, by rwa [← htsup]⟩
case intro.intro
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = Finset.sup c id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = Finset.sup d id
⊢ ∃ z, z ∈ S ∧ (fun x x_1 => x ≤ x_1) x z ∧ (fun x x_1 => x ≤ x_1) y z
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
⊢ DirectedOn (fun x x_1 => x ≤ x_1) S
rintro x ⟨c, hc⟩ y ⟨d, hd⟩
case intro.intro
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = Finset.sup c id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = Finset.sup d id
⊢ x ⊔ y ∈ S ∧ (fun x x_1 => x ≤ x_1) x (x ⊔ y) ∧ (fun x x_1 => x ≤ x_1) y (x ⊔ y)
case intro.intro
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = Finset.sup c id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = Finset.sup d id
⊢ ∃ z, z ∈ S ∧ (fun x x_1 => x ≤ x_1) x z ∧ (fun x x_1 => x ≤ x_1) y z
use x ⊔ y
case intro.intro.left
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = Finset.sup c id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = Finset.sup d id
⊢ x ⊔ y ∈ S

case intro.intro.right
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = Finset.sup c id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = Finset.sup d id
⊢ (fun x x_1 => x ≤ x_1) x (x ⊔ y) ∧ (fun x x_1 => x ≤ x_1) y (x ⊔ y)
case intro.intro
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = Finset.sup c id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = Finset.sup d id
⊢ x ⊔ y ∈ S ∧ (fun x x_1 => x ≤ x_1) x (x ⊔ y) ∧ (fun x x_1 => x ≤ x_1) y (x ⊔ y)
constructor
no goals
case intro.intro.right
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = Finset.sup c id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = Finset.sup d id
⊢ (fun x x_1 => x ≤ x_1) x (x ⊔ y) ∧ (fun x x_1 => x ≤ x_1) y (x ⊔ y)
simp only [and_self_iff, le_sup_left, le_sup_right]
case intro.intro.left
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = Finset.sup c id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = Finset.sup d id
⊢ ↑(c ∪ d) ⊆ s ∧ x ⊔ y = Finset.sup (c ∪ d) id
case intro.intro.left
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = Finset.sup c id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = Finset.sup d id
⊢ x ⊔ y ∈ S
use c ∪ d
case intro.intro.left.left
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = Finset.sup c id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = Finset.sup d id
⊢ ↑(c ∪ d) ⊆ s

case intro.intro.left.right
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = Finset.sup c id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = Finset.sup d id
⊢ x ⊔ y = Finset.sup (c ∪ d) id
case intro.intro.left
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = Finset.sup c id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = Finset.sup d id
⊢ ↑(c ∪ d) ⊆ s ∧ x ⊔ y = Finset.sup (c ∪ d) id
constructor
no goals
case intro.intro.left.left
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = Finset.sup c id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = Finset.sup d id
⊢ ↑(c ∪ d) ⊆ s
simp only [hc.left, hd.left, Set.union_subset_iff, Finset.coe_union, and_self_iff]
no goals
case intro.intro.left.right
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
x : α
c : Finset α
hc : ↑c ⊆ s ∧ x = Finset.sup c id
y : α
d : Finset α
hd : ↑d ⊆ s ∧ y = Finset.sup d id
⊢ x ⊔ y = Finset.sup (c ∪ d) id
simp only [hc.right, hd.right, Finset.sup_union]
case h
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
⊢ s ⊆ S
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
⊢ sSup s ≤ sSup S
apply sSup_le_sSup
case h
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
x : α
hx : x ∈ s
⊢ x ∈ S
case h
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
⊢ s ⊆ S
intro x hx
case h
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
x : α
hx : x ∈ s
⊢ ↑{x} ⊆ s ∧ x = Finset.sup {x} id
case h
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
x : α
hx : x ∈ s
⊢ x ∈ S
use {x}
no goals
case h
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
x : α
hx : x ∈ s
⊢ ↑{x} ⊆ s ∧ x = Finset.sup {x} id
simpa only [and_true_iff, id.def, Finset.coe_singleton, eq_self_iff_true,
  Finset.sup_singleton, Set.singleton_subset_iff]
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
this : ⊥ ∈ S
⊢ Set.Nonempty S

case this
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
⊢ ⊥ ∈ S
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
⊢ Set.Nonempty S
suffices : ⊥ ∈ S
case this
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
⊢ ⊥ ∈ S
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
this : ⊥ ∈ S
⊢ Set.Nonempty S

case this
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
⊢ ⊥ ∈ S
exact Set.nonempty_of_mem this
case this
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
⊢ ↑∅ ⊆ s ∧ ⊥ = Finset.sup ∅ id
case this
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
⊢ ⊥ ∈ S
use ∅
no goals
case this
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
⊢ ↑∅ ⊆ s ∧ ⊥ = Finset.sup ∅ id
simp only [Set.empty_subset, Finset.coe_empty, Finset.sup_empty, eq_self_iff_true,
  and_self_iff]
no goals
ι : Sort ?u.5271
α : Type u_1
inst✝ : CompleteLattice α
f : ι → α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hsup : k ≤ sSup s
S : Set α := {x | ∃ t, ↑t ⊆ s ∧ x = Finset.sup t id}
dir_US : DirectedOn (fun x x_1 => x ≤ x_1) S
sup_S : sSup s ≤ sSup S
Sne : Set.Nonempty S
j : α
hjk : k ≤ j
t : Finset α
htS : ↑t ⊆ s
htsup : j = Finset.sup t id
⊢ k ≤ Finset.sup t id
rwa [← htsup]