From 82c682d3850d2d48131fbed3dc58bec476709b64 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 12 Mar 2022 11:12:56 +0100
Subject: [PATCH] chore: remove redundant proof

---
 src/Init/Data/Array/Basic.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 4151e97e54..758d95e62c 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -659,7 +659,6 @@ def eraseIdxAux (i : Nat) (a : Array α) : Array α :=
     let idx  : Fin a.size := ⟨i, h⟩;
     let idx1 : Fin a.size := ⟨i - 1, by exact Nat.lt_of_le_of_lt (Nat.pred_le i) h⟩;
     let a' := a.swap idx idx1
-    have : a'.size - (i+1) < a.size - i := by rw [size_swap]; apply Nat.sub_succ_lt_self; assumption
     eraseIdxAux (i+1) a'
   else
     a.pop