-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem IsCompactElement.exists_finset_of_le_iSup {k : α} (hk : IsCompactElement k) {ι : Type*}
    (f : ι → α) (h : k ≤ ⨆ i, f i) : ∃ s : Finset ι, k ≤ ⨆ i ∈ s, f i

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ i, f i
g : Finset ι → α := fun s => ⨆ i ∈ s, f i
h1 : DirectedOn (fun x1 x2 => x1 ≤ x2) (range g)
⊢ ∃ s, k ≤ ⨆ i ∈ s, f i

Tactic:
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)))

Result:
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ i, f i
g : Finset ι → α := fun s => ⨆ i ∈ s, f i
h1 : DirectedOn (fun x1 x2 => x1 ≤ x2) (range g)
h2 : k ≤ sSup (range g)
⊢ ∃ s, k ≤ ⨆ i ∈ s, f i

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ i, f i
g : Finset ι → α := fun s => ⨆ i ∈ s, f i
h1 : DirectedOn (fun x1 x2 => x1 ≤ x2) (range g)
h2 : k ≤ sSup (range g)
⊢ ∃ s, k ≤ ⨆ i ∈ s, f i

Tactic:
obtain ⟨-, ⟨s, rfl⟩, hs⟩ :=
  (isCompactElement_iff_le_of_directed_sSup_le α k).mp hk (Set.range g) (Set.range_nonempty g)
    h1 h2

Result:
case intro.intro.intro
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ i, f i
g : Finset ι → α := fun s => ⨆ i ∈ s, f i
h1 : DirectedOn (fun x1 x2 => x1 ≤ x2) (range g)
h2 : k ≤ sSup (range g)
s : Finset ι
hs : k ≤ g s
⊢ ∃ s, k ≤ ⨆ i ∈ s, f i

Proof state:
case intro.intro
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ i, f i
g : Finset ι → α := fun s => ⨆ i ∈ s, f i
s t : Finset ι
⊢ ∃ z ∈ range g, (fun x1 x2 => x1 ≤ x2) (g s) z ∧ (fun x1 x2 => x1 ≤ x2) (g t) z

Tactic:
exact
  ⟨g (s ∪ t), ⟨s ∪ t, rfl⟩, iSup_le_iSup_of_subset Finset.subset_union_left,
    iSup_le_iSup_of_subset Finset.subset_union_right⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ i, f i
g : Finset ι → α := fun s => ⨆ i ∈ s, f i
⊢ DirectedOn (fun x1 x2 => x1 ≤ x2) (range g)

Tactic:
rintro - ⟨s, rfl⟩ - ⟨t, rfl⟩

Result:
case intro.intro
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ i, f i
g : Finset ι → α := fun s => ⨆ i ∈ s, f i
s t : Finset ι
⊢ ∃ z ∈ range g, (fun x1 x2 => x1 ≤ x2) (g s) z ∧ (fun x1 x2 => x1 ≤ x2) (g t) z

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ i, f i
⊢ ∃ s, k ≤ ⨆ i ∈ s, f i

Tactic:
let g : Finset ι → α := fun s => ⨆ i ∈ s, f i

Result:
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ i, f i
g : Finset ι → α := fun s => ⨆ i ∈ s, f i
⊢ ∃ s, k ≤ ⨆ i ∈ s, f i

Proof state:
case intro.intro.intro
α : Type u_2
inst✝ : CompleteLattice α
k : α
hk : IsCompactElement k
ι : Type u_3
f : ι → α
h : k ≤ ⨆ i, f i
g : Finset ι → α := fun s => ⨆ i ∈ s, f i
h1 : DirectedOn (fun x1 x2 => x1 ≤ x2) (range g)
h2 : k ≤ sSup (range g)
s : Finset ι
hs : k ≤ g s
⊢ ∃ s, k ≤ ⨆ i ∈ s, f i

Tactic:
exact ⟨s, hs⟩

Result:
no goals