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
 
 /-!