casting a function

Stream: Is there code for X?

[Jovan Gerbscheid]

Does the following lemma exist? Does it even hold?

theorem cast_apply {α : Type u} {β β' : Type v} (f : α → β) (h : β = β') (a : α) :
    cast h (f a) = (cast (h ▸ rfl) f : α → β') a

I ended up with a goal that could be closed by this lemma when trying to prove something.

[Kim Morrison]

The rule of thumb with such questions is: if by cases h; rfl works, then it's true, otherwise not!

[Jovan Gerbscheid]

Ah, thanks, this proved it!

It turned out I needed a more complicated version, which is also proved in the same way:

theorem cast_apply {α α' : Type u} {β β' : Type v} (f : α → β) (h : β = β') (a : α) (a' : α') (h' : HEq a a') :
    cast h (f a) = (cast (by cases h; cases h'; rfl) f : α' → β') a'

Is there also a nice way to prove this kind of goal when the proof in the cast is some complicated expression? Proving this very specific lemma for one use case is a bit awkward.

[Kim Morrison]

You could try generalize on the complicate expression, to make it a hypothesis you can then call cases on.

[Jovan Gerbscheid]

The complicated expression was generated by a tactic, so not really something I'd be able to explicitly write down (something similar to Fin (n+1) and Fin (1+n) being equal by ring_nf). When I managed to generalize it, the cases tactic failed. In the end I had to rewrite my statement in order to avoid a cast altogether.

I think it could be useful to have a tactic that can solve an equality goal where the terms themselves are exactly the same, but they involve some different casts.