From ecb2c7778c3cf4517105a30ae33365cd1f0fddb2 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 22 Oct 2024 10:47:37 +0000
Subject: [PATCH] refactor: Lint

---
 HepLean/Tensors/ComplexLorentz/Lemmas.lean |  7 +++----
 HepLean/Tensors/Tree/Basic.lean            | 18 ++++++++++++------
 HepLean/Tensors/Tree/Elab.lean             |  1 +
 3 files changed, 16 insertions(+), 10 deletions(-)

diff --git a/HepLean/Tensors/ComplexLorentz/Lemmas.lean b/HepLean/Tensors/ComplexLorentz/Lemmas.lean
index b793a7d..ec846c7 100644
--- a/HepLean/Tensors/ComplexLorentz/Lemmas.lean
+++ b/HepLean/Tensors/ComplexLorentz/Lemmas.lean
@@ -90,8 +90,8 @@ lemma coMetric_symm : {Lorentz.coMetric | μ ν = Lorentz.coMetric | ν μ}ᵀ :
   rw [coMetric_expand]
   simp only [TensorSpecies.F, Nat.succ_eq_add_one, Nat.reduceAdd, Functor.id_obj, Fin.isValue,
     map_sub]
-  simp only [coCoBasis, Nat.reduceAdd, Nat.succ_eq_add_one, OverColor.mk_hom, Functor.id_obj, Fin.isValue,
-      Lorentz.complexCoBasisFin4, Basis.coe_reindex, Function.comp_apply]
+  simp only [coCoBasis, Nat.succ_eq_add_one, Nat.reduceAdd, Functor.id_obj, OverColor.mk_hom,
+    Lorentz.complexCoBasisFin4, Fin.isValue, Basis.coe_reindex, Function.comp_apply]
   congr 1
   congr 1
   congr 1
@@ -127,8 +127,7 @@ lemma contr_rank_2_symm {T1 : (Lorentz.complexContr ⊗ Lorentz.complexContr).V}
     rw [perm_perm]
     rw [perm_eq_id]
     · rfl
-    · apply OverColor.Hom.ext
-      rfl
+    · rfl
   · apply OverColor.Hom.ext
     ext x
     exact Fin.elim0 x
diff --git a/HepLean/Tensors/Tree/Basic.lean b/HepLean/Tensors/Tree/Basic.lean
index c8281c2..2c2927f 100644
--- a/HepLean/Tensors/Tree/Basic.lean
+++ b/HepLean/Tensors/Tree/Basic.lean
@@ -246,12 +246,15 @@ def contrMap {n : ℕ} (c : Fin n.succ.succ → S.C)
 /-- Casts an element of the monoidal unit of `Rep S.k S.G` to the field `S.k`. -/
 def castToField (v : (↑((𝟙_ (Discrete S.C ⥤ Rep S.k S.G)).obj { as := c }).V)) : S.k := v
 
+/-- Casts an element of `(S.F.obj (OverColor.mk c)).V` for `c` a map from `Fin 0` to an
+  element of the field. -/
 def castFin0ToField {c : Fin 0 → S.C} : (S.F.obj (OverColor.mk c)).V →ₗ[S.k] S.k :=
   (PiTensorProduct.isEmptyEquiv (Fin 0)).toLinearMap
 
-lemma castFin0ToField_tprod {c : Fin 0 → S.C} (x : (i : Fin 0) → S.FDiscrete.obj (Discrete.mk (c i))) :
+lemma castFin0ToField_tprod {c : Fin 0 → S.C}
+    (x : (i : Fin 0) → S.FDiscrete.obj (Discrete.mk (c i))) :
     castFin0ToField S (PiTensorProduct.tprod S.k x) = 1 := by
-  simp [castFin0ToField]
+  simp only [castFin0ToField, mk_hom, Functor.id_obj, LinearEquiv.coe_coe]
   erw [PiTensorProduct.isEmptyEquiv_apply_tprod]
 
 lemma contrMap_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
@@ -383,7 +386,7 @@ def evalIso {n : ℕ} (c : Fin n.succ → S.C)
   (S.F.mapIso (OverColor.mkSum (c ∘ (HepLean.Fin.finExtractOne i).symm))).trans <|
   (S.F.μIso _ _).symm.trans <|
   tensorIso
-    ((S.F.mapIso (OverColor.mkIso (by ext x; fin_cases x; simp))).trans
+    ((S.F.mapIso (OverColor.mkIso (by ext x; fin_cases x; rfl))).trans
     (OverColor.forgetLiftApp S.FDiscrete (c i))) (S.F.mapIso (OverColor.mkIso (by ext x; simp)))
 
 lemma evalIso_tprod {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ)
@@ -443,7 +446,9 @@ lemma evalIso_tprod {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ)
       rfl
   · apply congrArg
     funext k
-    simp [lift.discreteFunctorMapEqIso]
+    simp only [lift.discreteFunctorMapEqIso, Functor.mapIso_hom, eqToIso.hom, Functor.mapIso_inv,
+      eqToIso.inv, eqToIso_refl, Functor.mapIso_refl, Iso.refl_hom, Action.id_hom, Iso.refl_inv,
+      LinearEquiv.ofLinear_apply]
     change (S.FDiscrete.map (eqToHom _)).hom
       (x ((HepLean.Fin.finExtractOne i).symm ((Sum.inr k)))) = _
     have h1' {a b : Fin n.succ} (h : a = b) :
@@ -603,6 +608,7 @@ def tensor : ∀ {n : ℕ} {c : Fin n → S.C}, TensorTree S c → S.F.obj (Over
   | contr i j h t => (S.contrMap _ i j h).hom t.tensor
   | eval i e t => (S.evalMap i (Fin.ofNat' e Fin.size_pos')) t.tensor
 
+/-- Takes a tensor tree based on `Fin 0`, into the field `S.k`. -/
 def field {c : Fin 0 → S.C} (t : TensorTree S c) : S.k := S.castFin0ToField t.tensor
 
 /-!
@@ -638,8 +644,8 @@ lemma contr_tensor {n : ℕ} {c : Fin n.succ.succ → S.C} {i : Fin n.succ.succ}
 
 lemma neg_tensor (t : TensorTree S c) : (neg t).tensor = - t.tensor := rfl
 
-lemma eval_tensor {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : ℕ)
-    (t : TensorTree S c) : (eval i e t).tensor = (S.evalMap i (Fin.ofNat' e Fin.size_pos')) t.tensor := rfl
+lemma eval_tensor {n : ℕ} {c : Fin n.succ → S.C} (i : Fin n.succ) (e : ℕ) (t : TensorTree S c) :
+    (eval i e t).tensor = (S.evalMap i (Fin.ofNat' e Fin.size_pos')) t.tensor := rfl
 
 /-!
 
diff --git a/HepLean/Tensors/Tree/Elab.lean b/HepLean/Tensors/Tree/Elab.lean
index e499fea..2f00a41 100644
--- a/HepLean/Tensors/Tree/Elab.lean
+++ b/HepLean/Tensors/Tree/Elab.lean
@@ -176,6 +176,7 @@ def stringToTerm (str : String) : TermElabM Term := do
     match stx with
     | `(term| $e) => return e
 
+/-- Specific types of tensors which appear which we want to elaborate in specific ways. -/
 def specialTypes : List (String × (Term → Term)) := [
   ("CoeSort.coe Lorentz.complexCo", fun T =>
     Syntax.mkApp (mkIdent ``TensorTree.vecNodeE) #[mkIdent ``Fermion.complexLorentzTensor,