{x ∈ S | x > 0} : set ℕ
{x ∈ s | x > 0} : finset ℕ
@set.sep.{1} nat
  (λ x,
     @gt.{1} nat nat._trans_of_decidable_linear_ordered_semiring_13 x
       (@zero.{1} nat nat._trans_of_decidable_linear_ordered_semiring_6))
  S :
  set.{1} nat
@finset.sep.{1} nat (λ a b, nat.has_decidable_eq a b)
  (λ x,
     @gt.{1} nat nat._trans_of_decidable_linear_ordered_semiring_13 x
       (@zero.{1} nat nat._trans_of_decidable_linear_ordered_semiring_6))
  (λ a, nat.decidable_lt (@zero.{1} nat nat._trans_of_decidable_linear_ordered_semiring_6) a)
  s :
  finset.{1} nat