Error with Set.BijOn.finsetCard_eq

Stream: new members

[Nathan]

import Mathlib

example : 1 = 1 :=
  have := Set.BijOn.finsetCard_eq
  sorry

I can't seem to load this theorem. I get this error:

invalid field notation, type is not of the form (C ...) where C is a constant
Set.BijOn
has type
(?m.132 → ?m.133) → Set ?m.132 → Set ?m.133 → Prop

[Ruben Van de Velde]

That's not the error I get:

MathlibDemo.lean:4:7
MathlibDemo.lean:4:7

failed to infer `have` declaration type

MathlibDemo.lean:4:10

don't know how to synthesize implicit argument `t`
  @Set.BijOn.finsetCard_eq ?m.8 ?m.9 ?m.10 ?m.11
context:
⊢ Finset ?m.9

MathlibDemo.lean:4:10

don't know how to synthesize implicit argument `t`
  @Set.BijOn.finsetCard_eq ?m.8 ?m.9 ?m.10 ?m.11
context:
⊢ Finset ?m.9

MathlibDemo.lean:4:10

don't know how to synthesize implicit argument `s`
  @Set.BijOn.finsetCard_eq ?m.8 ?m.9 ?m.10 ?m.11
context:
⊢ Finset ?m.8

MathlibDemo.lean:4:10

don't know how to synthesize implicit argument `s`
  @Set.BijOn.finsetCard_eq ?m.8 ?m.9 ?m.10 ?m.11
context:
⊢ Finset ?m.8

MathlibDemo.lean:4:10

don't know how to synthesize implicit argument `β`
  @Set.BijOn.finsetCard_eq ?m.8 ?m.9 ?m.10 ?m.11
context:
⊢ Type ?u.126

MathlibDemo.lean:4:10

don't know how to synthesize implicit argument `β`
  @Set.BijOn.finsetCard_eq ?m.8 ?m.9 ?m.10 ?m.11
context:
⊢ Type ?u.126

MathlibDemo.lean:4:10

don't know how to synthesize implicit argument `α`
  @Set.BijOn.finsetCard_eq ?m.8 ?m.9 ?m.10 ?m.11
context:
⊢ Type ?u.127

don't know how to synthesize implicit argument `α`
  @Set.BijOn.finsetCard_eq ?m.8 ?m.9 ?m.10 ?m.11
context:
⊢ Type ?u.127

[Kenny Lau]

in other words your mathlib is outdated

[Nathan]

Thank you! I hadn't set up the project correctly. Found the button in VSCode to setup a mathlib project.