diff --git a/Mathlib/Algebra/Lie/Loop.lean b/Mathlib/Algebra/Lie/Loop.lean
index 52d448747dc5b4..de0f5b65f7348b 100644
--- a/Mathlib/Algebra/Lie/Loop.lean
+++ b/Mathlib/Algebra/Lie/Loop.lean
@@ -7,8 +7,11 @@ module
 
 public import Mathlib.Algebra.Group.EvenFunction
 public import Mathlib.Algebra.Lie.Cochain
+public import Mathlib.Algebra.Lie.Graded
 public import Mathlib.Algebra.Lie.InvariantForm
+public import Mathlib.Algebra.MonoidAlgebra.Grading
 public import Mathlib.Algebra.Polynomial.Laurent
+public import Mathlib.LinearAlgebra.TensorProduct.Decomposition
 
 /-!
 # Loop Lie algebras and their central extensions
@@ -70,6 +73,43 @@ def loopAlgebraEquivLaurent :
 
 namespace LoopAlgebra
 
+noncomputable instance [DecidableEq A] [AddCommMonoid A] :
+    GradedLieAlgebra (fun (a : A) ↦ (DirectSum.decomposeTensor
+      (fun b ↦ AddMonoidAlgebra.grade R b) L a)) where
+  bracket_mem i j xi xj hi hj := by
+    rw [DirectSum.decomposeTensor_apply] at hi hj ⊢
+    obtain ⟨xi, hxi⟩ := hi
+    obtain ⟨xj, hxj⟩ := hj
+    rw [← hxi, ← hxj]
+    clear hxi hxj
+    induction xi using TensorProduct.induction_on with
+    | zero => simp
+    | tmul x y =>
+      simp only [LinearMap.rTensor_tmul, Submodule.subtype_apply]
+      induction xj using TensorProduct.induction_on with
+      | zero => simp
+      | tmul u v =>
+        obtain ⟨x, hx⟩ := x
+        obtain ⟨u, hu⟩ := u
+        use ⟨x * u, SetLike.mul_mem_graded hx hu⟩ ⊗ₜ ⁅y, v⁆
+        simp
+      | add u v hu hv =>
+        rw [LinearMap.map_add, lie_add]
+        obtain ⟨u', hu'⟩ := hu
+        obtain ⟨v', hv'⟩ := hv
+        use u' + v'
+        simp [← hu', ← hv']
+    | add x y hx hy =>
+      rw [LinearMap.map_add, add_lie]
+      obtain ⟨u, hu⟩ := hx
+      obtain ⟨v, hv⟩ := hy
+      use u + v
+      simp [← hu, ← hv]
+  decompose' :=
+    (DirectSum.tensorDecomposition (fun (a : A) ↦ AddMonoidAlgebra.grade R a) L).decompose'
+  left_inv := (DirectSum.tensorDecomposition _ L).left_inv
+  right_inv := (DirectSum.tensorDecomposition _ L).right_inv
+
 open scoped Classical in
 /-- A linear isomorphism to finitely supported functions. -/
 def toFinsupp : loopAlgebra R A L ≃ₗ[R] A →₀ L :=
