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

refactor: Linting

Browse source
This commit is contained in:
jstoobysmith 2024-04-18 09:56:51 -04:00
parent b9119dccf1
commit 3ef2394c6b
2 changed files with 15 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

18
HepLean/AnomalyCancellation/PureU1/Basic.lean
View file

@ -47,18 +47,18 @@ def accCubeTriLinSymm {n : ℕ} : TriLinearSymm (PureU1Charges n).charges where
intro i
ring
map_add₁' S L T R := by
simp
simp only [PureU1Charges_numberCharges, ACCSystemCharges.chargesAddCommMonoid_add]
rw [← Finset.sum_add_distrib]
apply Fintype.sum_congr
intro i
ring
swap₁' S L T := by
simp
simp only [PureU1Charges_numberCharges]
apply Fintype.sum_congr
intro i
ring
swap₂' S L T := by
simp
simp only [PureU1Charges_numberCharges]
apply Fintype.sum_congr
intro i
ring
@ -68,10 +68,10 @@ lemma accCubeTriLinSymm_cast {n m : ℕ} (h : m = n)
accCubeTriLinSymm S = ∑ i : Fin m,
S.1 (Fin.cast h i) * S.2.1 (Fin.cast h i) * S.2.2 (Fin.cast h i) := by
rw [← accCubeTriLinSymm.toFun_eq_coe, accCubeTriLinSymm]
simp
simp only [PureU1Charges_numberCharges]
rw [Finset.sum_equiv (Fin.castIso h).symm.toEquiv]
intro i
simp
simp only [mem_univ, Fin.symm_castIso, RelIso.coe_fn_toEquiv, Fin.castIso_apply]
intro i
simp
@ -86,9 +86,9 @@ lemma accCube_explicit (n : ℕ) (S : (PureU1Charges n).charges) :
rw [accCube, TriLinearSymm.toCubic]
change accCubeTriLinSymm.toFun (S, S, S) = _
rw [accCubeTriLinSymm]
simp
simp only [PureU1Charges_numberCharges]
apply Finset.sum_congr
simp
simp only
ring_nf
simp
@ -149,9 +149,9 @@ lemma pureU1_anomalyFree_ext {n : ℕ} {S T : (PureU1 n.succ).LinSols}
simp at hi
rw [hi]
rw [pureU1_last, pureU1_last]
simp
simp only [neg_inj]
apply Finset.sum_congr
simp
simp only
intro j _
exact h j

13
HepLean/AnomalyCancellation/PureU1/Permutations.lean
View file

@ -53,7 +53,7 @@ open PureU1Charges in
def permCharges {n : ℕ} : Representation ℚ (permGroup n) (PureU1 n).charges where
toFun f := chargeMap f⁻¹
map_mul' f g :=by
simp
simp only [permGroup, mul_inv_rev]
apply LinearMap.ext
intro S
funext i
@ -182,7 +182,7 @@ def permTwoInj : Fin 2 ↪ Fin n where
aesop
lemma permTwoInj_fst : i ∈ Set.range ⇑(permTwoInj hij) := by
simp
simp only [Set.mem_range]
use 0
rfl
@ -191,7 +191,7 @@ lemma permTwoInj_fst_apply :
exact (Equiv.symm_apply_eq (Function.Embedding.toEquivRange (permTwoInj hij))).mpr rfl
lemma permTwoInj_snd : j ∈ Set.range ⇑(permTwoInj hij) := by
simp
simp only [Set.mem_range]
use 1
rfl
@ -239,7 +239,7 @@ def permThreeInj : Fin 3 ↪ Fin n where
aesop
lemma permThreeInj_fst : i ∈ Set.range ⇑(permThreeInj hij hjk hik) := by
simp
simp only [Set.mem_range]
use 0
rfl
@ -250,7 +250,7 @@ lemma permThreeInj_fst_apply :
lemma permThreeInj_snd : j ∈ Set.range ⇑(permThreeInj hij hjk hik) := by
simp
simp only [Set.mem_range]
use 1
rfl
@ -259,9 +259,8 @@ lemma permThreeInj_snd_apply :
⟨j, permThreeInj_snd hij hjk hik⟩ = 1 := by
exact (Equiv.symm_apply_eq (Function.Embedding.toEquivRange (permThreeInj hij hjk hik))).mpr rfl
lemma permThreeInj_thd : k ∈ Set.range ⇑(permThreeInj hij hjk hik) := by
simp
simp only [Set.mem_range]
use 2
rfl