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

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2024-12-03 09:52:11 +00:00
parent da70d65c6d
commit bd2a915e03
4 changed files with 4 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

4
HepLean/PerturbationTheory/Wick/Contract.lean
View file

@ -256,8 +256,8 @@ lemma mem_snoc' {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
(hilej : i < j) → (hb1 : ∀ r, b1 r < i) → (hb2i : ∀ r, b2 r ≠ i) → (hb2j : ∀ r, b2 r ≠ j) →
(hb1' : Fin.snoc b1 i = b1' ∘ Fin.cast hk') →
(hb2' : Fin.snoc b2 j = b2' ∘ Fin.cast hk') →
∃ (w' : WickContract str b1 b2), w = castMaps hk' hb1' hb2' (
contr i j h hilej hb1 hb2i hb2j w') := fun
∃ (w' : WickContract str b1 b2), w = castMaps hk' hb1' hb2'
(contr i j h hilej hb1 hb2i hb2j w') := fun
| string => fun hk' => by
simp at hk'
| contr i' j' h' hilej' hb1' hb2i' hb2j' w' => by