no goals
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
⊢ IsCompactElement (Finset.sup s f)
classical
  rw [isCompactElement_iff_le_of_directed_sSup_le]
  intro d hemp hdir hsup
  rw [← Function.comp.left_id 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]
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
⊢ ∀ (s_1 : Set α),
    Set.Nonempty s_1 →
      DirectedOn (fun x x_1 => x ≤ x_1) s_1 → Finset.sup s f ≤ sSup s_1 → ∃ x, x ∈ s_1 ∧ Finset.sup s f ≤ x
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
⊢ IsCompactElement (Finset.sup s f)
rw [isCompactElement_iff_le_of_directed_sSup_le]
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
⊢ ∃ x, x ∈ d ∧ Finset.sup s f ≤ x
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
⊢ ∀ (s_1 : Set α),
    Set.Nonempty s_1 →
      DirectedOn (fun x x_1 => x ≤ x_1) s_1 → Finset.sup s f ≤ sSup s_1 → ∃ x, x ∈ s_1 ∧ Finset.sup s f ≤ x
intro d hemp hdir hsup
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
⊢ ∃ x, x ∈ d ∧ Finset.sup s (id ∘ f) ≤ x
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
⊢ ∃ x, x ∈ d ∧ Finset.sup s f ≤ x
rw [← Function.comp.left_id f]
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
⊢ ∃ x, x ∈ d ∧ Finset.sup (Finset.image f s) id ≤ x
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
⊢ ∃ x, x ∈ d ∧ Finset.sup s (id ∘ f) ≤ x
rw [← Finset.sup_image]
case a
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
⊢ ∀ (x : α), x ∈ Finset.image f s → ∃ y, y ∈ d ∧ x ≤ y
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
⊢ ∃ x, x ∈ d ∧ Finset.sup (Finset.image f s) id ≤ x
apply Finset.sup_le_of_le_directed d hemp hdir
case a
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
x : α
hx : x ∈ Finset.image f s
⊢ ∃ y, y ∈ d ∧ x ≤ y
case a
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
⊢ ∀ (x : α), x ∈ Finset.image f s → ∃ y, y ∈ d ∧ x ≤ y
rintro x hx
case a.intro.intro
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
⊢ ∃ y, y ∈ d ∧ f p ≤ y
case a
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
x : α
hx : x ∈ Finset.image f s
⊢ ∃ y, y ∈ d ∧ x ≤ y
obtain ⟨p, ⟨hps, rfl⟩⟩ := Finset.mem_image.mp hx
case a.intro.intro
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
h : IsCompactElement (f p)
⊢ ∃ y, y ∈ d ∧ f p ≤ y
case a.intro.intro
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
h : ∀ (x : β), x ∈ s → IsCompactElement (f x)
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
⊢ ∃ y, y ∈ d ∧ f p ≤ y
specialize h p hps
case a.intro.intro
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
h : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → f p ≤ sSup s → ∃ x, x ∈ s ∧ f p ≤ x
⊢ ∃ y, y ∈ d ∧ f p ≤ y
case a.intro.intro
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
h : IsCompactElement (f p)
⊢ ∃ y, y ∈ d ∧ f p ≤ y
rw [isCompactElement_iff_le_of_directed_sSup_le] at h
case a.intro.intro
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
h : ∃ x, x ∈ d ∧ f p ≤ x
⊢ ∃ y, y ∈ d ∧ f p ≤ y
case a.intro.intro
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
h : ∀ (s : Set α), Set.Nonempty s → DirectedOn (fun x x_1 => x ≤ x_1) s → f p ≤ sSup s → ∃ x, x ∈ s ∧ f p ≤ x
⊢ ∃ y, y ∈ d ∧ f p ≤ y
specialize h d hemp hdir (le_trans (Finset.le_sup hps) hsup)
no goals
case a.intro.intro
ι : Sort ?u.14463
α✝ : Type ?u.14466
inst✝¹ : CompleteLattice α✝
f✝ : ι → α✝
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : β → α
s : Finset β
d : Set α
hemp : Set.Nonempty d
hdir : DirectedOn (fun x x_1 => x ≤ x_1) d
hsup : Finset.sup s f ≤ sSup d
p : β
hps : p ∈ s
hx : f p ∈ Finset.image f s
h : ∃ x, x ∈ d ∧ f p ≤ x
⊢ ∃ y, y ∈ d ∧ f p ≤ y
simpa only [exists_prop]