[GOAL]
ι α : Type v
U : ι → α
inst✝ : CompleteLattice α
s : Cocone (diagram U)
⊢ (cocone U).pt ≤ s.pt
[PROOFSTEP]
apply CompleteSemilatticeSup.sSup_le
[GOAL]
case a
ι α : Type v
U : ι → α
inst✝ : CompleteLattice α
s : Cocone (diagram U)
⊢ ∀ (b : α), b ∈ Set.range U → b ≤ s.pt
[PROOFSTEP]
rintro _ ⟨j, rfl⟩
[GOAL]
case a.intro
ι α : Type v
U : ι → α
inst✝ : CompleteLattice α
s : Cocone (diagram U)
j : ι
⊢ U j ≤ s.pt
[PROOFSTEP]
exact (s.ι.app (single j)).le
