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

refactor: golf

Browse source
This commit is contained in:
jstoobysmith 2024-08-30 09:10:39 -04:00
parent 0c03778a76
commit d39c6c3e28
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
HepLean/SpaceTime/LorentzTensor/IndexNotation/ColorIndexList/Append.lean
View file

@ -119,10 +119,9 @@ lemma bool_iff (l l2 : IndexList 𝓒.Color) :
lemma iff_bool (l l2 : ColorIndexList 𝓒) : AppendCond l l2 ↔ bool l.toIndexList l2.toIndexList := by
rw [AppendCond]
simp [bool]
simp only [bool, ite_not, Bool.if_false_right, Bool.and_eq_true, decide_eq_true_eq]
rw [ColorCond.iff_bool]
simp
exact fun _ => Eq.to_iff rfl
exact Eq.to_iff rfl
lemma countId_contr_fst_eq_zero_mem_snd (h : AppendCond l l2) {I : Index 𝓒.Color}
(hI : I ∈ l2.val) : l.contr.countId I = 0 ↔ l.countId I = 0 := by