theorem Regex.Data.SparseSet.Bijection.surj_of_inj {n : Nat} (f : Fin n → Fin n) (h : Function.Injective f) : Function.Surjective f