Referencing hypothesis

Stream: maths

[Christopher Hoskin]

Given a subset s of lattice, I'm trying to define the set of supremums of finite subsets of s.

I've come up with:

import Mathlib.Data.Set.Finite

variable (α : Type _) [Lattice α] (s : Set α)

def myset := { a | ∃ F : Finset α, ↑F ⊆ s ∧ F.Nonempty ∧ a = F.sup' _ id   }

The _ produces the error don't know how to synthesize placeholder for argument 'H'.

I can't see how I should reference the hypothesis that F is non-empty in place of _?

Thanks.

Christopher

[Ruben Van de Velde]

You'd write \exists F : Finset \a, \exists H : F.Nonempty, ... a = F.sup' H id

[Yaël Dillies]

Btw, what's the context for this? I have a PR with irreducible and prime elements in an order.

[Yury G. Kudryashov]

When you write a ∧ b, propositions a and b can't depend on each other. If you need a proof of a to state b, then you have to use ∃ H : a, b H