More Lean typing question

Stream: new members

[Ching-Tsun Chou]

I have the following code:

noncomputable section

variable (α : Type*) [Fintype α] [DecidableEq α]

abbrev PreNumbering := α → Fin (card α + 1)

def initSeg (n : ℕ) : Finset (Fin (card α + 1)) := { i | i < n }

def setNumbering (s : Finset α) : Finset (PreNumbering α) :=
  { f | BijOn f s (initSeg α s.card) ∧ ∀ a ∈ sᶜ, (f a : ℕ) = 0 }

Now, if I substitute the definition of initSeg directly into its use:

def setNumbering (s : Finset α) : Finset (PreNumbering α) :=
  { f | BijOn f s { i | i < s.card } ∧ ∀ a ∈ sᶜ, (f a : ℕ) = 0 }

I get the error:

failed to synthesize
  DecidablePred fun f ↦ BijOn f ↑s {i | i < ↑s.card} ∧ ∀ a ∈ sᶜ, ↑(f a) = 0

The only way to get rid of the error I can think of is to explicitly type { i | i < s.card }:

def setNumbering (s : Finset α) : Finset (PreNumbering α) :=
  { f | BijOn f s ({ i | i < s.card } : Finset (Fin (card α + 1))) ∧ ∀ a ∈ sᶜ, (f a : ℕ) = 0 }

But then the expression becomes so ugly that I may as well keep initSeg. Is there any more elegant solution?

[Ching-Tsun Chou]

Another annoying thing is that if I use def instead abbrev in the definition of PreNumbering, then Lean fails to synthesize Fintype (PreNumbering α) in the definition of setNumbering and I had to explicitly prove an instance theorem.