From b4588e8a058b89212fa5d4c6e5def6f119ef030c Mon Sep 17 00:00:00 2001
From: Nathaneal <nateabr@gmail.com>
Date: Wed, 30 Sep 2026 23:14:57 +0400
Subject: [PATCH] chore: remove unused simp arguments in SuccSuccAbove

---
 Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean
index 7b4e84389..f7de17356 100644
--- a/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean
+++ b/Physlib/Relativity/Tensors/Contraction/SuccSuccAbove.lean
@@ -281,7 +281,7 @@ lemma succSuccAbove_comm_natAdd {n n1 : ℕ}
     (i j : Fin (n + 1 + 1)) (m : Fin n) :
     succSuccAbove (n := n1 + n) (Fin.natAdd n1 i) (Fin.natAdd n1 j) (Fin.natAdd n1 m)
     = Fin.natAdd (n1) (succSuccAbove i j m) := by
-  simp only [succSuccAbove, val_natAdd, add_lt_add_iff_left, add_le_add_iff_left, Fin.ext_iff]
+  simp only [succSuccAbove, val_natAdd, Fin.ext_iff]
   grind
 
 /-!