ι✝ : Sort ?u.10018
α : Type u_1
inst✝ : CompleteLattice α
f✝ : ι✝ → α
k : α
hk : IsCompactElement k
ι : Type u_2
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun s => ⨆ (i : ι) (_ : i ∈ s), f i
⊢ ∃ s, k ≤ ⨆ (i : ι) (_ : i ∈ s), f i
ι✝ : Sort ?u.10018
α : Type u_1
inst✝ : CompleteLattice α
f✝ : ι✝ → α
k : α
hk : IsCompactElement k
ι : Type u_2
f : ι → α
h : k ≤ ⨆ (i : ι), f i
⊢ ∃ s, k ≤ ⨆ (i : ι) (_ : i ∈ s), f i
let g : Finset ι → α := fun s => ⨆ i ∈ s, f i
ι✝ : Sort ?u.10018
α : Type u_1
inst✝ : CompleteLattice α
f✝ : ι✝ → α
k : α
hk : IsCompactElement k
ι : Type u_2
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun s => ⨆ (i : ι) (_ : i ∈ s), f i
h1 : DirectedOn (fun x x_1 => x ≤ x_1) (Set.range g)
h2 : k ≤ sSup (Set.range g)
⊢ ∃ s, k ≤ ⨆ (i : ι) (_ : i ∈ s), f i
ι✝ : Sort ?u.10018
α : Type u_1
inst✝ : CompleteLattice α
f✝ : ι✝ → α
k : α
hk : IsCompactElement k
ι : Type u_2
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun s => ⨆ (i : ι) (_ : i ∈ s), f i
h1 : DirectedOn (fun x x_1 => x ≤ x_1) (Set.range g)
⊢ ∃ s, k ≤ ⨆ (i : ι) (_ : i ∈ s), f i
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)))
case intro.intro.intro
ι✝ : Sort ?u.10018
α : Type u_1
inst✝ : CompleteLattice α
f✝ : ι✝ → α
k : α
hk : IsCompactElement k
ι : Type u_2
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun s => ⨆ (i : ι) (_ : i ∈ s), f i
h1 : DirectedOn (fun x x_1 => x ≤ x_1) (Set.range g)
h2 : k ≤ sSup (Set.range g)
s : Finset ι
hs : k ≤ g s
⊢ ∃ s, k ≤ ⨆ (i : ι) (_ : i ∈ s), f i
ι✝ : Sort ?u.10018
α : Type u_1
inst✝ : CompleteLattice α
f✝ : ι✝ → α
k : α
hk : IsCompactElement k
ι : Type u_2
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun s => ⨆ (i : ι) (_ : i ∈ s), f i
h1 : DirectedOn (fun x x_1 => x ≤ x_1) (Set.range g)
h2 : k ≤ sSup (Set.range g)
⊢ ∃ s, k ≤ ⨆ (i : ι) (_ : i ∈ s), f i
obtain ⟨-, ⟨s, rfl⟩, hs⟩ :=
  (isCompactElement_iff_le_of_directed_sSup_le α k).mp hk (Set.range g) (Set.range_nonempty g)
    h1 h2
no goals
case intro.intro.intro
ι✝ : Sort ?u.10018
α : Type u_1
inst✝ : CompleteLattice α
f✝ : ι✝ → α
k : α
hk : IsCompactElement k
ι : Type u_2
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun s => ⨆ (i : ι) (_ : i ∈ s), f i
h1 : DirectedOn (fun x x_1 => x ≤ x_1) (Set.range g)
h2 : k ≤ sSup (Set.range g)
s : Finset ι
hs : k ≤ g s
⊢ ∃ s, k ≤ ⨆ (i : ι) (_ : i ∈ s), f i
exact ⟨s, hs⟩
case intro.intro
ι✝ : Sort ?u.10018
α : Type u_1
inst✝ : CompleteLattice α
f✝ : ι✝ → α
k : α
hk : IsCompactElement k
ι : Type u_2
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun s => ⨆ (i : ι) (_ : i ∈ s), f i
s t : Finset ι
⊢ ∃ z, z ∈ Set.range g ∧ (fun x x_1 => x ≤ x_1) (g s) z ∧ (fun x x_1 => x ≤ x_1) (g t) z
ι✝ : Sort ?u.10018
α : Type u_1
inst✝ : CompleteLattice α
f✝ : ι✝ → α
k : α
hk : IsCompactElement k
ι : Type u_2
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun s => ⨆ (i : ι) (_ : i ∈ s), f i
⊢ DirectedOn (fun x x_1 => x ≤ x_1) (Set.range g)
rintro - ⟨s, rfl⟩ - ⟨t, rfl⟩
no goals
case intro.intro
ι✝ : Sort ?u.10018
α : Type u_1
inst✝ : CompleteLattice α
f✝ : ι✝ → α
k : α
hk : IsCompactElement k
ι : Type u_2
f : ι → α
h : k ≤ ⨆ (i : ι), f i
g : Finset ι → α := fun s => ⨆ (i : ι) (_ : i ∈ s), f i
s t : Finset ι
⊢ ∃ z, z ∈ Set.range g ∧ (fun x x_1 => x ≤ x_1) (g s) z ∧ (fun x x_1 => x ≤ x_1) (g t) z
exact
  ⟨g (s ∪ t), ⟨s ∪ t, rfl⟩, iSup_le_iSup_of_subset (Finset.subset_union_left s t),
    iSup_le_iSup_of_subset (Finset.subset_union_right s t)⟩