ι : Sort ?u.12274
α✝ : Type ?u.12277
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u_1
inst✝ : CompleteLattice α
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 α
hemp : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hbelow : ∀ (x : α), x ∈ s → x < k
⊢ sSup s < k
ι : Sort ?u.12274
α✝ : Type ?u.12277
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u_1
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
s : Set α
hemp : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hbelow : ∀ (x : α), x ∈ s → x < k
⊢ sSup s < k
rw [isCompactElement_iff_le_of_directed_sSup_le] at hk
ι : Sort ?u.12274
α✝ : Type ?u.12277
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u_1
inst✝ : CompleteLattice α
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 α
hemp : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hbelow : ∀ (x : α), x ∈ s → x < k
h : ¬sSup s < k
⊢ False
ι : Sort ?u.12274
α✝ : Type ?u.12277
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u_1
inst✝ : CompleteLattice α
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 α
hemp : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hbelow : ∀ (x : α), x ∈ s → x < k
⊢ sSup s < k
by_contra h
ι : Sort ?u.12274
α✝ : Type ?u.12277
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u_1
inst✝ : CompleteLattice α
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 α
hemp : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hbelow : ∀ (x : α), x ∈ s → x < k
h : ¬sSup s < k
sSup' : sSup s ≤ k
⊢ False
ι : Sort ?u.12274
α✝ : Type ?u.12277
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u_1
inst✝ : CompleteLattice α
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 α
hemp : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hbelow : ∀ (x : α), x ∈ s → x < k
h : ¬sSup s < k
⊢ False
have sSup' : sSup s ≤ k := sSup_le s k fun s hs => (hbelow s hs).le
ι : Sort ?u.12274
α✝ : Type ?u.12277
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u_1
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ SupSet.sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hemp : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hbelow : ∀ (x : α), x ∈ s → x < k
h : ¬SupSet.sSup s < k
sSup' : SupSet.sSup s ≤ k
sSup : SupSet.sSup s = k
⊢ False
ι : Sort ?u.12274
α✝ : Type ?u.12277
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u_1
inst✝ : CompleteLattice α
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 α
hemp : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hbelow : ∀ (x : α), x ∈ s → x < k
h : ¬sSup s < k
sSup' : sSup s ≤ k
⊢ False
replace sSup : sSup s = k := eq_iff_le_not_lt.mpr ⟨sSup', h⟩
case intro.intro
ι : Sort ?u.12274
α✝ : Type ?u.12277
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u_1
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ SupSet.sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hemp : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hbelow : ∀ (x : α), x ∈ s → x < k
h : ¬SupSet.sSup s < k
sSup' : SupSet.sSup s ≤ k
sSup : SupSet.sSup s = k
x : α
hxs : x ∈ s
hkx : k ≤ x
⊢ False
ι : Sort ?u.12274
α✝ : Type ?u.12277
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u_1
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ SupSet.sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hemp : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hbelow : ∀ (x : α), x ∈ s → x < k
h : ¬SupSet.sSup s < k
sSup' : SupSet.sSup s ≤ k
sSup : SupSet.sSup s = k
⊢ False
obtain ⟨x, hxs, hkx⟩ := hk s hemp hdir sSup.symm.le
case intro.intro
ι : Sort ?u.12274
α✝ : Type ?u.12277
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u_1
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ SupSet.sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hemp : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hbelow : ∀ (x : α), x ∈ s → x < k
h : ¬SupSet.sSup s < k
sSup' : SupSet.sSup s ≤ k
sSup : SupSet.sSup s = k
x : α
hxs : x ∈ s
hkx : k ≤ x
hxk : x < k
⊢ False
case intro.intro
ι : Sort ?u.12274
α✝ : Type ?u.12277
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u_1
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ SupSet.sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hemp : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hbelow : ∀ (x : α), x ∈ s → x < k
h : ¬SupSet.sSup s < k
sSup' : SupSet.sSup s ≤ k
sSup : SupSet.sSup s = k
x : α
hxs : x ∈ s
hkx : k ≤ x
⊢ False
obtain hxk := hbelow x hxs
no goals
case intro.intro
ι : Sort ?u.12274
α✝ : Type ?u.12277
inst✝¹ : CompleteLattice α✝
f : ι → α✝
α : Type u_1
inst✝ : CompleteLattice α
k : α
hk : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → k ≤ SupSet.sSup s → ∃ x, x ∈ s ∧ k ≤ x
s : Set α
hemp : Set.Nonempty s
hdir : DirectedOn (fun x x_1 => x ≤ x_1) s
hbelow : ∀ (x : α), x ∈ s → x < k
h : ¬SupSet.sSup s < k
sSup' : SupSet.sSup s ≤ k
sSup : SupSet.sSup s = k
x : α
hxs : x ∈ s
hkx : k ≤ x
hxk : x < k
⊢ False
exact hxk.ne (hxk.le.antisymm hkx)