Failed to synthesize DecidablePred

Stream: mathlib4

[Michael Lee]

I've written a proof of Newton's identities here and am trying to figure out how to rewrite the condition for the Finset pairs that's in bijection to the set of monomials on the LHS of the identity. Here's a minimal working example that shows the issue:

import Mathlib.Algebra.Algebra.Subalgebra.Basic
import Mathlib.Data.Finset.Card
import Mathlib.Data.Fintype.Basic

open Finset

variable (σ : Type _) [Fintype σ] [DecidableEq σ] (R : Type _) [CommRing R]

def pairs (σ : Type _) [Fintype σ] (k : ℕ) : Finset (Finset σ × σ) :=
  Finset.univ.filter (fun t => card t.fst ≤ k ∧ ((card t.fst = k) → t.snd ∈ t.fst))

I get an error failed to synthesize instance DecidablePred fun t ↦ card t.fst ≤ k ∧ (card t.fst = k → t.snd ∈ t.fst) on Finset.univ.filter, but this predicate does seem like it should be decidable constructively. Does anyone have a suggestion as to how to resolve this? Thanks!

[Eric Wieser]

You're missing [DecidableEq σ]

[Eric Wieser]

The one on the variables line is useless because you discard σ and replace it with a new σ in the def

[Eric Wieser]

(as an aside, there's something pretty wonky with the pretty-printer if you run #eval pairs (Fin 3) 3)

[Michael Lee]

Ah shoot, you're completely right. Dumb typo on my part. Thanks so much!