From 755476c7b1990665ff6afd418668fd98810c2691 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 3 Feb 2025 11:54:08 +0000
Subject: [PATCH] refactor: some min imports

---
 .../FieldOpFreeAlgebra/NormTimeOrder.lean      |  2 +-
 .../FeynmanDiagrams/Basic.lean                 |  2 +-
 .../Tensors/TensorSpecies/MetricTensor.lean    | 18 +++++++-----------
 HepLean/Tensors/TensorSpecies/Pure.lean        |  3 +--
 HepLean/Tensors/Tree/NodeIdentities/Assoc.lean |  4 ----
 5 files changed, 10 insertions(+), 19 deletions(-)

diff --git a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/NormTimeOrder.lean b/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/NormTimeOrder.lean
index bce2b3a..8343080 100644
--- a/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/NormTimeOrder.lean
+++ b/HepLean/PerturbationTheory/Algebras/FieldOpFreeAlgebra/NormTimeOrder.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.PerturbationTheory.FieldSpecification.TimeOrder
-import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.SuperCommute
+import HepLean.PerturbationTheory.Algebras.FieldOpFreeAlgebra.Basic
 import HepLean.PerturbationTheory.Koszul.KoszulSign
 /-!
 
diff --git a/HepLean/PerturbationTheory/FeynmanDiagrams/Basic.lean b/HepLean/PerturbationTheory/FeynmanDiagrams/Basic.lean
index 910caad..ddf4c12 100644
--- a/HepLean/PerturbationTheory/FeynmanDiagrams/Basic.lean
+++ b/HepLean/PerturbationTheory/FeynmanDiagrams/Basic.lean
@@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import Mathlib.Tactic.FinCases
 import Mathlib.CategoryTheory.Comma.Over
-import Mathlib.CategoryTheory.Limits.Shapes.Terminal
+import Mathlib.CategoryTheory.IsomorphismClasses
 import Mathlib.Data.Fintype.Perm
 import Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting
 /-!
diff --git a/HepLean/Tensors/TensorSpecies/MetricTensor.lean b/HepLean/Tensors/TensorSpecies/MetricTensor.lean
index 12adca0..c2b300f 100644
--- a/HepLean/Tensors/TensorSpecies/MetricTensor.lean
+++ b/HepLean/Tensors/TensorSpecies/MetricTensor.lean
@@ -102,18 +102,14 @@ lemma metricTensor_contr_dual_metricTensor_outer_eq_unit (c : S.C) :
   apply perm_congr _ rfl
   apply OverColor.Hom.fin_ext
   intro i
-  simp only [Functor.id_obj, mk_hom, Function.comp_apply, Equiv.refl_symm, Equiv.coe_refl, id_eq,
-    Fin.zero_eta, Matrix.cons_val_zero, List.pmap.eq_1, ContrPair.contrSwapHom,
+  simp only [Function.comp_apply, Equiv.refl_symm, Equiv.coe_refl, id_eq, ContrPair.contrSwapHom,
     extractOne_homToEquiv, Category.assoc, Hom.hom_comp, Over.comp_left, equivToHomEq_hom_left,
-    Equiv.toFun_as_coe, types_comp_apply, finMapToEquiv_apply, mkIso_hom_hom_left_apply]
-  rw [extractTwo_hom_left_apply]
-  simp only [mk_left, braidPerm_toEquiv, Equiv.symm_trans_apply, Equiv.symm_symm,
-    Equiv.sumComm_symm, Equiv.sumComm_apply, finExtractOnePerm_symm_apply, Equiv.trans_apply,
-    Equiv.symm_apply_apply, Sum.swap_swap, Equiv.apply_symm_apply, finExtractOne_symm_inr_apply,
-    Fin.zero_succAbove, List.pmap.eq_2, Fin.mk_one, List.pmap.eq_1, Matrix.cons_val_one,
-    Matrix.head_cons, extractTwo_hom_left_apply, permProdRight_toEquiv, equivToHomEq_toEquiv,
-    Equiv.sumCongr_refl, Equiv.refl_trans, Equiv.symm_trans_self, Equiv.refl_symm, Equiv.refl_apply,
-    predAboveI_succAbove, finExtractOnePerm_apply]
+    types_comp_apply, mkIso_hom_hom_left_apply]
+  conv_lhs =>
+    right
+    rw [extractTwo_hom_left_apply]
+  simp only [mk_left, braidPerm_toEquiv, permProdRight_toEquiv, equivToHomEq_toEquiv,
+    finExtractOnePerm_apply, finExtractOne_symm_inr_apply, extractTwo_hom_left_apply]
   fin_cases i
   · decide
   · decide
diff --git a/HepLean/Tensors/TensorSpecies/Pure.lean b/HepLean/Tensors/TensorSpecies/Pure.lean
index e8ee183..7f63ce9 100644
--- a/HepLean/Tensors/TensorSpecies/Pure.lean
+++ b/HepLean/Tensors/TensorSpecies/Pure.lean
@@ -3,7 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.Tensors.TensorSpecies.DualRepIso
+import HepLean.Tensors.TensorSpecies.Basic
 /-!
 
 # Pure tensors
@@ -20,7 +20,6 @@ open MonoidalCategory
 noncomputable section
 
 namespace TensorSpecies
-open TensorTree
 variable (S : TensorSpecies)
 
 /-- The type of tensors specified by a map to colors `c : OverColor S.C`. -/
diff --git a/HepLean/Tensors/Tree/NodeIdentities/Assoc.lean b/HepLean/Tensors/Tree/NodeIdentities/Assoc.lean
index a722fd9..3c11916 100644
--- a/HepLean/Tensors/Tree/NodeIdentities/Assoc.lean
+++ b/HepLean/Tensors/Tree/NodeIdentities/Assoc.lean
@@ -3,14 +3,10 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.Tensors.Tree.NodeIdentities.ProdComm
-import HepLean.Tensors.Tree.NodeIdentities.PermProd
 import HepLean.Tensors.Tree.NodeIdentities.PermContr
-import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
 import HepLean.Tensors.Tree.NodeIdentities.ProdContr
 import HepLean.Tensors.Tree.NodeIdentities.ContrContr
 import HepLean.Tensors.Tree.NodeIdentities.ProdAssoc
-import HepLean.Tensors.TensorSpecies.Contractions.Categorical
 /-!
 
 ## Specific associativity results for tensor trees