p2m_TensorObj_p2

import Mathlib.LinearAlgebra.PiTensorProduct
import Mathlib.LinearAlgebra.FiniteDimensional.Basic
import Mathlib.RingTheory.TensorProduct.Finite
import Mathlib.LinearAlgebra.TensorProduct.Finiteness
import Mathlib.Logic.Basic
import Mathlib.Algebra.Module.ULift
import Mathlib.LinearAlgebra.Prod
import Mathlib.Algebra.Module.PUnit
import Mathlib.LinearAlgebra.TensorProduct.Prod
import Mathlib.LinearAlgebra.TensorProduct.Tower
import Definitions.Def_p2m_TensorObj_p1

universe u v w

open BigOperators TensorProduct
open PiTensorProduct

set_option maxHeartbeats 1000000

open TensorObj

namespace TensorObj

variable {K : Type u} [Field K] {d : ℕ} [Fact (1 < d)]


/-- Addition respects mutual restriction. -/
theorem add_isomorphic {X Y Z W : TensorObj K d}
    (h1 : Restrict X Y ∧ Restrict Y X) (h2 : Restrict Z W ∧ Restrict W Z) :
    Restrict (X + Z) (Y + W) ∧ Restrict (Y + W) (X + Z) := by
  obtain ⟨⟨f, hf⟩, ⟨f', hf'⟩⟩ := h1
  obtain ⟨⟨g, hg⟩, ⟨g', hg'⟩⟩ := h2
  constructor
  · refine ⟨fun i => LinearMap.prodMap (f i) (g i), ?_⟩
    simp only [add_t]
    have h1 : (fun i => LinearMap.prodMap (f i) (g i) ∘ₗ LinearMap.inl K (Y.V i) (W.V i)) =
              (fun i => LinearMap.inl K (X.V i) (Z.V i) ∘ₗ f i) := by
      funext i; ext x <;> simp [LinearMap.prodMap]
    have h2 : (fun i => LinearMap.prodMap (f i) (g i) ∘ₗ LinearMap.inr K (Y.V i) (W.V i)) =
              (fun i => LinearMap.inr K (X.V i) (Z.V i) ∘ₗ g i) := by
      funext i; ext x <;> simp [LinearMap.prodMap]
    have key : (liftMap (fun i => (f i).prodMap (g i)))
        ((liftMap (fun i => LinearMap.inl K (Y.V i) (W.V i))) Y.t +
         (liftMap (fun i => LinearMap.inr K (Y.V i) (W.V i))) W.t) =
        (liftMap (fun i => LinearMap.inl K (X.V i) (Z.V i))) X.t +
        (liftMap (fun i => LinearMap.inr K (X.V i) (Z.V i))) Z.t := by
      rw [(liftMap _).map_add, liftMap_comp, liftMap_comp, h1, h2, ← liftMap_comp, ← liftMap_comp, hf, hg]
    exact key
  · refine ⟨fun i => LinearMap.prodMap (f' i) (g' i), ?_⟩
    simp only [add_t]
    have h1 : (fun i => LinearMap.prodMap (f' i) (g' i) ∘ₗ LinearMap.inl K (X.V i) (Z.V i)) =
              (fun i => LinearMap.inl K (Y.V i) (W.V i) ∘ₗ f' i) := by
      funext i; ext x <;> simp [LinearMap.prodMap]
    have h2 : (fun i => LinearMap.prodMap (f' i) (g' i) ∘ₗ LinearMap.inr K (X.V i) (Z.V i)) =
              (fun i => LinearMap.inr K (Y.V i) (W.V i) ∘ₗ g' i) := by
      funext i; ext x <;> simp [LinearMap.prodMap]
    have key : (liftMap (fun i => (f' i).prodMap (g' i)))
        ((liftMap (fun i => LinearMap.inl K (X.V i) (Z.V i))) X.t +
         (liftMap (fun i => LinearMap.inr K (X.V i) (Z.V i))) Z.t) =
        (liftMap (fun i => LinearMap.inl K (Y.V i) (W.V i))) Y.t +
        (liftMap (fun i => LinearMap.inr K (Y.V i) (W.V i))) W.t := by
      rw [(liftMap _).map_add, liftMap_comp, liftMap_comp, h1, h2, ← liftMap_comp, ← liftMap_comp, hf', hg']
    exact key

/-- Helper: liftMap with a linear equiv applied to a sum of inl/inr. -/
private theorem add_comm_restrict (X Y : TensorObj K d) :
    Restrict (X + Y) (Y + X) :=
  ⟨fun i => (prodComm : (Y.V i × X.V i) ≃ₗ[K] (X.V i × Y.V i)).toLinearMap, by
    simp only [add_t]
    have h1 : (fun i => (prodComm : (Y.V i × X.V i) ≃ₗ[K] _).toLinearMap ∘ₗ LinearMap.inl K (Y.V i) (X.V i)) =
              fun i => LinearMap.inr K (X.V i) (Y.V i) := by
      funext i; ext x <;> simp [prodComm]
    have h2 : (fun i => (prodComm : (Y.V i × X.V i) ≃ₗ[K] _).toLinearMap ∘ₗ LinearMap.inr K (Y.V i) (X.V i)) =
              fun i => LinearMap.inl K (X.V i) (Y.V i) := by
      funext i; ext x <;> simp [prodComm]
    erw [(liftMap _).map_add, liftMap_comp, liftMap_comp, h1, h2]
    exact add_comm _ _⟩

theorem add_comm_isomorphic {X Y : TensorObj K d} :
    Restrict (X + Y) (Y + X) ∧ Restrict (Y + X) (X + Y) :=
  ⟨add_comm_restrict X Y, add_comm_restrict Y X⟩

private theorem add_assoc_restrict_aux (X Y Z : TensorObj K d)
    (x : PiTensorProduct K X.V) (y : PiTensorProduct K Y.V) (z : PiTensorProduct K Z.V) :
    (liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).symm.toLinearMap))
      (liftMap (fun i => LinearMap.inl K (X.V i) ((Y + Z).V i)) x +
       liftMap (fun i => LinearMap.inr K (X.V i) ((Y + Z).V i))
         (liftMap (fun i => LinearMap.inl K (Y.V i) (Z.V i)) y +
          liftMap (fun i => LinearMap.inr K (Y.V i) (Z.V i)) z)) =
    liftMap (fun i => LinearMap.inl K ((X + Y).V i) (Z.V i))
      (liftMap (fun i => LinearMap.inl K (X.V i) (Y.V i)) x +
       liftMap (fun i => LinearMap.inr K (X.V i) (Y.V i)) y) +
    liftMap (fun i => LinearMap.inr K ((X + Y).V i) (Z.V i)) z := by
  -- Direct induction: hA/hB/hC without liftMap_comp.
  -- hA: prodAssoc.symm (inl_X_YZ x) = inl_XY_Z (inl_X_Y x)
  -- hB: prodAssoc.symm (inr_X_YZ (inl_Y_Z y)) = inl_XY_Z (inr_X_Y y)
  -- hC: prodAssoc.symm (inr_X_YZ (inr_Y_Z z)) = inr_XY_Z z
  have hA : ∀ t : PiTensorProduct K X.V,
      liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).symm.toLinearMap)
        (liftMap (fun i => LinearMap.inl K (X.V i) ((Y + Z).V i)) t) =
      liftMap (fun i => LinearMap.inl K ((X + Y).V i) (Z.V i))
        (liftMap (fun i => LinearMap.inl K (X.V i) (Y.V i)) t) := by
    suffices h : ∀ t : PiTensorProduct K X.V,
        liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).symm.toLinearMap)
          (liftMap (fun i => LinearMap.inl K (X.V i) (Y.V i × Z.V i)) t) =
        liftMap (fun i => LinearMap.inl K (X.V i × Y.V i) (Z.V i))
          (liftMap (fun i => LinearMap.inl K (X.V i) (Y.V i)) t) from h
    intro t; induction t using PiTensorProduct.induction_on with
    | smul_tprod c v =>
        simp only [liftMap, PiTensorProduct.lift.tprod, LinearEquiv.prodAssoc, map_smul]; rfl
    | add t1 t2 ih1 ih2 => simp only [map_add, ih1, ih2]
  have hB : ∀ t : PiTensorProduct K Y.V,
      liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).symm.toLinearMap)
        (liftMap (fun i => LinearMap.inr K (X.V i) ((Y + Z).V i))
          (liftMap (fun i => LinearMap.inl K (Y.V i) (Z.V i)) t)) =
      liftMap (fun i => LinearMap.inl K ((X + Y).V i) (Z.V i))
        (liftMap (fun i => LinearMap.inr K (X.V i) (Y.V i)) t) := by
    suffices h : ∀ t : PiTensorProduct K Y.V,
        liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).symm.toLinearMap)
          (liftMap (fun i => LinearMap.inr K (X.V i) (Y.V i × Z.V i))
            (liftMap (fun i => LinearMap.inl K (Y.V i) (Z.V i)) t)) =
        liftMap (fun i => LinearMap.inl K (X.V i × Y.V i) (Z.V i))
          (liftMap (fun i => LinearMap.inr K (X.V i) (Y.V i)) t) from h
    intro t; induction t using PiTensorProduct.induction_on with
    | smul_tprod c v =>
        simp [liftMap, PiTensorProduct.lift.tprod, LinearEquiv.prodAssoc, map_smul,
              MultilinearMap.compLinearMap_apply, LinearMap.inl_apply, LinearMap.inr_apply]
    | add t1 t2 ih1 ih2 => simp only [map_add, ih1, ih2]
  have hC : ∀ t : PiTensorProduct K Z.V,
      liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).symm.toLinearMap)
        (liftMap (fun i => LinearMap.inr K (X.V i) ((Y + Z).V i))
          (liftMap (fun i => LinearMap.inr K (Y.V i) (Z.V i)) t)) =
      liftMap (fun i => LinearMap.inr K ((X + Y).V i) (Z.V i)) t := by
    suffices h : ∀ t : PiTensorProduct K Z.V,
        liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).symm.toLinearMap)
          (liftMap (fun i => LinearMap.inr K (X.V i) (Y.V i × Z.V i))
            (liftMap (fun i => LinearMap.inr K (Y.V i) (Z.V i)) t)) =
        liftMap (fun i => LinearMap.inr K (X.V i × Y.V i) (Z.V i)) t from h
    intro t; induction t using PiTensorProduct.induction_on with
    | smul_tprod c v =>
        simp [liftMap, PiTensorProduct.lift.tprod, MultilinearMap.compLinearMap_apply,
              LinearMap.inr_apply, LinearEquiv.prodAssoc]; norm_cast
    | add t1 t2 ih1 ih2 => simp only [map_add, ih1, ih2]
  -- apply hA/hB/hC by linearity
  have step1 : (liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).symm.toLinearMap))
      (liftMap (fun i => LinearMap.inl K (X.V i) ((Y + Z).V i)) x +
       liftMap (fun i => LinearMap.inr K (X.V i) ((Y + Z).V i))
         (liftMap (fun i => LinearMap.inl K (Y.V i) (Z.V i)) y +
          liftMap (fun i => LinearMap.inr K (Y.V i) (Z.V i)) z)) =
      liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).symm.toLinearMap)
        (liftMap (fun i => LinearMap.inl K (X.V i) ((Y + Z).V i)) x) +
      liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).symm.toLinearMap)
        (liftMap (fun i => LinearMap.inr K (X.V i) ((Y + Z).V i))
          (liftMap (fun i => LinearMap.inl K (Y.V i) (Z.V i)) y +
           liftMap (fun i => LinearMap.inr K (Y.V i) (Z.V i)) z)) :=
    (liftMap _).map_add _ _
  have step2 : liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).symm.toLinearMap)
      (liftMap (fun i => LinearMap.inr K (X.V i) ((Y + Z).V i))
        (liftMap (fun i => LinearMap.inl K (Y.V i) (Z.V i)) y +
         liftMap (fun i => LinearMap.inr K (Y.V i) (Z.V i)) z)) =
      liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).symm.toLinearMap)
        (liftMap (fun i => LinearMap.inr K (X.V i) ((Y + Z).V i))
          (liftMap (fun i => LinearMap.inl K (Y.V i) (Z.V i)) y)) +
      liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).symm.toLinearMap)
        (liftMap (fun i => LinearMap.inr K (X.V i) ((Y + Z).V i))
          (liftMap (fun i => LinearMap.inr K (Y.V i) (Z.V i)) z)) := by
    have hmid : liftMap (fun i => LinearMap.inr K (X.V i) ((Y + Z).V i))
        (liftMap (fun i => LinearMap.inl K (Y.V i) (Z.V i)) y +
         liftMap (fun i => LinearMap.inr K (Y.V i) (Z.V i)) z) =
        liftMap (fun i => LinearMap.inr K (X.V i) ((Y + Z).V i))
          (liftMap (fun i => LinearMap.inl K (Y.V i) (Z.V i)) y) +
        liftMap (fun i => LinearMap.inr K (X.V i) ((Y + Z).V i))
          (liftMap (fun i => LinearMap.inr K (Y.V i) (Z.V i)) z) :=
      (liftMap _).map_add _ _
    rw [hmid]
    exact (liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).symm.toLinearMap)).map_add _ _
  have step3 : liftMap (fun i => LinearMap.inl K ((X + Y).V i) (Z.V i))
      (liftMap (fun i => LinearMap.inl K (X.V i) (Y.V i)) x +
       liftMap (fun i => LinearMap.inr K (X.V i) (Y.V i)) y) =
      liftMap (fun i => LinearMap.inl K ((X + Y).V i) (Z.V i))
        (liftMap (fun i => LinearMap.inl K (X.V i) (Y.V i)) x) +
      liftMap (fun i => LinearMap.inl K ((X + Y).V i) (Z.V i))
        (liftMap (fun i => LinearMap.inr K (X.V i) (Y.V i)) y) :=
    (liftMap _).map_add _ _
  rw [step1, step2, hA, hB, hC, step3]
  abel

