From 7e29b5470da12b5ddae8e3d7310c502423c8af3c Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 28 Oct 2024 08:22:56 +0000
Subject: [PATCH] fix: proof

---
 HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean b/HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean
index fce7080..d38ce9d 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean
@@ -60,6 +60,7 @@ lemma leftContrJ_succAbove_leftContrI : (q.leftContrI n1).succAbove (q.leftContr
     rename_i h1 h2
     rw [Fin.lt_def] at h1 h2
     simp_all
+  omega
 
 lemma succAbove_leftContrJ_leftContrI_castAdd (x : Fin n) :
     (q.leftContrI n1).succAbove ((q.leftContrJ n1).succAbove (Fin.castAdd n1 x)) =