theorem Fin.cast_bijective {k l : ℕ} (h : k = l) : Function.Bijective (Fin.cast h)

theorem Fin.cast_surjective {k l : ℕ} (h : k = l) : Function.Surjective (Fin.cast h)

theorem Fin.forall_fin_three {p : Fin 3 → Prop} : (∀ (i : Fin 3), p i) ↔ p 0 ∧ p 1 ∧ p 2