DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix: proof

Browse source
This commit is contained in:
jstoobysmith 2024-10-28 08:22:56 +00:00
parent 51c56d3e07
commit 7e29b5470d
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
HepLean/Tensors/Tree/NodeIdentities/ProdContr.lean
View file

@ -60,6 +60,7 @@ lemma leftContrJ_succAbove_leftContrI : (q.leftContrI n1).succAbove (q.leftContr
rename_i h1 h2 rename_i h1 h2
rw [Fin.lt_def] at h1 h2 rw [Fin.lt_def] at h1 h2
simp_all simp_all
omega
lemma succAbove_leftContrJ_leftContrI_castAdd (x : Fin n) : lemma succAbove_leftContrJ_leftContrI_castAdd (x : Fin n) :
(q.leftContrI n1).succAbove ((q.leftContrJ n1).succAbove (Fin.castAdd n1 x)) = (q.leftContrI n1).succAbove ((q.leftContrJ n1).succAbove (Fin.castAdd n1 x)) =