-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem isCompactElement_finsetSup {α β : Type*} [CompleteLattice α] {f : β → α} (s : Finset β)
    (h : ∀ x ∈ s, IsCompactElement (f x)) : IsCompactElement (s.sup f)

Proof state:
case a.intro.intro
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
⊢ ∃ y ∈ d, f p ≤ y

Tactic:
specialize h p hps

Result:
case a.intro.intro
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
h : IsCompactElement (f p)
⊢ ∃ y ∈ d, f p ≤ y

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
⊢ ∃ x ∈ d, s.sup (id ∘ f) ≤ x

Tactic:
rw [← Finset.sup_image]

Result:
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
⊢ ∃ x ∈ d, (Finset.image f s).sup id ≤ x

Proof state:
case a.intro.intro
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
h : IsCompactElement (f p)
⊢ ∃ y ∈ d, f p ≤ y

Tactic:
rw [isCompactElement_iff_le_of_directed_sSup_le] at h

Result:
case a.intro.intro
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) s → f p ≤ sSup s → ∃ x ∈ s, f p ≤ x
⊢ ∃ y ∈ d, f p ≤ y

Proof state:
case a
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
⊢ ∀ x ∈ Finset.image f s, ∃ y ∈ d, x ≤ y

Tactic:
rintro x hx

Result:
case a
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
x : α
hx : x ∈ Finset.image f s
⊢ ∃ y ∈ d, x ≤ y

Proof state:
case a.intro.intro
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
h : ∃ x ∈ d, f p ≤ x
⊢ ∃ y ∈ d, f p ≤ y

Tactic:
simpa only [exists_prop]

Result:
no goals

Proof state:
case a.intro.intro
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
h : ∀ (s : Set α), s.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) s → f p ≤ sSup s → ∃ x ∈ s, f p ≤ x
⊢ ∃ y ∈ d, f p ≤ y

Tactic:
specialize h d hemp hdir (le_trans (Finset.le_sup hps) hsup)

Result:
case a.intro.intro
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
h : ∃ x ∈ d, f p ≤ x
⊢ ∃ y ∈ d, f p ≤ y

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
⊢ IsCompactElement (s.sup f)

Tactic:
rw [isCompactElement_iff_le_of_directed_sSup_le]

Result:
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
⊢ ∀ (s_1 : Set α), s_1.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) s_1 → s.sup f ≤ sSup s_1 → ∃ x ∈ s_1, s.sup f ≤ x

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
⊢ ∃ x ∈ d, (Finset.image f s).sup id ≤ x

Tactic:
apply Finset.sup_le_of_le_directed d hemp hdir

Result:
case a
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
⊢ ∀ x ∈ Finset.image f s, ∃ y ∈ d, x ≤ y

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
⊢ IsCompactElement (s.sup f)

Tactic:
classical
  rw [isCompactElement_iff_le_of_directed_sSup_le]
  intro d hemp hdir hsup
  rw [← Function.id_comp f]
  rw [← Finset.sup_image]
  apply Finset.sup_le_of_le_directed d hemp hdir
  rintro x hx
  obtain ⟨p, ⟨hps, rfl⟩⟩ := Finset.mem_image.mp hx
  specialize h p hps
  rw [isCompactElement_iff_le_of_directed_sSup_le] at h
  specialize h d hemp hdir (le_trans (Finset.le_sup hps) hsup)
  simpa only [exists_prop]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
⊢ ∀ (s_1 : Set α), s_1.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) s_1 → s.sup f ≤ sSup s_1 → ∃ x ∈ s_1, s.sup f ≤ x

Tactic:
intro d hemp hdir hsup

Result:
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
⊢ ∃ x ∈ d, s.sup f ≤ x

Proof state:
case a
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
x : α
hx : x ∈ Finset.image f s
⊢ ∃ y ∈ d, x ≤ y

Tactic:
obtain ⟨p, ⟨hps, rfl⟩⟩ := Finset.mem_image.mp hx

Result:
case a.intro.intro
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
⊢ ∃ y ∈ d, f p ≤ y

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
⊢ ∃ x ∈ d, s.sup f ≤ x

Tactic:
rw [← Function.id_comp f]

Result:
α : Type u_3
β : Type u_4
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ x ∈ s, IsCompactElement (f x)
d : Set α
hemp : d.Nonempty
hdir : DirectedOn (fun x1 x2 => x1 ≤ x2) d
hsup : s.sup f ≤ sSup d
⊢ ∃ x ∈ d, s.sup (id ∘ f) ≤ x