a `piFinCastSum` generalizing `piFinCastSucc`?

Stream: mathlib4

[Shaopeng]

In Mathlib.Logic.Equiv.Fin we currently have

def Equiv.piFinCastSucc (n : ℕ) (β : Type u) : (Fin (n + 1) → β) ≃ β × (Fin n → β) :=
  Equiv.piFinSuccAbove (fun _ => β) (.last _)

In a project I would like to use a slightly more general version of this: Equiv.piFinCastSum (n : ℕ)(m : ℕ) (β : Type u) : (Fin (n + m) → β) ≃ (Fin m → β) × (Fin n → β) . Has this been documented somewhere or do I need to write a short proof myself?

Also any advice about finding proofs in similar situation faster in Mathlib (in addition to doing Search in this repository which sometimes seems inefficient) would be greatly appreciated!

Thanks a lot in advance for your help.

[Eric Wieser]

This should follow from docs#finSumFinEquiv and docs#Equiv.sumArrowEquivProdArrow

[Eric Wieser]

docs#Fin.append is one direction of this, so maybe we should have Fin.appendEquiv to match

[Shaopeng]

Eric Wieser said:

This should follow from docs#finSumFinEquiv and docs#Equiv.sumArrowEquivProdArrow

Thanks a lot for this, Eric! Really appreciate it.