Fixup after leanprover/lean4#10627

Author: nomeata

Batteries/Data/Fin/Lemmas.lean

@@ -11,16 +11,6 @@ namespace Fin
 
 attribute [norm_cast] val_last
 
--- Forward port from lean4#10627
-@[simp] theorem forall_fin_zero {P : Fin 0 → Prop} : (∀ i, P i) ↔ True := by
-  rw [iff_true]; intro ⟨_, _⟩; contradiction
-
--- Forward port from lean4#10627
-@[simp] theorem exists_fin_zero {P : Fin 0 → Prop} : (∃ i, P i) ↔ False := by simp
-
--- Forward port from lean4#10627
-attribute [simp] exists_fin_one forall_fin_one exists_fin_two forall_fin_two
-
 /-! ### foldl/foldr -/
 
 theorem foldl_assoc {op : α → α → α} [ha : Std.Associative op] {f : Fin n → α} {a₁ a₂} :