Rewrite type of expression

Stream: new members

[hakanaras]

Is there a quick and easy way to use an expression of type A where an expression of type B is expected, if (A = B) can be shown easily, e.g. by grind? For example can I do this without introducing a separate lemma1 here:

def lemma1 {a s : Nat} : List.Vector α (a + (s + 0)).succ -> List.Vector α (a + 1 + 0 + s)
  | ⟨ l, len ⟩ => ⟨ l, by grind only ⟩

/-- Applies the stack permutation to the given input and stack vectors. -/
def apply {α : Type} {i s : Nat} :
  (perm : StackPermutation i s) -> (input : V α i) -> (stack : V α s) -> V α (i + s)
    | .nil, _, _ => V.nil
    | .skip 0 rest, ⟨ ih :: it, i ⟩, ⟨ ss, s ⟩ => lemma1 $ V.cons ih $ apply rest ⟨ it, by grind only [List.length_cons] ⟩ ⟨ ss, s ⟩
    | .skip (Nat.succ n) rest, ⟨ i :: is, _ ⟩, ⟨ ss, _ ⟩ => sorry -- apply (.skip n rest) ⟨ is, _ ⟩ ⟨ i :: ss, _ ⟩
    | .pop rest, is, ⟨ s :: ss, _ ⟩ => V.cons s $ apply rest is ⟨ ss, by grind only [List.length_cons] ⟩

Also I have a feeling I'm making apply way more complicated than it needs to be. I'd be thankful for any tips on simplifying it.

I have gone through much of the language reference and other parts of the documentation, and I'm still continuing to do so, but I can't easily find answers to questions like this.

[Kenny Lau]

without reading your example, it's the various cast functions (whose precise implementation depends on what A and B are), such as docs#Fin.cast that casts Fin m to Fin n

[hakanaras]

Thanks, regular cast was exactly what I needed

[Kenny Lau]

the reason why various cast functions are defined (which are all equal to cast) is because sometimes you want to carry certain structures

[hakanaras]

I understand, I checked if there is one for List.Vector from mathlib4 but there isn't