English
If v : Fin (m+n) → γ i, then addCases (fun i ↦ v (castAdd n i)) (fun j ↦ v (natAdd m j)) = v.
Русский
Пусть v : Fin (m+n) → γ, тогда addCases (castAdd n) и natAdd дают обратно v.
LaTeX
$$$\\mathrm{addCases}(\\lambda i. v(\\mathrm{castAdd}\\, n\\ i))(\\lambda j. v(\\mathrm{natAdd}\\, m\\ j)) = v.$$$
Lean4
theorem append_injective_iff {xs : Fin m → α} {ys : Fin n → α} :
Function.Injective (Fin.append xs ys) ↔ Function.Injective xs ∧ Function.Injective ys ∧ ∀ i j, xs i ≠ ys j := by
-- TODO: move things around so we can just import this.
-- We inline it because it's still shorter than proving from scratch.
let finSumFinEquiv : Fin m ⊕ Fin n ≃ Fin (m + n) :=
{ toFun := Sum.elim (Fin.castAdd n) (Fin.natAdd m)
invFun i := @Fin.addCases m n (fun _ => Fin m ⊕ Fin n) Sum.inl Sum.inr i
left_inv x := by rcases x with y | y <;> simp
right_inv x := by refine Fin.addCases (fun i => ?_) (fun i => ?_) x <;> simp }
rw [← Sum.elim_injective, ← append_comp_sumElim, ← finSumFinEquiv.injective_comp, Equiv.coe_fn_mk]