diff --git a/Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean b/Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean
index c881518d4189a0..ad785d4e31d16e 100644
--- a/Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean
+++ b/Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean
@@ -116,6 +116,14 @@ lemma directSumLeft_tmul (m : ⨁ i, M₁ i) (n : M₂') (i : ι₁) :
   · subst hj; simp
   · simp [DirectSum.component.of, hj]
 
+lemma directSumLeft_symm_of {i : ι₁} (x : (M₁ i) ⊗[R] M₂') :
+    (directSumLeft R S M₁ M₂').symm ((of (fun i ↦ M₁ i ⊗[R] M₂') i) x) =
+      rTensor M₂' (lof S ι₁ M₁ i) x := by
+  induction x using TensorProduct.induction_on with
+  | zero => simp
+  | tmul x y => simp [LinearEquiv.symm_apply_eq]; simp [lof_eq_of]
+  | add x y h₁ h₂ => simp [h₁, h₂]
+
 @[simp]
 theorem directSumRight_tmul_lof (x : M₁') (i : ι₂) (y : M₂ i) :
     directSumRight R S M₁' M₂ (x ⊗ₜ[R] DirectSum.lof R _ _ i y) =
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Decomposition.lean b/Mathlib/LinearAlgebra/TensorProduct/Decomposition.lean
index 19034038b799ec..aeb3b1507e7672 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Decomposition.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Decomposition.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kenny Lau
+Authors: Kenny Lau, Scott Carnahan
 -/
 module
 
@@ -10,9 +10,13 @@ public import Mathlib.LinearAlgebra.DirectSum.TensorProduct
 
 /-! # Decomposition of tensor product
 
-In this file we show that if `ℳ` is a decomposition of an `R`-module `M` indexed by a type `ι`,
-then the `S`-module `S ⊗[R] M` has a decomposition `fun i ↦ (ℳ i).baseChange S` indexed by the
-same `ι`.
+In this file, we describe the properties of decomposition under tensor product. Suppose `ℳ` is a
+decomposition of an `R`-module `M` indexed by a type `ι`. Given an `R`-module `N`, the `R`-module
+`M ⊗[R] N` has a decomposition into pieces `fun i ↦ (ℳ i) ⊗[R] N`. Given a commutative `R`-algebra
+`S`, the `S`-module `S ⊗[R] M` has a decomposition `fun i ↦ (ℳ i).baseChange S`.
+
+## Declarations
+
 -/
 
 public section
@@ -21,13 +25,13 @@ open TensorProduct LinearMap
 
 namespace DirectSum
 
-variable {ι R M S : Type*} [DecidableEq ι]
+variable {ι R M S : Type*}
   [CommSemiring R] [AddCommMonoid M] [Module R M]
   (ℳ : ι → Submodule R M)
-  [CommSemiring S] [Algebra R S]
 
-section Decomposition
-variable [Decomposition ℳ]
+section BaseChange
+
+variable [DecidableEq ι] [Decomposition ℳ] [CommSemiring S] [Algebra R S]
 
 instance Decomposition.baseChange : Decomposition fun i ↦ (ℳ i).baseChange S := by
   refine .ofLinearMap _ (lmap (ℳ · |>.toBaseChange S) ∘ₗ
@@ -52,10 +56,84 @@ theorem toBaseChange_injective (i : ι) : Function.Injective ((ℳ i).toBaseChan
 theorem toBaseChange_bijective (i : ι) : Function.Bijective ((ℳ i).toBaseChange S) :=
   ⟨toBaseChange_injective ℳ i, (ℳ i).toBaseChange_surjective S⟩
 
-end Decomposition
+end BaseChange
+
+section TensorModule
+
+variable (N : Type*) [AddCommMonoid N] [Module R N]
+
+/-- The submodule of a tensor product corresponding to a decomposition on the left. -/
+def decomposeTensor : ι → Submodule R (M ⊗[R] N) :=
+  fun i ↦ ((ℳ i).subtype.rTensor N).range
+
+lemma decomposeTensor_apply {i : ι} :
+    decomposeTensor ℳ N i = ((ℳ i).subtype.rTensor N).range := by
+  exact Submodule.toSubMulAction_inj.mp rfl
+
+variable [DecidableEq ι] [Decomposition ℳ]
+
+lemma subtype_rTensor_injective (i : ι) :
+    Function.Injective ((ℳ i).subtype.rTensor N) :=
+  injective_of_comp_eq_id ((ℳ i).subtype.rTensor N) (((component R ι (fun i ↦ ↥(ℳ i)) i) ∘ₗ
+    (DirectSum.decomposeLinearEquiv ℳ).toLinearMap).rTensor N) (by ext; simp)
+
+/-- The linear isomorphism to the submodule from the tensor product with a summand. -/
+noncomputable def decomposeTensorEquiv (i : ι) :
+    (ℳ i) ⊗[R] N ≃ₗ[R] decomposeTensor ℳ N i :=
+  LinearEquiv.ofInjective ((ℳ i).subtype.rTensor N) (subtype_rTensor_injective ℳ N i)
+
+@[simp]
+lemma decomposeTensorEquiv_apply {i : ι} (x : (ℳ i) ⊗[R] N) :
+    decomposeTensorEquiv ℳ N i x = ((ℳ i).subtype.rTensor N) x := by rfl
+
+lemma decomposeTensorEquiv_of_apply {i : ι} (x : (ℳ i) ⊗[R] N) :
+    (congrLinearEquiv fun a ↦ decomposeTensorEquiv ℳ N a) ((of (fun i ↦ ↥(ℳ i) ⊗[R] N) i) x) =
+    (of (fun i ↦ ↥(decomposeTensor ℳ N i)) i) (decomposeTensorEquiv ℳ N i x) := by
+  ext; simp [coe_congrLinearEquiv]
+
+lemma decomposeLinearEquiv_comp_subtype {i : ι} :
+    (decomposeLinearEquiv ℳ) ∘ₗ (ℳ i).subtype = lof R ι (fun i ↦ ℳ i) i := by
+  ext; simp
+
+lemma coe_decomposeTensor_apply (x : (⨁ (i : ι), decomposeTensor ℳ N i)) :
+    (DirectSum.coeAddMonoidHom (decomposeTensor ℳ N)) x =
+    ((DirectSum.decomposeLinearEquiv ℳ).symm.rTensor N)
+    ((TensorProduct.directSumLeft R R (fun a ↦ ℳ a) N).symm
+      ((DirectSum.congrLinearEquiv fun a ↦ decomposeTensorEquiv ℳ N a).symm x)) := by
+  rw [← LinearEquiv.symm_rTensor, LinearEquiv.eq_symm_apply]
+  induction x using DirectSum.induction_on with
+  | zero => simp
+  | of i x =>
+    obtain ⟨x, y, h⟩ := x
+    simp only [← h, coeAddMonoidHom_of]
+    rw [LinearEquiv.eq_symm_apply, LinearEquiv.eq_symm_apply,
+      ← LinearEquiv.coe_coe (LinearEquiv.rTensor N _), LinearEquiv.coe_rTensor,
+      ← rTensor_comp_apply, decomposeLinearEquiv_comp_subtype]
+    have : (rTensor N (lof R ι (fun i ↦ ↥(ℳ i)) i)) y =
+        (directSumLeft R R (fun i ↦ ℳ i) N).symm ((of (fun i ↦ ℳ i ⊗[R] N) i) y) :=
+      (TensorProduct.directSumLeft_symm_of R R (M₁ := fun i ↦ ℳ i) y).symm
+    rw [this, LinearEquiv.apply_symm_apply, decomposeTensorEquiv_of_apply]
+    rfl
+  | add x y hx hy => simp [hx, hy]
+
+/-- The decomposition of a tensor product induced by a decomposition of the left module. -/
+@[reducible]
+noncomputable def tensorDecomposition (N : Type*) [AddCommGroup N] [Module R N] :
+    DirectSum.Decomposition (decomposeTensor ℳ N) where
+  decompose' x := (DirectSum.congrLinearEquiv fun a ↦ decomposeTensorEquiv ℳ N a)
+    (TensorProduct.directSumLeft R R (fun a ↦ ℳ a) N
+      ((DirectSum.decomposeLinearEquiv ℳ).rTensor N x))
+  left_inv x := by
+    simp [coe_decomposeTensor_apply ℳ N _, ← LinearEquiv.symm_rTensor]
+  right_inv x := by
+    simp [coe_decomposeTensor_apply ℳ N _, ← LinearEquiv.symm_rTensor]
+
+end TensorModule
 
 namespace IsInternal
 
+variable [DecidableEq ι] [CommSemiring S] [Algebra R S]
+
 theorem baseChange (hm : IsInternal ℳ) : IsInternal fun i ↦ (ℳ i).baseChange S :=
   haveI := hm.chooseDecomposition
   Decomposition.isInternal _
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Map.lean b/Mathlib/LinearAlgebra/TensorProduct/Map.lean
index c2f23fa7984d96..ac9e7ae0a5aafc 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Map.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Map.lean
@@ -595,21 +595,29 @@ def rTensor (f : N ≃ₗ[R] P) : N ⊗[R] M ≃ₗ[R] P ⊗[R] M := TensorProdu
 
 variable (g : P ≃ₗ[R] Q) (f : N ≃ₗ[R] P) (m : M) (n : N) (p : P) (x : M ⊗[R] N) (y : N ⊗[R] M)
 
+@[simp] theorem symm_lTensor : (f.lTensor M).symm = f.symm.lTensor M := rfl
+
+@[simp] theorem symm_rTensor : (f.rTensor M).symm = f.symm.rTensor M := rfl
+
 @[simp] theorem coe_lTensor : lTensor M f = (f : N →ₗ[R] P).lTensor M := rfl
 
-@[simp] theorem coe_lTensor_symm : (lTensor M f).symm = (f.symm : P →ₗ[R] N).lTensor M := rfl
+@[deprecated "use symm_lTensor and coe_lTensor" (since := "2026-07-04")]
+theorem coe_lTensor_symm : (lTensor M f).symm = (f.symm : P →ₗ[R] N).lTensor M := rfl
 
 @[simp] theorem coe_rTensor : rTensor M f = (f : N →ₗ[R] P).rTensor M := rfl
 
-@[simp] theorem coe_rTensor_symm : (rTensor M f).symm = (f.symm : P →ₗ[R] N).rTensor M := rfl
+@[deprecated "use symm_rTensor and coe_rTensor" (since := "2026-07-04")]
+theorem coe_rTensor_symm : (rTensor M f).symm = (f.symm : P →ₗ[R] N).rTensor M := rfl
 
 @[simp] theorem lTensor_tmul : f.lTensor M (m ⊗ₜ n) = m ⊗ₜ f n := rfl
 
-@[simp] theorem lTensor_symm_tmul : (f.lTensor M).symm (m ⊗ₜ p) = m ⊗ₜ f.symm p := rfl
+@[deprecated "use symm_lTensor and lTensor_tmul" (since := "2026-07-04")]
+theorem lTensor_symm_tmul : (f.lTensor M).symm (m ⊗ₜ p) = m ⊗ₜ f.symm p := rfl
 
 @[simp] theorem rTensor_tmul : f.rTensor M (n ⊗ₜ m) = f n ⊗ₜ m := rfl
 
-@[simp] theorem rTensor_symm_tmul : (f.rTensor M).symm (p ⊗ₜ m) = f.symm p ⊗ₜ m := rfl
+@[deprecated "use symm_rTensor and rTensor_tmul" (since := "2026-07-04")]
+theorem rTensor_symm_tmul : (f.rTensor M).symm (p ⊗ₜ m) = f.symm p ⊗ₜ m := rfl
 
 lemma comm_trans_rTensor_trans_comm_eq (g : N ≃ₗ[R] P) :
     TensorProduct.comm R Q N ≪≫ₗ rTensor Q g ≪≫ₗ TensorProduct.comm R P Q = lTensor Q g :=
diff --git a/Mathlib/RingTheory/Coalgebra/CoassocSimps.lean b/Mathlib/RingTheory/Coalgebra/CoassocSimps.lean
index 433e94131ac863..5b185e6f6f3b53 100644
--- a/Mathlib/RingTheory/Coalgebra/CoassocSimps.lean
+++ b/Mathlib/RingTheory/Coalgebra/CoassocSimps.lean
@@ -73,8 +73,8 @@ attribute [coassoc_simps] LinearMap.comp_id LinearMap.id_comp TensorProduct.map_
   LinearEquiv.coe_trans LinearEquiv.trans_symm
   LinearEquiv.refl_toLinearMap TensorProduct.toLinearMap_congr
   LinearEquiv.comp_symm LinearEquiv.symm_comp LinearEquiv.symm_symm
-  LinearEquiv.coe_lTensor LinearEquiv.coe_lTensor_symm
-  LinearEquiv.coe_rTensor LinearEquiv.coe_rTensor_symm
+  LinearEquiv.coe_lTensor LinearEquiv.symm_lTensor
+  LinearEquiv.coe_rTensor LinearEquiv.symm_rTensor
   IsCocomm.comm_comp_comul TensorProduct.AlgebraTensorModule.map_eq
   TensorProduct.AlgebraTensorModule.assoc_eq TensorProduct.AlgebraTensorModule.rightComm_eq
   TensorProduct.tensorTensorTensorComm TensorProduct.AlgebraTensorModule.tensorTensorTensorComm