private theorem add_assoc_restrict (X Y Z : TensorObj K d) :
    Restrict (X + Y + Z) (X + (Y + Z)) :=
  ⟨fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).symm.toLinearMap, by
    simp only [add_t]
    exact add_assoc_restrict_aux X Y Z X.t Y.t Z.t⟩

-- Auxiliary: liftMap prodAssoc on add_t = add_t rearranged (symmetric to add_assoc_restrict_aux)
private theorem add_assoc_bwd_aux (X Y Z : TensorObj K d)
    (x : PiTensorProduct K X.V) (y : PiTensorProduct K Y.V) (z : PiTensorProduct K Z.V) :
    (liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).toLinearMap))
      (liftMap (fun i => LinearMap.inl K ((X + Y).V i) (Z.V i))
        (liftMap (fun i => LinearMap.inl K (X.V i) (Y.V i)) x +
         liftMap (fun i => LinearMap.inr K (X.V i) (Y.V i)) y) +
       liftMap (fun i => LinearMap.inr K ((X + Y).V i) (Z.V i)) z) =
    liftMap (fun i => LinearMap.inl K (X.V i) ((Y + Z).V i)) x +
    liftMap (fun i => LinearMap.inr K (X.V i) ((Y + Z).V i))
      (liftMap (fun i => LinearMap.inl K (Y.V i) (Z.V i)) y +
       liftMap (fun i => LinearMap.inr K (Y.V i) (Z.V i)) z) := by
  -- Direct induction: hA'/hB'/hC' without liftMap_comp.
  have hA' : ∀ t : PiTensorProduct K X.V,
      liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).toLinearMap)
        (liftMap (fun i => LinearMap.inl K ((X + Y).V i) (Z.V i))
          (liftMap (fun i => LinearMap.inl K (X.V i) (Y.V i)) t)) =
      liftMap (fun i => LinearMap.inl K (X.V i) ((Y + Z).V i)) t := by
    suffices h : ∀ t : PiTensorProduct K X.V,
        liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).toLinearMap)
          (liftMap (fun i => LinearMap.inl K (X.V i × Y.V i) (Z.V i))
            (liftMap (fun i => LinearMap.inl K (X.V i) (Y.V i)) t)) =
        liftMap (fun i => LinearMap.inl K (X.V i) (Y.V i × Z.V i)) t from h
    intro t; induction t using PiTensorProduct.induction_on with
    | smul_tprod c v =>
        simp only [liftMap, PiTensorProduct.lift.tprod, LinearEquiv.prodAssoc, map_smul,
                   MultilinearMap.compLinearMap_apply, LinearMap.inl_apply]; rfl
    | add t1 t2 ih1 ih2 => simp only [map_add, ih1, ih2]
  have hB' : ∀ t : PiTensorProduct K Y.V,
      liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).toLinearMap)
        (liftMap (fun i => LinearMap.inl K ((X + Y).V i) (Z.V i))
          (liftMap (fun i => LinearMap.inr K (X.V i) (Y.V i)) t)) =
      liftMap (fun i => LinearMap.inr K (X.V i) ((Y + Z).V i))
        (liftMap (fun i => LinearMap.inl K (Y.V i) (Z.V i)) t) := by
    suffices h : ∀ t : PiTensorProduct K Y.V,
        liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).toLinearMap)
          (liftMap (fun i => LinearMap.inl K (X.V i × Y.V i) (Z.V i))
            (liftMap (fun i => LinearMap.inr K (X.V i) (Y.V i)) t)) =
        liftMap (fun i => LinearMap.inr K (X.V i) (Y.V i × Z.V i))
          (liftMap (fun i => LinearMap.inl K (Y.V i) (Z.V i)) t) from h
    intro t; induction t using PiTensorProduct.induction_on with
    | smul_tprod c v =>
        simp [liftMap, PiTensorProduct.lift.tprod, MultilinearMap.compLinearMap_apply,
              LinearMap.inl_apply, LinearMap.inr_apply, LinearEquiv.prodAssoc]
    | add t1 t2 ih1 ih2 => simp only [map_add, ih1, ih2]
  have hC' : ∀ t : PiTensorProduct K Z.V,
      liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).toLinearMap)
        (liftMap (fun i => LinearMap.inr K ((X + Y).V i) (Z.V i)) t) =
      liftMap (fun i => LinearMap.inr K (X.V i) ((Y + Z).V i))
        (liftMap (fun i => LinearMap.inr K (Y.V i) (Z.V i)) t) := by
    suffices h : ∀ t : PiTensorProduct K Z.V,
        liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).toLinearMap)
          (liftMap (fun i => LinearMap.inr K (X.V i × Y.V i) (Z.V i)) t) =
        liftMap (fun i => LinearMap.inr K (X.V i) (Y.V i × Z.V i))
          (liftMap (fun i => LinearMap.inr K (Y.V i) (Z.V i)) t) from h
    intro t; induction t using PiTensorProduct.induction_on with
    | smul_tprod c v =>
        simp only [liftMap, PiTensorProduct.lift.tprod, LinearEquiv.prodAssoc, map_smul]; rfl
    | add t1 t2 ih1 ih2 => simp only [map_add, ih1, ih2]
  have step1' : (liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).toLinearMap))
      (liftMap (fun i => LinearMap.inl K ((X + Y).V i) (Z.V i))
        (liftMap (fun i => LinearMap.inl K (X.V i) (Y.V i)) x +
         liftMap (fun i => LinearMap.inr K (X.V i) (Y.V i)) y) +
       liftMap (fun i => LinearMap.inr K ((X + Y).V i) (Z.V i)) z) =
      liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).toLinearMap)
        (liftMap (fun i => LinearMap.inl K ((X + Y).V i) (Z.V i))
          (liftMap (fun i => LinearMap.inl K (X.V i) (Y.V i)) x +
           liftMap (fun i => LinearMap.inr K (X.V i) (Y.V i)) y)) +
      liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).toLinearMap)
        (liftMap (fun i => LinearMap.inr K ((X + Y).V i) (Z.V i)) z) :=
    (liftMap _).map_add _ _
  have step2' : liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).toLinearMap)
      (liftMap (fun i => LinearMap.inl K ((X + Y).V i) (Z.V i))
        (liftMap (fun i => LinearMap.inl K (X.V i) (Y.V i)) x +
         liftMap (fun i => LinearMap.inr K (X.V i) (Y.V i)) y)) =
      liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).toLinearMap)
        (liftMap (fun i => LinearMap.inl K ((X + Y).V i) (Z.V i))
          (liftMap (fun i => LinearMap.inl K (X.V i) (Y.V i)) x)) +
      liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).toLinearMap)
        (liftMap (fun i => LinearMap.inl K ((X + Y).V i) (Z.V i))
          (liftMap (fun i => LinearMap.inr K (X.V i) (Y.V i)) y)) := by
    have hmid' : liftMap (fun i => LinearMap.inl K ((X + Y).V i) (Z.V i))
        (liftMap (fun i => LinearMap.inl K (X.V i) (Y.V i)) x +
         liftMap (fun i => LinearMap.inr K (X.V i) (Y.V i)) y) =
        liftMap (fun i => LinearMap.inl K ((X + Y).V i) (Z.V i))
          (liftMap (fun i => LinearMap.inl K (X.V i) (Y.V i)) x) +
        liftMap (fun i => LinearMap.inl K ((X + Y).V i) (Z.V i))
          (liftMap (fun i => LinearMap.inr K (X.V i) (Y.V i)) y) :=
      (liftMap _).map_add _ _
    rw [hmid']
    exact (liftMap (fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).toLinearMap)).map_add _ _
  have step3' : liftMap (fun i => LinearMap.inr K (X.V i) ((Y + Z).V i))
      (liftMap (fun i => LinearMap.inl K (Y.V i) (Z.V i)) y +
       liftMap (fun i => LinearMap.inr K (Y.V i) (Z.V i)) z) =
      liftMap (fun i => LinearMap.inr K (X.V i) ((Y + Z).V i))
        (liftMap (fun i => LinearMap.inl K (Y.V i) (Z.V i)) y) +
      liftMap (fun i => LinearMap.inr K (X.V i) ((Y + Z).V i))
        (liftMap (fun i => LinearMap.inr K (Y.V i) (Z.V i)) z) :=
    (liftMap _).map_add _ _
  rw [step1', step2', hA', hB', hC', step3']
  abel

theorem add_assoc_isomorphic {X Y Z : TensorObj K d} :
    Restrict (X + Y + Z) (X + (Y + Z)) ∧ Restrict (X + (Y + Z)) (X + Y + Z) :=
  ⟨add_assoc_restrict X Y Z,
   ⟨fun i => (LinearEquiv.prodAssoc K (X.V i) (Y.V i) (Z.V i)).toLinearMap, by
    simp only [add_t]
    exact add_assoc_bwd_aux X Y Z X.t Y.t Z.t⟩⟩


end TensorObj