feat: Some simple extensions of lemmas

HepLean/Tensors/OverColor/Basic.lean

@@ -100,6 +100,9 @@ def toIso (m : f ⟶ g) : f ≅ g := {
     simp only [CategoryStruct.comp, Iso.symm_self_id, Iso.refl_hom, Over.id_left, types_id_apply]
     rfl}
 
+@[simp]
+lemma hom_comp (m : f ⟶ g) (n : g ⟶ h) : (m ≫ n).hom = m.hom ≫ n.hom := by rfl
+
 end Hom
 
 section monoidal
@@ -273,12 +276,32 @@ def mk (f : X → C) : OverColor C := Over.mk f
 lemma mk_hom (f : X → C) : (mk f).hom = f := rfl
 open MonoidalCategory
 
+@[simp]
+lemma mk_left (f : X → C) : (mk f).left = X := rfl
+
 lemma Hom.fin_ext {n : ℕ} {f g : Fin n → C} (σ σ' : OverColor.mk f ⟶ OverColor.mk g)
     (h : ∀ (i : Fin n), σ.hom.left i = σ'.hom.left i) : σ = σ' := by
   apply Hom.ext
   ext i
   apply h
 
+@[simp]
+lemma β_hom_toEquiv (f : X → C) (g : Y → C) :
+    Hom.toEquiv (β_ (OverColor.mk f) (OverColor.mk g)).hom = Equiv.sumComm X Y := by
+  rfl
+
+@[simp]
+lemma β_inv_toEquiv (f : X → C) (g : Y → C) :
+    Hom.toEquiv (β_ (OverColor.mk f) (OverColor.mk g)).inv = Equiv.sumComm Y X := by
+  rfl
+
+@[simp]
+lemma whiskeringLeft_toEquiv (f : X → C) (g : Y → C) (h : Z → C) (σ : OverColor.mk f ⟶  OverColor.mk g) :
+    Hom.toEquiv (OverColor.mk h ◁ σ) = (Equiv.refl Z).sumCongr (Hom.toEquiv σ) := by
+  simp [MonoidalCategory.whiskerLeft]
+  rfl
+
+
 end OverColor
 
 end IndexNotation

HepLean/Tensors/OverColor/Iso.lean

@@ -32,6 +32,11 @@ lemma equivToIso_homToEquiv {c : X → C} (e : X ≃ Y) :
     Hom.toEquiv (equivToIso (c := c) e).hom = e := by
   rfl
 
+@[simp]
+lemma equivToIso_inv_homToEquiv {c : X → C} (e : X ≃ Y) :
+    Hom.toEquiv (equivToIso (c := c) e).inv = e.symm := by
+  rfl
+
 /-- The homomorphism between `c : X → C` and `c ∘ e.symm` as objects in `OverColor C` for an
   equivalence `e`. -/
 def equivToHom {c : X → C} (e : X ≃ Y) : mk c ⟶ mk (c ∘ e.symm) :=
@@ -65,6 +70,17 @@ lemma mkIso_refl_hom {c : X → C} : (mkIso (by rfl : c =c)).hom = 𝟙 _ := by
   rw [mkIso]
   rfl
 
+lemma mkIso_hom_hom_left {c1 c2 : X → C} (h : c1 = c2) : (mkIso h).hom.hom.left =
+    (Equiv.refl X).toFun  := by
+  rw [mkIso]
+  rfl
+
+@[simp]
+lemma mkIso_hom_hom_left_apply {c1 c2 : X → C} (h : c1 = c2) (x : X) :
+    (mkIso h).hom.hom.left x = x := by
+  rw [mkIso_hom_hom_left]
+  rfl
+
 @[simp]
 lemma equivToIso_mkIso_hom {c1 c2 : X → C} (h : c1 = c2) :
     Hom.toEquiv (mkIso h).hom = Equiv.refl _ := by
@@ -81,6 +97,17 @@ def equivToHomEq {c : X → C} {c1 : Y → C} (e : X ≃ Y)
     (h : ∀ x, c1 x = (c ∘ e.symm) x := by decide) : mk c ⟶ mk c1 :=
   (equivToHom e).trans (mkIso (funext fun x => (h x).symm)).hom
 
+@[simp]
+lemma equivToHomEq_hom_left {c : X → C} {c1 : Y → C} (e : X ≃ Y)
+    (h : ∀ x, c1 x = (c ∘ e.symm) x := by decide) : (equivToHomEq e h).hom.left =
+    e.toFun := by
+  rfl
+
+@[simp]
+lemma equivToHomEq_toEquiv  {c : X → C} {c1 : Y → C} (e : X ≃ Y)
+    (h : ∀ x, c1 x = (c ∘ e.symm) x := by decide)  : Hom.toEquiv (equivToHomEq e h) = e := by
+    rfl
+
 /-- The isomorphism splitting a `mk c` for `Fin 2 → C` into the tensor product of
   the `Fin 1 → C` maps defined by `c 0` and `c 1`. -/
 def fin2Iso {c : Fin 2 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1] := by
@@ -163,6 +190,14 @@ def extractTwo {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
     equivToHomEq (Equiv.refl _) (by simp) ≫ extractOne j (extractOne i σ) ≫
     equivToHomEq (Equiv.refl _) (by simp)
 
+@[simp]
+lemma extractTwo_hom_left_apply {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fin n.succ.succ)
+    {c1 c2 : Fin n.succ.succ.succ → C} (σ : mk c1 ⟶ mk c2) (x : Fin n.succ) :
+    (extractTwo i j σ).hom.left x = (finExtractOnePerm ((finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j)
+      (finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ))) x := by
+  simp only [extractTwo, extractOne]
+  rfl
+
 /-- Removes a given `i : Fin n.succ.succ` and `j : Fin n.succ` from a morphism in `OverColor C`.
   This is from and to different (by equivalent) objects to `extractTwo`. -/
 def extractTwoAux {n : ℕ} (i : Fin n.succ.succ) (j : Fin n.succ)
@@ -231,7 +266,7 @@ lemma extractTwo_finExtractTwo_succ {n : ℕ} (i : Fin n.succ.succ.succ) (j : Fi
   simp only [Nat.succ_eq_add_one, Equiv.apply_symm_apply]
   match k with
   | Sum.inl (Sum.inl 0) =>
-    simp
+    simp [-OverColor.mk_left]
   | Sum.inl (Sum.inr 0) =>
     simp only [Fin.isValue, finExtractTwo_symm_inl_inr_apply, Sum.map_inl, id_eq]
     have h1 : ((Hom.toEquiv σ) (Fin.succAbove

HepLean/Tensors/TensorSpecies/MetricTensor.lean

@@ -5,6 +5,10 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.Tensors.TensorSpecies.UnitTensor
 import HepLean.Tensors.TensorSpecies.ContractLemmas
+import HepLean.Tensors.Tree.NodeIdentities.ProdComm
+import HepLean.Tensors.Tree.NodeIdentities.PermProd
+import HepLean.Tensors.Tree.NodeIdentities.ContrSwap
+import HepLean.Tensors.Tree.NodeIdentities.PermContr
 /-!
 
 ## Metrics in tensor trees
@@ -28,6 +32,14 @@ def metricTensor (S : TensorSpecies) (c : S.C) : S.F.obj (OverColor.mk ![c, c])
 
 variable {S : TensorSpecies}
 
+lemma metricTensor_congr {c c' : S.C} (h : c = c') : {S.metricTensor c | μ ν}ᵀ.tensor =
+    (perm  (OverColor.equivToHomEq (Equiv.refl _) (fun x => by subst h; fin_cases x <;> rfl ))
+    {S.metricTensor c' | μ ν}ᵀ).tensor := by
+  subst h
+  change _ = (S.F.map (𝟙 _)).hom (S.metricTensor c)
+  simp
+
+
 lemma pairIsoSep_inv_metricTensor (c : S.C) :
     (Discrete.pairIsoSep S.FD).inv.hom (S.metricTensor c) =
     (S.metric.app (Discrete.mk c)).hom (1 : S.k) := by
@@ -48,12 +60,9 @@ lemma contr_metric_braid_unit (c : S.C) :  (((S.FD.obj (Discrete.mk c)) ◁
     (OverColor.Discrete.pairIsoSep S.FD).inv.hom (S.metricTensor (S.τ c)))))))) =
     (β_ (S.FD.obj (Discrete.mk (S.τ c))) (S.FD.obj (Discrete.mk c))).hom.hom
       ((S.unit.app (Discrete.mk c)).hom (1 : S.k)) := by
-  have hx : Function.Injective (β_ (S.FD.obj (Discrete.mk c)) (S.FD.obj (Discrete.mk (S.τ c))) ).hom.hom := by
-    change  Function.Injective (β_ (S.FD.obj (Discrete.mk c)).V (S.FD.obj (Discrete.mk (S.τ c))).V ).hom
-    exact (β_ (S.FD.obj (Discrete.mk c)).V (S.FD.obj (Discrete.mk (S.τ c))).V ).toLinearEquiv.toEquiv.injective
-  apply hx
+  apply (β_ _ _).toLinearEquiv.toEquiv.injective
   rw [pairIsoSep_inv_metricTensor, pairIsoSep_inv_metricTensor]
-  rw [S.contr_metric c]
+  erw [S.contr_metric c]
   change  _ = (β_  (S.FD.obj { as := S.τ c }) (S.FD.obj { as := c })).inv.hom
     ((β_ (S.FD.obj { as := S.τ c }) (S.FD.obj { as := c })).hom.hom _)
   rw [Discrete.rep_iso_inv_hom_apply]
@@ -66,16 +75,53 @@ lemma metricTensor_contr_dual_metricTensor_perm_cond (c : S.C) : ∀ (x : Fin (N
   · rfl
   · rfl
 
-/-- The contraction of a metric tensor with its dual gives the unit. -/
+/-- The contraction of a metric tensor with its dual via the inner indices gives the unit. -/
 lemma metricTensor_contr_dual_metricTensor_eq_unit (c : S.C) :
-    {S.metricTensor c | μ ν ⊗ S.metricTensor (S.τ c) | ν ρ}ᵀ.tensor =
-    (perm (OverColor.equivToHomEq (finMapToEquiv ![1, 0] ![1, 0])
-      (metricTensor_contr_dual_metricTensor_perm_cond c)) {S.unitTensor c | μ ρ}ᵀ).tensor := by
+    {S.metricTensor c | μ ν ⊗ S.metricTensor (S.τ c) | ν ρ}ᵀ.tensor = ({S.unitTensor c | μ ρ}ᵀ |>
+    perm (OverColor.equivToHomEq (finMapToEquiv ![1, 0] ![1, 0])
+      (metricTensor_contr_dual_metricTensor_perm_cond c))).tensor := by
   rw [contr_two_two_inner, contr_metric_braid_unit, Discrete.pairIsoSep_β]
   change (S.F.map _ ≫ S.F.map _ ).hom _ = _
   rw [← S.F.map_comp]
   rfl
 
+/-- The contraction of a metric tensor with its dual via the outer indices gives the unit. -/
+lemma metricTensor_contr_dual_metricTensor_outer_eq_unit  (c : S.C) :
+    {S.metricTensor c | ν μ ⊗ S.metricTensor (S.τ c) | ρ ν}ᵀ.tensor = ({S.unitTensor c | μ ρ}ᵀ |>
+    perm (OverColor.equivToHomEq
+      (finMapToEquiv ![1, 0] ![1, 0]) (fun x => by fin_cases x <;> rfl))).tensor := by
+  conv_lhs =>
+    rw [contr_tensor_eq <| prod_tensor_eq_fst <| metricTensor_congr (S.τ_involution c).symm]
+    rw [contr_tensor_eq <| prod_comm _ _ _ _]
+    rw [perm_contr_congr 2 1 (by rfl) (by rfl)]
+    rw [perm_tensor_eq <| contr_tensor_eq <| prod_perm_right _ _ _ _]
+    rw [perm_tensor_eq <| perm_contr_congr 2 1 (by rfl) (by rfl)]
+    rw [perm_perm]
+    rw [perm_tensor_eq <| contr_swap _ _]
+    rw [perm_perm]
+    erw [perm_tensor_eq <| metricTensor_contr_dual_metricTensor_eq_unit _]
+    rw [perm_perm]
+    rw [perm_tensor_eq <| dual_unitTensor_eq_perm _]
+    rw [perm_perm]
+  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,
+    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]
+  fin_cases i
+  · decide
+  · decide
+
 end TensorSpecies
 
 end

HepLean/Tensors/Tree/NodeIdentities/Basic.lean

@@ -140,7 +140,7 @@ lemma perm_eq_iff_eq_perm {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
       apply Hom.ext
       ext x
       change (Hom.toEquiv σ) ((Hom.toEquiv σ).symm x) = x
-      simp
+      simp [-OverColor.mk_left]
     rw [h1]
     simp
 

HepLean/Tensors/Tree/NodeIdentities/PermProd.lean

@@ -35,6 +35,11 @@ def permProdLeft := (equivToIso finSumFinEquiv).inv ≫ σ ▷ OverColor.mk c2
 def permProdRight := (equivToIso finSumFinEquiv).inv ≫ OverColor.mk c2 ◁ σ
   ≫ (equivToIso finSumFinEquiv).hom
 
+@[simp]
+lemma permProdRight_toEquiv : Hom.toEquiv (permProdRight c2 σ) =  finSumFinEquiv.symm.trans
+    (((Equiv.refl (Fin n2)).sumCongr (Hom.toEquiv σ)).trans finSumFinEquiv)  := by
+  simp [permProdRight]
+
 /-- When a `prod` acts on a `perm` node in the left entry, the `perm` node can be moved through
   the `prod` node via right-whiskering. -/
 theorem prod_perm_left (t : TensorTree S c) (t2 : TensorTree S c2) :

HepLean/Tensors/Tree/NodeIdentities/ProdComm.lean

@@ -31,6 +31,11 @@ def braidPerm : OverColor.mk (Sum.elim c2 c ∘ ⇑finSumFinEquiv.symm) ⟶
   (β_ (OverColor.mk c2) (OverColor.mk c)).hom
   ≫ (equivToIso finSumFinEquiv).hom
 
+@[simp]
+lemma braidPerm_toEquiv : Hom.toEquiv (braidPerm c c2) = finSumFinEquiv.symm.trans
+    ((Equiv.sumComm (Fin n2) (Fin n)).trans finSumFinEquiv) := by
+  simp [braidPerm]
+
 lemma finSumFinEquiv_comp_braidPerm :
     (equivToIso finSumFinEquiv).hom ≫ braidPerm c c2 =
     (β_ (OverColor.mk c2) (OverColor.mk c)).hom