diff --git a/FormalConjectures/ForMathlib/Combinatorics/TensorContraction.lean b/FormalConjectures/ForMathlib/Combinatorics/TensorContraction.lean
new file mode 100644
index 000000000..eb9ccaf95
--- /dev/null
+++ b/FormalConjectures/ForMathlib/Combinatorics/TensorContraction.lean
@@ -0,0 +1,349 @@
+import Mathlib
+
+open scoped TensorProduct
+open scoped BigOperators
+
+-- TODO(Paul): change this to `Set.univ \ Set.range f` ?
+abbrev Free {A : Type*} {R : Type*} (f : R → A) :=
+  {a : A // a ∉ Set.range f}
+
+variable {V : Type*}
+variable {A : Type*}
+variable {B : Type*}
+variable {C : Type*}
+variable {R : Type*}
+variable (fst : R → A) (snd : R → B)
+variable (f : (Free fst) ⊕ (Free snd) ≃ C) (vA : A → V) (vB : B → V)
+
+def PurePartOfContraction :
+    (C → V) :=
+  let inc : (Free fst) ⊕ (Free snd) → A ⊕ B := Sum.map (fun i => i) (fun i => i)
+  let vSum : A ⊕ B → V := fun s =>
+    match s with
+    | Sum.inl a => vA a
+    | Sum.inr a => vB a
+  vSum ∘ inc ∘ f.symm
+
+lemma PurePart_Invariance_Right
+    [DecidableEq B]
+    (i : Set.range snd)
+    (x : V):
+    PurePartOfContraction fst snd f vA (Function.update vB i.val x) = PurePartOfContraction fst snd f vA vB := by
+  simp only [PurePartOfContraction, ← Function.comp_assoc, f.symm.surjective.right_cancellable]
+  funext j
+  cases j with
+  | inl a => simp
+  | inr b => grind
+
+lemma PurePart_Invariance_Left
+    [DecidableEq A]
+    (i : Set.range fst)
+    (x : V):
+    PurePartOfContraction fst snd f (Function.update vA i.val x) vB = PurePartOfContraction fst snd f vA vB := by
+  simp only [PurePartOfContraction, ← Function.comp_assoc,
+    f.symm.surjective.right_cancellable]
+  funext j
+  cases j with
+  | inl a => grind
+  | inr b => simp
+
+lemma PurePart_Update_Right
+    [DecidableEq B]
+    [DecidableEq C]
+    (i : Free snd)
+    (x : V):
+    PurePartOfContraction fst snd f vA (Function.update vB i.val x) = Function.update (PurePartOfContraction fst snd f vA vB) (f (Sum.inr i)) x := by
+  simp [PurePartOfContraction]
+  funext t
+  by_cases h : t = f (Sum.inr i)
+  . grind
+  · rw [Function.update_of_ne h]
+    cases hft : f.symm t with
+    | inl a => simp [hft]
+    | inr a => grind
+
+lemma PurePart_Update_Left
+    [DecidableEq A]
+    [DecidableEq C]
+    (i : Free fst)
+    (x : V):
+    PurePartOfContraction fst snd f (Function.update vA i.val x) vB = Function.update (PurePartOfContraction fst snd f vA vB) (f (Sum.inl i)) x := by
+  simp [PurePartOfContraction]
+  funext t
+  by_cases h : t = f (Sum.inl i)
+  . grind
+  · rw [Function.update_of_ne h]
+    cases hft : f.symm t with
+    | inr a => simp [hft]
+    | inl a => grind
+
+variable [NormedAddCommGroup V] [InnerProductSpace ℝ V]
+variable [Fintype R]
+
+noncomputable def ScalarPartOfContraction : ℝ :=
+  let scalars : R → ℝ := fun r =>
+    inner ℝ (vA (fst r)) (vB (snd r))
+  ∏ r : R, scalars r
+
+lemma ScalarPart_Invariance_Right
+     [DecidableEq B]
+    (i : Free snd)
+    (x : V):
+    ScalarPartOfContraction fst snd vA (Function.update vB i.val x) = ScalarPartOfContraction fst snd vA vB := by
+  simp [ScalarPartOfContraction]
+  grind
+
+lemma ScalarPart_Invariance_Left
+    [DecidableEq A]
+    (i : Free fst)
+    (x : V):
+    ScalarPartOfContraction fst snd (Function.update vA i.val x) vB = ScalarPartOfContraction fst snd vA vB := by
+  simp [ScalarPartOfContraction]
+  grind
+
+variable [DecidableEq R]
+
+lemma ScalarPart_Update_Add_Right
+     [DecidableEq B]
+    (hInjsnd : Function.Injective snd)
+    (i : Set.range snd)
+    (x y: V):
+    ScalarPartOfContraction fst snd vA (Function.update vB i.val (x + y)) = (ScalarPartOfContraction fst snd vA (Function.update vB i.val x)) + (ScalarPartOfContraction fst snd vA (Function.update vB i.val y)) := by
+  simp only [ScalarPartOfContraction]
+  rcases i.property with ⟨r₀, hr₀i⟩
+  have hr₀R : r₀ ∈ (Finset.univ : Finset R) := by simp
+  have hsplit (z : V) :=
+    (Finset.mul_prod_erase
+      (s := (Finset.univ : Finset R))
+      (f := fun r => inner ℝ (vA (fst r)) (Function.update vB i z (snd r)))
+      (a := r₀)
+      (h := hr₀R)
+      ).symm
+  have prod_const (z : V) :
+    (∏ r ∈ ((Finset.univ : Finset R).erase r₀),
+        inner ℝ (vA (fst r)) (
+          if snd r = i then
+            z
+          else vB (snd r)
+          ))
+      =
+    (∏ r ∈ ((Finset.univ : Finset R).erase r₀),
+        inner ℝ (vA (fst r)) (vB (snd r))) := by
+    refine Finset.prod_congr rfl ?_
+    grind
+  simp_rw [hsplit]
+  simp [Function.update, hr₀i, inner_add_right, add_mul, prod_const]
+
+lemma ScalarPart_Update_Add_Left
+    [DecidableEq A]
+    (fst : R → A) (snd : R → B)
+    (hInjfst : Function.Injective fst)
+    (vA : A → V) (vB : B → V)
+    (i : Set.range fst)
+    (x y: V):
+    ScalarPartOfContraction fst snd (Function.update vA i.val (x + y)) vB = (ScalarPartOfContraction fst snd (Function.update vA i.val x) vB) + (ScalarPartOfContraction fst snd (Function.update vA i.val y) vB) := by
+  simp only [ScalarPartOfContraction]
+  rcases i.property with ⟨r₀, hr₀i⟩
+  have hr₀R : r₀ ∈ (Finset.univ : Finset R) := by simp
+  have hsplit (z : V) :=
+    (Finset.mul_prod_erase
+      (s := (Finset.univ : Finset R))
+      (f := fun r => inner ℝ (Function.update vA i z (fst r)) (vB (snd r)))
+      (a := r₀)
+      (h := hr₀R)
+      ).symm
+  have prod_const (z : V) :
+    (∏ r ∈ ((Finset.univ : Finset R).erase r₀),
+        inner ℝ (
+          if fst r = i then
+            z
+          else vA (fst r)
+          ) (vB (snd r)))
+      =
+    (∏ r ∈ ((Finset.univ : Finset R).erase r₀),
+        inner ℝ (vA (fst r)) (vB (snd r))) := by
+    refine Finset.prod_congr rfl ?_
+    grind
+  simp [hsplit]
+  simp [Function.update, hr₀i, inner_add_left, add_mul, prod_const]
+
+lemma ScalarPart_Update_Mul_Right
+     [DecidableEq B]
+    (fst : R → A) (snd : R → B)
+    (hInjsnd : Function.Injective snd)
+    (vA : A → V) (vB : B → V)
+    (i : Set.range snd)
+    (c : ℝ) (x : V) :
+    ScalarPartOfContraction fst snd vA (Function.update vB i.val (c • x)) = c • ScalarPartOfContraction fst snd vA (Function.update vB i.val x) := by
+  simp only [ScalarPartOfContraction]
+  rcases i.property with ⟨r₀, hr₀i⟩
+  have hr₀R : r₀ ∈ (Finset.univ : Finset R) := by simp
+  have hsplit (z : V) :=
+    (Finset.mul_prod_erase
+      (s := (Finset.univ : Finset R))
+      (f := fun r => inner ℝ (vA (fst r)) (Function.update vB i z (snd r)))
+      (a := r₀)
+      (h := hr₀R)
+      ).symm
+  have prod_const (z : V) :
+    (∏ r ∈ ((Finset.univ : Finset R).erase r₀),
+        inner ℝ (vA (fst r)) (
+          if snd r = i then
+            z
+          else vB (snd r)
+          ))
+      =
+    (∏ r ∈ ((Finset.univ : Finset R).erase r₀),
+        inner ℝ (vA (fst r)) (vB (snd r))) := by
+    refine Finset.prod_congr rfl ?_
+    grind
+  simp [hsplit]
+  simp [Function.update, hr₀i, inner_smul_right, mul_assoc, prod_const]
+
+lemma ScalarPart_Update_Mul_Left
+    [DecidableEq A]
+    (fst : R → A) (snd : R → B)
+    (hInjsnd : Function.Injective fst)
+    (vA : A → V) (vB : B → V)
+    (i : Set.range fst)
+    (c : ℝ) (x : V) :
+    ScalarPartOfContraction fst snd (Function.update vA i.val (c • x)) vB = c • ScalarPartOfContraction fst snd (Function.update vA i.val x) vB := by
+  simp only [ScalarPartOfContraction]
+  rcases i.property with ⟨r₀, hr₀i⟩
+  have hr₀R : r₀ ∈ (Finset.univ : Finset R) := by simp
+  have hsplit (z : V) :=
+    (Finset.mul_prod_erase
+      (s := (Finset.univ : Finset R))
+      (f := fun r => inner ℝ (Function.update vA i z (fst r)) (vB (snd r)))
+      (a := r₀)
+      (h := hr₀R)
+      ).symm
+  have prod_const (z : V) :
+    (∏ r ∈ ((Finset.univ : Finset R).erase r₀),
+        inner ℝ (
+          if fst r = i then
+            z
+          else vA (fst r)
+          ) (vB (snd r)))
+      =
+    (∏ r ∈ ((Finset.univ : Finset R).erase r₀),
+        inner ℝ (vA (fst r)) (vB (snd r))) := by
+    refine Finset.prod_congr rfl ?_
+    grind
+  simp [hsplit]
+  simp [Function.update, hr₀i, inner_smul_left, mul_assoc, prod_const]
+
+noncomputable def EvaluateContraction
+    {m : ℕ}
+    (f : (Free fst) ⊕ (Free snd) ≃ Fin m)
+    (vA : A → V) (vB : B → V) :
+    (⨂[ℝ]^m V) :=
+  letI pure : Fin m → V := PurePartOfContraction fst snd f vA vB
+  letI scal : ℝ := ScalarPartOfContraction fst snd vA vB
+  scal • (PiTensorProduct.tprod ℝ pure)
+
+noncomputable def ContractionWithPure
+    {l m : ℕ}
+    (fst : R → A) (snd : R → (Fin l))
+    (hInjsnd : Function.Injective snd)
+    (f : (Free fst) ⊕ (Free snd) ≃ Fin m)
+    (vA : A → V) :
+    MultilinearMap ℝ (fun _ : Fin l => V) (⨂[ℝ]^m V) := by
+  refine
+    { toFun := ?toFun,
+      map_update_add' := ?map_update_add',
+      map_update_smul' := ?map_update_smul'
+      }
+  . intro vB
+    let hDec : DecidableEq (Fin l) := instDecidableEqFin l
+    exact EvaluateContraction fst snd f vA vB
+  . intro _ vB i x y
+    by_cases hi : i ∈ Set.range snd
+    . have hScalar := ScalarPart_Update_Add_Right fst snd (B := Fin l) vA vB hInjsnd ⟨i,hi⟩ x y
+      have hPure (z : V) := PurePart_Invariance_Right fst snd f vA vB ⟨i,hi⟩ z
+      simp [EvaluateContraction, hScalar, hPure, add_smul]
+    . have hPure (z : V) := PurePart_Update_Right fst snd f vA vB ⟨i, hi⟩ z
+      have hScalar (z : V) := ScalarPart_Invariance_Right fst snd vA vB ⟨i,hi⟩ z
+      simp [EvaluateContraction, hScalar, hPure]
+  . intro _ vB i c x
+    by_cases hi : i ∈ Set.range snd
+    . have hScalar :=
+        ScalarPart_Update_Mul_Right fst snd hInjsnd vA vB ⟨i,hi⟩ c x
+      have hPure (z : V) := PurePart_Invariance_Right fst snd f vA vB ⟨i,hi⟩ z
+      simp [EvaluateContraction, hScalar, hPure, mul_smul]
+    . have hScalar (z : V) := ScalarPart_Invariance_Right fst snd vA vB ⟨i, hi⟩ z
+      have hPure (z : V) := PurePart_Update_Right fst snd f vA vB ⟨i,hi⟩ z
+      simp [EvaluateContraction, hScalar, hPure, ← smul_assoc, mul_comm]
+
+lemma ContractionWithPure_update_add
+    [DecidableEq A]
+    {l m : ℕ}
+    (fst : R → A) (snd : R → (Fin l))
+    (hInjfst : Function.Injective fst)
+    (hInjsnd : Function.Injective snd)
+    (f : (Free fst) ⊕ (Free snd) ≃ Fin m)
+    (vA : A → V) (i : A) (x y : V):
+      ContractionWithPure fst snd hInjsnd f (Function.update vA i (x + y)) = (ContractionWithPure fst snd hInjsnd f (Function.update vA i x)) + (ContractionWithPure fst snd hInjsnd f (Function.update vA i y)) := by
+  simp only [ContractionWithPure]
+  ext vB
+  by_cases hi : i ∈ Set.range fst
+  . have hScalar := ScalarPart_Update_Add_Left fst snd hInjfst vA vB ⟨i,hi⟩ x y
+    have hPure (z : V) := PurePart_Invariance_Left fst snd f vA vB ⟨i,hi⟩ z
+    simp [EvaluateContraction, hScalar, hPure, add_smul]
+  . have hPure (z : V) := PurePart_Update_Left fst snd f vA vB ⟨i, hi⟩ z
+    have hScalar (z : V) := ScalarPart_Invariance_Left fst snd vA vB ⟨i,hi⟩ z
+    simp [EvaluateContraction, hScalar, hPure]
+
+lemma ContractionWithPure_update_mul
+    [DecidableEq A]
+    {l m : ℕ}
+    (fst : R → A) (snd : R → (Fin l))
+    (hInjfst : Function.Injective fst)
+    (hInjsnd : Function.Injective snd)
+    (f : (Free fst) ⊕ (Free snd) ≃ Fin m)
+    (vA : A → V) (i : A) (c : ℝ) (x : V):
+      ContractionWithPure fst snd hInjsnd f (Function.update vA i (c • x)) = c • (ContractionWithPure fst snd hInjsnd f (Function.update vA i x)) := by
+  simp only [ContractionWithPure]
+  ext vB
+  by_cases hi : i ∈ Set.range fst
+  . have hScalar :=
+      ScalarPart_Update_Mul_Left fst snd hInjfst vA vB ⟨i,hi⟩ c x
+    have hPure (z : V) := PurePart_Invariance_Left fst snd f vA vB ⟨i,hi⟩ z
+    simp [EvaluateContraction, hScalar, hPure, mul_smul]
+  . have hScalar (z : V) :=
+      ScalarPart_Invariance_Left fst snd vA vB ⟨i, hi⟩ z
+    have hPure (z : V) :=
+      PurePart_Update_Left fst snd f vA vB ⟨i,hi⟩ z
+    simp [EvaluateContraction, hScalar, hPure, ← smul_assoc, mul_comm]
+
+noncomputable def MultiLinearTensorContraction
+    {k l m : ℕ}
+    (fst : R → (Fin k)) (snd : R → (Fin l))
+    (hInjfst : Function.Injective fst)
+    (hInjsnd : Function.Injective snd)
+    (f : (Free fst) ⊕ (Free snd) ≃ Fin m) :
+      MultilinearMap ℝ (fun _ : Fin k => V) (⨂[ℝ]^l V →ₗ[ℝ] ⨂[ℝ]^m V) where
+  toFun va := PiTensorProduct.lift (ContractionWithPure fst snd hInjsnd f va)
+  map_update_add' := by
+    intro _ vA i x y
+    simpa using congrArg PiTensorProduct.lift
+      (ContractionWithPure_update_add
+        (fst := fst) (snd := snd)
+        (hInjfst := hInjfst) (hInjsnd := hInjsnd)
+        (f := f) (vA := vA) (i := i) (x := x) (y := y))
+  map_update_smul' := by
+    intro _ vA i c x
+    simpa using congrArg PiTensorProduct.lift
+      (ContractionWithPure_update_mul
+        (fst := fst) (snd := snd)
+        (hInjfst := hInjfst) (hInjsnd := hInjsnd)
+        (f := f) (vA := vA) (i := i) (c := c) (x := x))
+
+noncomputable def TensorContraction
+    {k l m : ℕ}
+    (fst : R → (Fin k)) (snd : R → (Fin l))
+    (hInjfst : Function.Injective fst)
+    (hInjsnd : Function.Injective snd)
+    (f : (Free fst) ⊕ (Free snd) ≃ Fin m) :
+      (⨂[ℝ]^k V) →ₗ[ℝ] ⨂[ℝ]^l V →ₗ[ℝ] ⨂[ℝ]^m V :=
+  PiTensorProduct.lift (MultiLinearTensorContraction fst snd hInjfst hInjsnd f)
diff --git a/FormalConjectures/ForMathlib/Combinatorics/TensorNetwork.lean b/FormalConjectures/ForMathlib/Combinatorics/TensorNetwork.lean
new file mode 100644
index 000000000..8a90ff517
--- /dev/null
+++ b/FormalConjectures/ForMathlib/Combinatorics/TensorNetwork.lean
@@ -0,0 +1,392 @@
+import Mathlib
+import FormalConjectures.ForMathlib.Combinatorics.TensorContraction
+
+
+open scoped TensorProduct
+open scoped BigOperators
+
+variable (V : Type*)[NormedAddCommGroup V] [InnerProductSpace ℝ V]
+
+structure TensorNetwork (α β : Type*) [Fintype α] [Fintype β] where
+  G : Graph α β
+  [loc : ∀ x : α, Fintype (G.incidenceSet x)]
+  loopless : ∀ (e : β) (x : α), ¬ G.IsLoopAt e x
+  c : ∀ x : α, G.incidenceSet x → Fin (Fintype.card (G.incidenceSet x))
+  hc : ∀ x : α, Function.Bijective (c x)
+
+namespace TensorNetwork
+noncomputable def deg {α β : Type*} [Fintype α] [Fintype β] (G : TensorNetwork α β) (x : α) : ℕ := by
+  have hfin : Fintype (G.G.incidenceSet x) := G.loc x
+  exact Fintype.card (G.G.incidenceSet x)
+end TensorNetwork
+
+/-- Given a tensor network `G`, the assignement of a tensor `T_v` for each vertex.
+Note: we also assigne "junk values for elements of `α` that aren't edges". -/
+structure TensorMap {α β : Type*} [Fintype α] [Fintype β] (G : TensorNetwork α β)  where
+  tensor : ∀ x : α, ⨂[ℝ]^(G.deg x) V
+
+noncomputable def SingleLegContractionGraph {α β: Type*} [Fintype α] [DecidableEq α] [Fintype β] {G : TensorNetwork α β} (loopless : ∀ (e : β) (x : α), ¬ G.G.IsLoopAt e x) (v w : α) (hv : v ∈ G.G.vertexSet) (hvw : ¬v = w): Graph α β := by
+  classical
+  refine
+    { vertexSet := ?_
+      IsLink := ?_
+      edgeSet := ?_
+      isLink_symm := ?_
+      eq_or_eq_of_isLink_of_isLink := ?_
+      edge_mem_iff_exists_isLink := ?_
+      left_mem_of_isLink := ?_
+      }
+  . exact G.G.vertexSet \ {w}
+  . let is_link_new : β → α → α → Prop := fun e x y =>
+      if (w = x) ∨ (w = y) ∨ (x = y) then
+        False
+      else if (x = v) then
+        (G.G.IsLink e v y) ∨ (G.G.IsLink e w y)
+      else if (y = v) then
+        (G.G.IsLink e x v) ∨ (G.G.IsLink e x w)
+      else
+        G.G.IsLink e x y
+    exact is_link_new
+  . exact G.G.edgeSet \ {e | G.G.IsLink e v w}
+  . intro e h
+    have he : e ∈ G.G.edgeSet := ((Set.mem_diff (s := G.G.edgeSet) (t := {e | G.G.IsLink e v w}) (e : β)).1 h).1
+    simp [Symmetric]
+    intro x y hwx hwy hxy hexy
+    have hsymm := G.G.isLink_symm (e := e) he
+    constructor
+    . simp [hwx,hwy,Ne.symm hxy]
+    . by_cases hyv : y = v
+      . simp [hyv]
+        by_cases hxv : x = v
+        . simp [hxv, hyv] at hexy
+          simp [hxv, hexy]
+        . simp [hxv,hyv] at hexy
+          by_cases hlinkexv : G.G.IsLink e x v
+          . simp [hsymm hlinkexv]
+          . simp [hlinkexv] at hexy
+            simp [hsymm hexy]
+      . simp [hyv]
+        by_cases hxv : x = v
+        . simp [hxv]
+          simp [hxv] at hexy
+          by_cases hlinkevy : G.G.IsLink e v y
+          . simp [hsymm hlinkevy]
+          . simp [hlinkevy] at hexy
+            simp [hsymm hexy]
+        . simp [hxv]
+          simp [hxv, hyv] at hexy
+          simp [hsymm hexy]
+  . intro e x y v_1 w_1 h1 h2
+    by_cases hxv1 : x = v_1
+    . simp [hxv1]
+    . simp [hxv1]
+      by_cases hxw1 : x = w_1
+      . exact hxw1
+      . by_cases hwx : w = x
+        . simp [hwx] at h1
+        . by_cases hwy : w = y
+          . simp [hwy] at h1
+          . by_cases hxy : x = y
+            . simp [hxy] at h1
+            . simp [hwx,hwy,hxy] at h1
+              by_cases hwv1 : w = v_1
+              . simp [hwv1] at h2
+              . simp [hwv1] at h2
+                by_cases hww1 : w = w_1
+                . simp [hww1] at h2
+                . simp [hww1] at h2
+                  by_cases hv1w1 : v_1 = w_1
+                  . simp [hv1w1] at h2
+                  . simp [hv1w1] at h2
+                    by_cases hvx : v = x
+                    . simp [hvx] at h1
+                      simp [hvx] at h2
+                      simp [Ne.symm hxv1, Ne.symm hxw1] at h2
+                      have he := (G.G.edge_mem_iff_exists_isLink e).symm.1 ⟨v_1, w_1, h2⟩
+                      have hG := G.G.eq_or_eq_of_isLink_of_isLink (e := e)
+                      by_cases hlink : G.G.IsLink e x y
+                      . apply hG (x := x) (y := y) (v := v_1) (w := w_1) at hlink
+                        apply hlink at h2
+                        simp [hxv1,hxw1] at h2
+                      . simp [hlink] at h1
+                        apply hG (x := w) (y := y) (v := v_1) (w := w_1) at h1
+                        apply h1 at h2
+                        simp [hwv1,hww1] at h2
+                    . simp [Ne.symm hvx] at h1
+                      by_cases hv1v : v_1 = v
+                      . simp [hv1v] at h2
+                        by_cases hyv : y = v
+                        . simp [hyv] at h1
+                          by_cases hlink : G.G.IsLink e x v
+                          . have he := (G.G.edge_mem_iff_exists_isLink e).symm.1 ⟨x, v, hlink⟩
+                            have hG := G.G.eq_or_eq_of_isLink_of_isLink (e := e)
+                            by_cases hlink2 : G.G.IsLink e v w_1
+                            . apply hG (x := x) (y := v) (v := v) (w := w_1) hlink at hlink2
+                              simp [Ne.symm hvx, hxw1] at hlink2
+                            . simp [hlink2] at h2
+                              apply hG (x := x) (y := v) (v := w) (w := w_1) hlink at h2
+                              simp [Ne.symm hwx, hxw1] at h2
+                          . simp [hlink] at h1
+                            have he := (G.G.edge_mem_iff_exists_isLink e).symm.1 ⟨x, w, h1⟩
+                            have hG := G.G.eq_or_eq_of_isLink_of_isLink (e := e)
+                            by_cases hlink2 : G.G.IsLink e v w_1
+                            . apply hG (x := x) (y := w) (v := v) (w := w_1) h1 at hlink2
+                              simp [Ne.symm hvx, hxw1] at hlink2
+                            . simp [hlink2] at h2
+                              apply hG (x := x) (y := w) (v := w) (w := w_1) h1 at h2
+                              simp [Ne.symm hwx, hxw1] at h2
+                        . simp [hyv] at h1
+                          have he := (G.G.edge_mem_iff_exists_isLink e).symm.1 ⟨x, y, h1⟩
+                          have hG := G.G.eq_or_eq_of_isLink_of_isLink (e := e)
+                          by_cases hlink : G.G.IsLink e v w_1
+                          . apply hG (x := x) (y := y) (v := v) (w := w_1) h1 at hlink
+                            simp [Ne.symm hvx, hxw1] at hlink
+                          . simp [hlink] at h2
+                            apply hG (x := x) (y := y) (v := w) (w := w_1) h1 at h2
+                            simp [Ne.symm hwx, hxw1] at h2
+                      . simp [hv1v] at h2
+                        by_cases hyv : y = v
+                        . simp [hyv] at h1
+                          by_cases hw1v : w_1 = v
+                          . simp [hw1v] at h2
+                            by_cases hlink : G.G.IsLink e x v
+                            . have he := (G.G.edge_mem_iff_exists_isLink e).symm.1 ⟨x, v, hlink⟩
+                              have hG := G.G.eq_or_eq_of_isLink_of_isLink (e := e)
+                              by_cases hlink2 : G.G.IsLink e v_1 v
+                              . apply hG (x := x) (y := v) (v := v_1) (w := v) hlink at hlink2
+                                simp [hxv1, Ne.symm hvx] at hlink2
+                              . simp [hlink2] at h2
+                                apply hG (x := x) (y := v) (v := v_1) (w := w) hlink at h2
+                                simp [hxv1, Ne.symm hwx] at h2
+                            . simp [hlink] at h1
+                              have he := (G.G.edge_mem_iff_exists_isLink e).symm.1 ⟨x, w, h1⟩
+                              have hG := G.G.eq_or_eq_of_isLink_of_isLink (e := e)
+                              by_cases hlink2 : G.G.IsLink e v_1 v
+                              . apply hG (x := x) (y := w) (v := v_1) (w := v) h1 at hlink2
+                                simp [hxv1, Ne.symm hvx] at hlink2
+                              . simp [hlink2] at h2
+                                apply hG (x := x) (y := w) (v := v_1) (w := w) h1 at h2
+                                simp [hxv1, Ne.symm hwx] at h2
+                          . simp [hw1v] at h2
+                            have he := (G.G.edge_mem_iff_exists_isLink e).symm.1 ⟨v_1, w_1, h2⟩
+                            have hG := G.G.eq_or_eq_of_isLink_of_isLink (e := e)
+                            by_cases hlink : G.G.IsLink e x v
+                            . apply hG (x := x) (y := v) (v := v_1) (w := w_1) hlink at h2
+                              simp [hxv1, hxw1] at h2
+                            . simp [hlink] at h1
+                              apply hG (x := x) (y := w) (v := v_1) (w := w_1) h1 at h2
+                              simp [hxv1, hxw1] at h2
+                        . simp [hyv] at h1
+                          have he := (G.G.edge_mem_iff_exists_isLink e).symm.1 ⟨x, y, h1⟩
+                          have hG := G.G.eq_or_eq_of_isLink_of_isLink (e := e)
+                          by_cases hw1v : w_1 = v
+                          . simp [hw1v] at h2
+                            by_cases hlink : G.G.IsLink e v_1 v
+                            . apply hG (x := x) (y := y) (v := v_1) (w := v) h1 at hlink
+                              simp [hxv1, Ne.symm hvx] at hlink
+                            . simp [hlink] at h2
+                              apply hG (x := x) (y := y) (v := v_1) (w := w) h1 at h2
+                              simp [hxv1, Ne.symm hwx] at h2
+                          . simp [hw1v] at h2
+                            apply hG (x := x) (y := y) (v := v_1) (w := w_1) h1 at h2
+                            simp [hxv1, hxw1] at h2
+  . intro e
+    constructor
+    . intro he
+      simp at he
+      have he1 := he.1
+      have he2 := he.2
+      apply (G.G.edge_mem_iff_exists_isLink (e := e)).1 at he1
+      rcases he1 with ⟨s, t, hst⟩
+      by_cases hsw : s = w
+      . use v, t
+        simp [Ne.symm hvw]
+        simp [hsw] at hst
+        apply G.G.isLink_comm.1 at hst
+        by_cases htv : t = v
+        . simp [htv] at hst
+          simp [hst] at he2
+        . by_cases hwt : w = t
+          . simp [hwt] at hst
+            simp [loopless] at hst
+          . simp [hwt, Ne.symm htv]
+            simp [G.G.isLink_comm.1 hst]
+      . by_cases htw : t = w
+        . use s, v
+          simp [Ne.symm hsw, Ne.symm hvw]
+          by_cases hsv : s = v
+          . simp [hsv]
+            simp [htw,hsv,he2] at hst
+          . simp [hsv]
+            simp [htw] at hst
+            simp [hst]
+        . use s, t
+          simp [Ne.symm hsw, Ne.symm htw]
+          by_cases hst2 : s = t
+          . simp [hst2]
+            simp [hst2, loopless] at hst
+          . simp [hst2]
+            by_cases hsv : s = v
+            . simp [hsv]
+              simp [hsv] at hst
+              simp [hst]
+            . simp [hsv]
+              by_cases htv : t = v
+              . simp [htv]
+                simp [htv] at hst
+                simp [hst]
+              . simp [htv, hst]
+    . intro h
+      rcases h with ⟨s, t, hst⟩
+      by_cases hws : w = s
+      . simp [hws] at hst
+      . by_cases hwt : w = t
+        . simp [hwt] at hst
+        . by_cases hst2 : s = t
+          . simp [hst2] at hst
+          . simp [hws, hwt, hst2] at hst
+            by_cases hsv : s = v
+            . simp [hsv] at hst
+              by_cases hlink : G.G.IsLink e v t
+              . refine And.intro ?_ ?_
+                . exact (G.G.edge_mem_iff_exists_isLink (e := e)).2 ⟨v, t, hlink⟩
+                . simp
+                  have h := ((G.G.eq_or_eq_of_isLink_of_isLink (e := e) (x := t) (y := v) (v := w) (w := v)) (G.G.isLink_comm.1 hlink))
+                  simp [G.G.isLink_comm] at h
+                  intro hG
+                  simp [hG] at h
+                  simp [Ne.symm hwt] at h
+                  simp [h] at hlink
+                  simp [loopless] at hlink
+              . simp [hlink] at hst
+                refine And.intro ?_ ?_
+                . exact (G.G.edge_mem_iff_exists_isLink (e := e)).2 ⟨w, t, hst⟩
+                . simp
+                  have h := ((G.G.eq_or_eq_of_isLink_of_isLink (e := e) (x := t) (y := w) (v := v) (w := w)) (G.G.isLink_comm.1 hst))
+                  intro hG
+                  simp [hG] at h
+                  simp [Ne.symm hwt] at h
+                  simp [h,hsv] at hst2
+            . simp [hsv] at hst
+              by_cases htv : t = v
+              . simp [htv] at hst
+                by_cases hlink : G.G.IsLink e s v
+                . refine And.intro ?_ ?_
+                  . exact (G.G.edge_mem_iff_exists_isLink (e := e)).2 ⟨s, v, hlink⟩
+                  . simp
+                    have h := ((G.G.eq_or_eq_of_isLink_of_isLink (e := e) (x := s) (y := v) (v := w) (w := v)) hlink)
+                    simp [G.G.isLink_comm] at h
+                    intro hG
+                    simp [hG] at h
+                    simp [Ne.symm hws, hsv] at h
+                . simp [hlink] at hst
+                  refine And.intro ?_ ?_
+                  . exact (G.G.edge_mem_iff_exists_isLink (e := e)).2 ⟨s, w, hst⟩
+                  . simp
+                    have h := ((G.G.eq_or_eq_of_isLink_of_isLink (e := e) (x := s) (y := w) (v := w) (w := v)) hst)
+                    intro hG
+                    simp [G.G.isLink_comm] at h
+                    simp [hG] at h
+                    simp [Ne.symm hws, hsv] at h
+              . simp [htv] at hst
+                refine And.intro ?_ ?_
+                . exact (G.G.edge_mem_iff_exists_isLink (e := e)).2 ⟨s, t, hst⟩
+                . simp
+                  have h := ((G.G.eq_or_eq_of_isLink_of_isLink (e := e) (x := s) (y := t) (v := v) (w := w)) hst)
+                  intro hG
+                  simp [hG] at h
+                  simp [Ne.symm hws, hsv] at h
+  . intro e x y h
+    by_cases hwx : w = x
+    . simp [hwx] at h
+    . by_cases hwy : w = y
+      . simp [hwy] at h
+      . by_cases hxy : x = y
+        . simp [hxy] at h
+        . simp [hwx,hwy,hxy] at h
+          by_cases hxv : x = v
+          . simp [hxv] at hwx
+            simp [hxv, hv, Ne.symm hwx]
+          . simp [hxv] at h
+            by_cases hyv : y = v
+            . simp [hyv] at h
+              by_cases hlink : G.G.IsLink e x v
+              . simp [Ne.symm hwx]
+                exact Graph.IsLink.left_mem (h := hlink)
+              . simp [hlink] at h
+                simp [Ne.symm hwx]
+                exact Graph.IsLink.left_mem (h := h)
+            . simp [hyv] at h
+              simp [Ne.symm hwx]
+              exact Graph.IsLink.left_mem (h := h)
+
+noncomputable def SingleLegContractionTensorNetwork {α β: Type*} [Fintype α] [DecidableEq α] [Fintype β] (G : TensorNetwork α β) (loopless : ∀ (e : β) (x : α), ¬ G.G.IsLoopAt e x) (v w : α) (hv : v ∈ G.G.vertexSet) (hvw : ¬v = w):
+  TensorNetwork (α := α) (β := β) := by
+  classical
+  let G' := SingleLegContractionGraph (G := G) (loopless := loopless) (v := v) (w := w) (hv := hv) (hvw := hvw)
+  refine
+  { G := G'
+    loc := ?_         -- the fintype instance field
+    loopless := ?_
+    c := ?_
+    hc := ?_ }
+  . intro x
+    classical
+    infer_instance    -- usually works if β is fintype and IsLink is decidable enough
+  . intro e x
+    simp [G', SingleLegContractionGraph]
+    intro h
+    apply Graph.isLink_self_iff.2 at h
+    rcases h with ⟨hneq, _⟩
+    exact hneq.2.2 rfl
+  . intro x
+    exact (Fintype.equivFin (G'.incidenceSet x)).1
+  . intro x
+    exact (Fintype.equivFin (G'.incidenceSet x)).bijective
+
+noncomputable def SingleLegContractionTensorMap {α β: Type*} [Fintype α] [DecidableEq α] [Fintype β] {G : TensorNetwork α β} (T : TensorMap (V := V) G) (loopless : ∀ (e : β) (x : α), ¬ G.G.IsLoopAt e x) (v w : α) (hv : v ∈ G.G.vertexSet) (hvw : ¬v = w):
+  TensorMap (V := V) (G := SingleLegContractionTensorNetwork (loopless := loopless) (v := v) (w := w) (hv := hv) (hvw := hvw)):= by
+  classical
+  let G' := SingleLegContractionTensorNetwork (loopless := loopless) (v := v) (w := w) (hv := hv) (hvw := hvw)
+  let E : Set β := { e | e ∈ G.G.edgeSet ∧ G.G.IsLink e v w }
+  haveI : Fintype (↑(G.G.incidenceSet v)) := G.loc v
+  let φ : (↑E) → ↑(G.G.incidenceSet v) := fun e =>
+    ⟨(e : β), by
+      have hw : G.G.IsLink (e : β) v w := by simpa [E] using e.2.2
+      exact ⟨w, hw⟩⟩
+  have hφ : Function.Injective φ := by
+    intro a b hab
+    apply Subtype.ext
+    simpa [φ] using congrArg Subtype.val hab
+  have hcard_le : Fintype.card (↑E) ≤ Fintype.card (↑(G.G.incidenceSet v)) :=
+    Fintype.card_le_of_injective φ hφ
+  have hcard_le_deg_v : Fintype.card (↑E) ≤ TensorNetwork.deg (G := G) v := by
+    -- deg is card of incidenceSet, and hcard_le is already in that form
+    simpa [TensorNetwork.deg] using hcard_le
+
+  refine
+  {
+    tensor := ?_
+  }
+  . intro x
+    by_cases hxw : x = w
+    . simp [hxw]
+      simp [SingleLegContractionTensorNetwork]
+      have hfilter_empty : Finset.filter (fun e => e ∈ (G'.G.incidenceSet w)) Finset.univ = (∅ : Finset β) := by
+        ext e
+        simp [Graph.incidenceSet]
+      simp [hfilter_empty]  -- goal becomes ⊢ ⨂[ℝ]^0 V
+      exact 0
+    . by_cases hxv : x = v
+      . simp [hxv]
+        simp [SingleLegContractionTensorNetwork]
+        have Tk' : ⨂[ℝ]^(G.deg v) V := by
+          simpa [TensorNetwork.deg] using (T.tensor v)
+        have Tl' : ⨂[ℝ]^(G.deg w) V := by
+          simpa [TensorNetwork.deg] using (T.tensor w)
+        let Rel : { e : β // e ∈ G.G.edgeSet ∧ G.G.IsLink e v w } → ℕ × ℕ := fun e =>
+          (G.c v ⟨e.1, ⟨w, e.2.2⟩⟩, G.c w ⟨e.1, ⟨v, ((G.G.isLink_symm (e := e) (x := v) (y := w)) e.2.1) e.2.2⟩⟩)
+        let R : Set (ℕ × ℕ) := Set.image Rel Set.univ
+
+        have Tvw : ⨂[ℝ]^(G.deg v + G.deg w) V :=
+          (TensorContraction (V := V) (k := G.deg v) (l := G.deg w) (m := m) R hR hInjfst hInjsnd f) Tk' Tl'
diff --git a/lake-manifest.json b/lake-manifest.json
index eb4351f9b..f98bdfdb5 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,27 +5,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "79e94a093aff4a60fb1b1f92d9681e407124c2ca",
+   "rev": "2df2f0150c275ad53cb3c90f7c98ec15a56a1a67",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "v4.26.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b100ad4c5d74a464f497aaa8e7c74d86bf39a56f",
+   "rev": "160af9e8e7d4ae448f3c92edcc5b6a8522453f11",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
+   "rev": "3591c3f664ac3719c4c86e4483e21e228707bfa2",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,60 +35,60 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "eb164a46de87078f27640ee71e6c3841defc2484",
+   "rev": "e9f31324f15ead11048b1443e62c5deaddd055d2",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1253a071e6939b0faf5c09d2b30b0bfc79dae407",
+   "rev": "b4fb2aa5290ebf61bc5f80a5375ba642f0a49192",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.68",
+   "inputRev": "v0.0.83",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1256a18522728c2eeed6109b02dd2b8f207a2a3c",
+   "rev": "2f6d238744c4cb07fdc91240feaf5d4221a27931",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "917bfa5064b812b7fbd7112d018ea0b4def25ab3",
+   "rev": "9312503909aa8e8bb392530145cc1677a6298574",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "240676e9568c254a69be94801889d4b13f3b249f",
+   "rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.22.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "c682c91d2d4dd59a7187e2ab977ac25bd1f87329",
+   "rev": "933fce7e893f65969714c60cdb4bd8376786044e",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.26.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "formal_conjectures",
diff --git a/lakefile.lean b/lakefile.lean
index 042b8326a..fab0e8499 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -30,4 +30,4 @@ lean_lib FormalConjectures where
   roots := #[`FormalConjectures]
   globs := #[.submodules `FormalConjectures]
 
-require "leanprover-community" / "mathlib" @ git "v4.22.0"
+require "leanprover-community" / "mathlib" @ git "v4.26.0"
diff --git a/lean-toolchain b/lean-toolchain
index 6ac6d4c4c..e59446d59 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.22.0
+leanprover/lean4:v4.26.0