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-08-26 10:11:49 -04:00
parent 201ae42db8
commit 4f9b572274
3 changed files with 8 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean
View file

@ -486,7 +486,7 @@ lemma countId_neq_zero_mem (I : Index X) (h : l.countId I ≠ 0) :
simp only [List.mem_filter, decide_eq_true_eq] at hI'
exact ⟨I', hI'⟩
lemma countId_mem (I : Index X) (hI : I ∈ l.val ) : l.countId I ≠ 0 := by
lemma countId_mem (I : Index X) (hI : I ∈ l.val) : l.countId I ≠ 0 := by
rw [countId_eq_length_filter]
by_contra hn
rw [List.length_eq_zero] at hn

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

@ -112,8 +112,8 @@ lemma contr_left (h : AppendCond l l2) : AppendCond l.contr l2 := by
apply ColorCond.countColorCond_of_filter_eq (l.toIndexList ++ l2.toIndexList) _ _
· have h2 := h.2
rw [ColorCond.iff_countColorCond_all] at h2
· simp only [append_val, countId_append, List.all_append, Bool.and_eq_true, List.all_eq_true,
decide_eq_true_eq] at h2
· simp only [append_val, countId_append, List.all_append, Bool.and_eq_true,
List.all_eq_true, decide_eq_true_eq] at h2
have hn := h2.1 I (List.mem_of_mem_filter hI)
have hc : l.countId I + l2.countId I = 2 := by
rw [contr, countId_contrIndexList_eq_one_iff_countId_eq_one] at hIC1
@ -138,8 +138,8 @@ lemma contr_left (h : AppendCond l l2) : AppendCond l.contr l2 := by
apply ColorCond.countColorCond_of_filter_eq (l.toIndexList ++ l2.toIndexList) _ _
· have h2 := h.2
rw [ColorCond.iff_countColorCond_all] at h2
· simp only [append_val, countId_append, List.all_append, Bool.and_eq_true, List.all_eq_true,
decide_eq_true_eq] at h2
· simp only [append_val, countId_append, List.all_append, Bool.and_eq_true,
List.all_eq_true, decide_eq_true_eq] at h2
refine h2.2 I hI1 ?_
rw [contr, countId_contrIndexList_eq_one_iff_countId_eq_one] at hIC1
omega
@ -152,7 +152,7 @@ lemma contr_left (h : AppendCond l l2) : AppendCond l.contr l2 := by
rw [filter_id_of_countId_eq_one_mem l.contr hI' hIC1]
simp [contr, contrIndexList] at hI'
exact filter_id_of_countId_eq_one_mem l hI'.1 hI'.2
· have hICt : l2.countId I = 2 := by
· have hICt : l2.countId I = 2 := by
omega
apply ColorCond.countColorCond_of_filter_eq l2 _ _
· have hl2C := l2.dual_color
@ -207,7 +207,7 @@ lemma countId_contr_fst_eq_zero_mem_snd (h : AppendCond l l2) {I : Index 𝓒.Co
rw [withUniqueDual_eq_withDual_iff_countId_leq_two'] at h1
have h1I := h1 I
simp at h1I
have h2 : l2.countId I ≠ 0 := countId_mem l2.toIndexList I hI
have h2 : l2.countId I ≠ 0 := countId_mem l2.toIndexList I hI
omega
· simp [h']

3
HepLean/SpaceTime/LorentzTensor/IndexNotation/OnlyUniqueDuals.lean
View file

@ -168,7 +168,6 @@ lemma withUniqueDual_eq_withDual_iff_countId_leq_two' :
rw [hI']
exact h ⟨List.indexOf I' l.val, hi⟩
lemma withUniqueDual_eq_withDual_countId_cases (h : l.withUniqueDual = l.withDual)
(i : Fin l.length) : l.countId (l.val.get i) = 0 ∨
l.countId (l.val.get i) = 1 ∨ l.countId (l.val.get i) = 2 := by
@ -596,7 +595,7 @@ lemma append_withDual_eq_withUniqueDual_swap :
rw [withUniqueDualInOther_eq_withDualInOther_append_of_symm]
lemma append_withDual_eq_withUniqueDual_contr_left
(h1 : (l ++ l2).withUniqueDual = (l ++ l2).withDual):
(h1 : (l ++ l2).withUniqueDual = (l ++ l2).withDual) :
(l.contrIndexList ++ l2).withUniqueDual = (l.contrIndexList ++ l2).withDual := by
rw [withUniqueDual_eq_withDual_iff_all_countId_le_two] at h1 ⊢
simp only [append_val, countId_append, List.all_append, Bool.and_eq_true, List.all_eq_true,