Why have the cast operators disappeared?

Stream: new members

[Ching-Tsun Chou]

I have the following code:

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

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

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

example (s : Finset α) (a : α) (h_as : a ∈ s) (f : PreNumbering α) (h1 : BijOn f (↑s \ {a}) (↑(initSeg α #s) \ {f a})) :
    BijOn f (↑s \ {a}) ↑(initSeg α (s.card - 1)) := by
  have h2 : ↑(initSeg α #s) \ {f a} = ↑(initSeg α (#s - 1)) := by
    sorry
-- At this point we have the following, where ↑ has disappeared!
-- h2 : initSeg α #s \ {f a} = initSeg α (#s - 1)
-- Consequently the following rewrite fails.
--  rw [h2] at h1
  sorry

As indicated in the comments, the cast operators disappeared from both LHS and RHS of h2, even though I explicitly spelled them out. Consequently, the rewrite using h2 fails. Why is going on?

[Notification Bot]

This topic was moved here from #new members > Why have the cast operators disappear? by Ching-Tsun Chou.

[Yaël Dillies]

Ching-Tsun Chou said:

the cast operators disappeared from both LHS and RHS of h2, even though I explicitly spelled them out.

That's because cast operators are polymorphic and try to cast as little as possible. Here there's the option to not cast at all, so they do just that

[Yaël Dillies]

have h2 : (initSeg α #s : Set α) \ {f a} = initSeg α (#s - 1) or have h2 : (initSeg α #s).toSet \ {f a} = initSeg α (#s - 1) will work

[Ching-Tsun Chou]

Thanks! That works. I have to say working with the Fin n types is truly a pain.