feat(Analysis/InnerProductSpace/TensorProduct): add TensorProduct.congrL

Mathlib/Analysis/InnerProductSpace/TensorProduct.lean

@@ -8,6 +8,9 @@ module
 public import Mathlib.Analysis.InnerProductSpace.Adjoint
 public import Mathlib.LinearAlgebra.TensorProduct.Finiteness
 public import Mathlib.RingTheory.TensorProduct.Finite
+import Mathlib.Analysis.InnerProductSpace.GramMatrix
+import Mathlib.Analysis.InnerProductSpace.Positive
+import Mathlib.Topology.Algebra.Module.Equiv
 
 /-!
 
@@ -32,13 +35,14 @@ inner product spaces.
 * `TensorProduct.commIsometry`: the linear isometry version of `TensorProduct.comm`.
 * `TensorProduct.lidIsometry`: the linear isometry version of `TensorProduct.lid`.
 * `TensorProduct.assocIsometry`: the linear isometry version of `TensorProduct.assoc`.
+* `TensorProduct.mapL`: the continuous version of `TensorProduct.map f g` when
+  `f` and `g` are continuous linear maps.
+  `TensorProduct.congrL f g` the continuous version of `TensorProduct.congr f g`.
 * `OrthonormalBasis.tensorProduct`: the orthonormal basis of the tensor product of two orthonormal
   bases.
 
 ## TODO:
 
-* Define the continuous linear map version of `TensorProduct.map`.
-* Complete space of tensor products.
 * Define the normed space without needing inner products, this should be analogous to
   `Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean`.
 
@@ -409,21 +413,325 @@ noncomputable def assocIsometry : E ⊗[𝕜] F ⊗[𝕜] G ≃ₗᵢ[𝕜] E 
 
 end isometry
 
--- TODO: upgrade `map` to a `ContinuousLinearMap`
-@[simp] theorem adjoint_map [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G]
-    [FiniteDimensional 𝕜 H] (f : E →ₗ[𝕜] F) (g : G →ₗ[𝕜] H) :
-    LinearMap.adjoint (map f g) = map (LinearMap.adjoint f) (LinearMap.adjoint g) :=
-  ext' fun _ _ => by simp [TensorProduct.ext_iff_inner_right, LinearMap.adjoint_inner_left]
+end TensorProduct
+
+namespace ContinuousLinearMap
+
+open TensorProduct
+
+variable (G)
+
+/-- `LinearMap.rTensor` as a continuous linear map, i.e. the continuous linear map `f` extended to
+the map `x ⊗ₜ[𝕜] y ↦ f(x) ⊗ₜ[𝕜] y`. -/
+noncomputable def rTensor (f : E →L[𝕜] F) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] G) :=
+  (f.toLinearMap.rTensor G).mkContinuous ‖f‖ fun x ↦ by
+    /-
+    Any tensor `x` can be written as a linear combination of pure tensors, `x = ∑ e n ⊗ₜ g n`. This
+    induces three Gram matrices, one based on `e`, one on `f ∘ e` and one on `g`. Up to a constant,
+    the `e`-based Gram matrix is larger than the `f ∘ e`-based one. This implies the existence of
+    a matrix, whose form is used to show that `‖f‖ ^ 2 * ‖x‖ ^ 2 - ‖f x‖ ^ 2` is a sum of
+    nonnegative terms.
+    -/
+    obtain ⟨n, e, g, hx⟩ := exists_sum_tmul_eq x
+    obtain ⟨c, hc_supp, hc⟩ := Submodule.mem_span_set.mp
+      ((span_tmul_eq_top 𝕜 E G) ▸ Submodule.mem_top (x := x))
+    obtain ⟨m, A, hA⟩ := Matrix.posSemidef_iff_eq_sum_vecMulVec.mp
+      (Matrix.posSemidef_opNorm_smul_gram_sub_gram e f)
+    apply (sq_le_sq₀ (norm_nonneg _) (by positivity)).mp
+    simp_rw [sub_eq_iff_eq_add', ← sub_eq_iff_eq_add, ← Matrix.ext_iff, Matrix.sub_apply,
+      Matrix.smul_apply, Matrix.gram_apply, Function.comp_apply] at hA
+    simp_rw [mul_pow, hx, map_sum, LinearMap.rTensor_tmul, coe_coe,
+      ← inner_self_eq_norm_sq (𝕜 := 𝕜), inner_sum, sum_inner, inner_tmul, ← hA, sub_mul,
+      Finset.sum_sub_distrib, map_sub, ← RCLike.smul_re, Finset.smul_sum, smul_mul_assoc,
+      sub_le_self_iff, Matrix.sum_apply, mul_comm, Finset.mul_sum]
+    simp_rw +singlePass [Finset.sum_comm_cycle, Matrix.vecMulVec, Matrix.of_apply, Pi.star_apply,
+      ← mul_left_comm, ← mul_assoc, ← starRingEnd_self_apply (A _ _), ← inner_smul_left]
+    simp [mul_comm, ← inner_smul_right, ← sum_inner, ← inner_sum, Finset.sum_nonneg]
+
+variable {G} in
+@[simp] lemma rTensor_apply (f : E →L[𝕜] F) (x : E ⊗ G) :
+    f.rTensor G x = f.toLinearMap.rTensor G x := rfl
+
+variable {G} in
+lemma rTensor_tmul (f : E →L[𝕜] F) (m : E) (n : G) : f.rTensor G (m ⊗ₜ n) = f m ⊗ₜ n := rfl
+
+@[simp] lemma toLinearMap_rTensor (f : E →L[𝕜] F) :
+    (f.rTensor G).toLinearMap = f.toLinearMap.rTensor G := rfl
+
+@[simp] lemma _root_.LinearIsometry.toContinuousLinearMap_rTensor (f : E →ₗᵢ[𝕜] F) :
+    (f.rTensor G).toContinuousLinearMap = f.toContinuousLinearMap.rTensor G := rfl
+
+theorem norm_rTensor_le (f : E →L[𝕜] F) : ‖f.rTensor G‖ ≤ ‖f‖ :=
+  LinearMap.mkContinuous_norm_le _ (norm_nonneg _) _
+
+@[simp] lemma rTensor_add (f₁ f₂ : E →L[𝕜] F) :
+    (f₁ + f₂).rTensor G = f₁.rTensor G + f₂.rTensor G := by ext; simp
+
+@[simp] lemma rTensor_smul (r : 𝕜) (f : E →L[𝕜] F) :
+    (r • f).rTensor G = r • f.rTensor G := by ext; simp
+
+@[simp] lemma rTensor_id : (.id 𝕜 E : E →L[𝕜] E).rTensor G = .id 𝕜 _ := by ext; simp
+@[simp] lemma rTensor_one : (1 : E →L[𝕜] E).rTensor G = 1 := rTensor_id _
+@[simp] lemma rTensor_zero : (0 : E →L[𝕜] F).rTensor G = 0 := by ext; simp
+@[simp] lemma rTensor_neg (f : E →L[𝕜] F) : (-f).rTensor G = -f.rTensor G := by ext; simp
+
+@[simp] lemma rTensor_sub (f₁ f₂ : E →L[𝕜] F) :
+    (f₁ - f₂).rTensor G = f₁.rTensor G - f₂.rTensor G := by ext; simp
+
+lemma rTensor_comp (f₁ : E →L[𝕜] F) (f₂ : H →L[𝕜] E) :
+    (f₁ ∘L f₂).rTensor G = f₁.rTensor G ∘L f₂.rTensor G := by ext; simp [LinearMap.rTensor_comp]
+
+lemma rTensor_mul (f₁ f₂ : E →L[𝕜] E) : (f₁ * f₂).rTensor G = f₁.rTensor G * f₂.rTensor G :=
+  rTensor_comp _ _ _
+
+@[simp] lemma rTensor_pow (f : E →L[𝕜] E) (n : ℕ) : (f ^ n).rTensor G = (f.rTensor G) ^ n := by
+  simp [← coe_inj]
+
+/-- `LinearMap.lTensor` as a continuous linear map, i.e. the continuous linear map `g` extended to
+the map `x ⊗ₜ[𝕜] y ↦ x ⊗ₜ[𝕜] g(y)`. -/
+noncomputable def lTensor (g : E →L[𝕜] F) : (G ⊗[𝕜] E) →L[𝕜] (G ⊗[𝕜] F) :=
+  commIsometry 𝕜 F G ∘L g.rTensor G ∘L commIsometry 𝕜 G E
+
+variable {G} in
+@[simp] lemma lTensor_apply (g : G →L[𝕜] H) (x : E ⊗ G) :
+    g.lTensor E x = g.toLinearMap.lTensor E x := by
+  simp [lTensor, ← LinearMap.comm_comp_rTensor_comp_comm_eq]
+
+lemma lTensor_tmul (g : E →L[𝕜] F) (m : G) (n : E) : g.lTensor G (m ⊗ₜ n) = m ⊗ₜ g n := rfl
+
+theorem commIsometry_comp_lTensor_comp_commIsometry_eq (g : E →L[𝕜] F) :
+    commIsometry 𝕜 F G ∘L g.rTensor G ∘L commIsometry 𝕜 G E = g.lTensor G :=
+  rfl
+
+theorem commIsometry_comp_rTensor_comp_commIsometry_eq (f : E →L[𝕜] F) :
+    commIsometry 𝕜 G F ∘L f.lTensor G ∘L commIsometry 𝕜 E G = f.rTensor G := by
+  ext; simp [lTensor]
+
+theorem lTensor_comp_commIsometry (f : E →L[𝕜] F) :
+    f.lTensor G ∘L commIsometry 𝕜 E G = commIsometry 𝕜 F G ∘L f.rTensor G := by
+  ext; simp [lTensor]
+
+theorem rTensor_comp_commIsometry (g : E →L[𝕜] F) :
+    g.rTensor G ∘L commIsometry 𝕜 G E = commIsometry 𝕜 G F ∘L g.lTensor G := by
+  ext; simp [lTensor]
+
+@[simp] lemma toLinearMap_lTensor (g : E →L[𝕜] F) :
+    (g.lTensor G).toLinearMap = g.toLinearMap.lTensor G := by ext; simp
+
+@[simp] lemma _root_.LinearIsometry.toContinuousLinearMap_lTensor (g : E →ₗᵢ[𝕜] F) :
+    (g.lTensor G).toContinuousLinearMap = g.toContinuousLinearMap.lTensor G := by ext; simp
+
+theorem norm_lTensor_le (g : E →L[𝕜] F) : ‖g.lTensor G‖ ≤ ‖g‖ := by
+  simp_rw [lTensor, ← LinearIsometryEquiv.toContinuousLinearMap_toLinearIsometry]
+  grw [opNorm_comp_le, opNorm_comp_le, LinearIsometry.norm_toContinuousLinearMap_le,
+    LinearIsometry.norm_toContinuousLinearMap_le, mul_one, one_mul, norm_rTensor_le]
+
+@[simp] lemma lTensor_add (f₁ f₂ : E →L[𝕜] F) :
+    (f₁ + f₂).lTensor G = f₁.lTensor G + f₂.lTensor G := by ext; simp
+
+@[simp] lemma lTensor_smul (r : 𝕜) (f : E →L[𝕜] F) : (r • f).lTensor G = r • f.lTensor G := by
+  ext; simp
+
+@[simp] lemma lTensor_id : (.id 𝕜 E : E →L[𝕜] E).lTensor G = .id 𝕜 _ := by ext; simp
+@[simp] lemma lTensor_one : (1 : E →L[𝕜] E).lTensor G = 1 := lTensor_id _
+@[simp] lemma lTensor_zero : (0 : E →L[𝕜] F).lTensor G = 0 := by ext; simp
+@[simp] lemma lTensor_neg (f : E →L[𝕜] F) : (-f).lTensor G = -f.lTensor G := by ext; simp
+
+@[simp] lemma lTensor_sub (f₁ f₂ : E →L[𝕜] F) :
+    (f₁ - f₂).lTensor G = f₁.lTensor G - f₂.lTensor G := by ext; simp
+
+lemma lTensor_comp (f₁ : E →L[𝕜] F) (f₂ : H →L[𝕜] E) :
+    (f₁ ∘L f₂).lTensor G = f₁.lTensor G ∘L f₂.lTensor G := by ext; simp [LinearMap.lTensor_comp]
+
+lemma lTensor_mul (f₁ f₂ : E →L[𝕜] E) : (f₁ * f₂).lTensor G = f₁.lTensor G * f₂.lTensor G :=
+  lTensor_comp _ _ _
+
+@[simp] lemma lTensor_pow (f : E →L[𝕜] E) (n : ℕ) : (f ^ n).lTensor G = (f.lTensor G) ^ n := by
+  simp [← coe_inj]
+
+end ContinuousLinearMap
+
+namespace TensorProduct
+
+/-- `TensorProduct.map` as a continuous linear map, i.e. the continuous linear map
+`x ⊗ₜ[𝕜] y ↦ f(x) ⊗ₜ[𝕜] g(y)` formed from the continuous linear maps `f` and `g`. -/
+noncomputable def mapL (f : E →L[𝕜] F) (g : G →L[𝕜] H) : (E ⊗[𝕜] G) →L[𝕜] (F ⊗[𝕜] H) :=
+  f.rTensor H ∘L g.lTensor E
+
+theorem norm_mapL_le (f : E →L[𝕜] F) (g : G →L[𝕜] H) : ‖mapL f g‖ ≤ ‖f‖ * ‖g‖ := by
+  grw [mapL, ContinuousLinearMap.opNorm_comp_le, ContinuousLinearMap.norm_rTensor_le,
+    ContinuousLinearMap.norm_lTensor_le]
+
+@[simp] lemma mapL_apply (f : E →L[𝕜] F) (g : G →L[𝕜] H) (x) :
+    mapL f g x = map f.toLinearMap g.toLinearMap x := by
+  simp [mapL, ← LinearMap.rTensor_comp_lTensor]
+
+lemma mapL_tmul (f : E →L[𝕜] F) (g : G →L[𝕜] H) (m : E) (n : G) :
+    mapL f g (m ⊗ₜ n) = f m ⊗ₜ g n := rfl
+
+@[simp] lemma mapL_zero_left (f : E →L[𝕜] F) : mapL (0 : G →L[𝕜] H) f = 0 := by simp [mapL]
+@[simp] lemma mapL_zero_right (f : E →L[𝕜] F) : mapL f (0 : G →L[𝕜] H) = 0 := by simp [mapL]
+@[simp] lemma mapL_id_id : mapL (.id 𝕜 E) (.id 𝕜 G) = .id 𝕜 _ := by simp [mapL]
+
+lemma mapL_comp_commIsometry (f : E →L[𝕜] F) (g : G →L[𝕜] H) :
+    mapL f g ∘L commIsometry 𝕜 G E = commIsometry 𝕜 H F ∘L mapL g f := by ext; simp [map_comm]
+
+lemma mapL_add_left (f₁ f₂ : E →L[𝕜] F) (g : G →L[𝕜] H) :
+    mapL (f₁ + f₂) g = mapL f₁ g + mapL f₂ g := by ext; simp [map_add_left]
+
+lemma mapL_add_right (f : E →L[𝕜] F) (g₁ g₂ : G →L[𝕜] H) :
+    mapL f (g₁ + g₂) = mapL f g₁ + mapL f g₂ := by ext; simp [map_add_right]
+
+lemma mapL_smul_left (r : 𝕜) (f : E →L[𝕜] F) (g : G →L[𝕜] H) :
+    mapL (r • f) g = r • mapL f g := by ext; simp [map_smul_left]
+
+lemma mapL_smul_right (r : 𝕜) (f : E →L[𝕜] F) (g : G →L[𝕜] H) :
+    mapL f (r • g) = r • mapL f g := by ext; simp [map_smul_right]
+
+@[simp] lemma toLinearMap_mapL (f : E →L[𝕜] F) (g : G →L[𝕜] H) :
+    (mapL f g).toLinearMap = map f g := by ext; simp
+
+@[simp] lemma toContinuousLinearMap_mapIsometry (f : E →ₗᵢ[𝕜] F) (g : G →ₗᵢ[𝕜] H) :
+    (mapIsometry f g).toContinuousLinearMap =
+      mapL f.toContinuousLinearMap g.toContinuousLinearMap := by
+  ext; simp
+
+section comp
+
+variable {A B : Type*} [NormedAddCommGroup A] [InnerProductSpace 𝕜 A] [NormedAddCommGroup B]
+  [InnerProductSpace 𝕜 B]
+
+lemma mapL_comp (f₁ : E →L[𝕜] F) (f₂ : A →L[𝕜] E) (g₁ : G →L[𝕜] H) (g₂ : B →L[𝕜] G) :
+    mapL (f₁ ∘L f₂) (g₁ ∘L g₂) = mapL f₁ g₁ ∘L mapL f₂ g₂ := by ext; simp [map_map]
+
+lemma mapL_mul (f₁ f₂ : E →L[𝕜] E) (g₁ g₂ : F →L[𝕜] F) :
+    mapL (f₁ * f₂) (g₁ * g₂) = mapL f₁ g₁ * mapL f₂ g₂ := mapL_comp _ _ _ _
+
+@[simp] lemma mapL_pow (f : E →L[𝕜] E) (g : F →L[𝕜] F) (n : ℕ) :
+    (mapL f g) ^ n = mapL (f ^ n) (g ^ n) := by simp [← ContinuousLinearMap.coe_inj]
+
+@[simp] lemma _root_.ContinuousLinearMap.mapL_comp_rTensor (f₁ : E →L[𝕜] F) (f₂ : A →L[𝕜] E)
+    (g : G →L[𝕜] H) : mapL f₁ g ∘L f₂.rTensor G = mapL (f₁ ∘L f₂) g := by ext; simp
+
+@[simp] lemma _root_.ContinuousLinearMap.mapL_comp_lTensor (f : E →L[𝕜] F) (g₁ : G →L[𝕜] H)
+    (g₂ : A →L[𝕜] G) : mapL f g₁ ∘L g₂.lTensor E = mapL f (g₁ ∘L g₂) := by ext; simp
+
+@[simp] lemma _root_.ContinuousLinearMap.rTensor_comp_mapL (f₁ : E →L[𝕜] F) (f₂ : A →L[𝕜] E)
+    (g : G →L[𝕜] H) : f₁.rTensor H ∘L mapL f₂ g = mapL (f₁ ∘L f₂) g := by ext; simp
+
+@[simp] lemma _root_.ContinuousLinearMap.lTensor_comp_mapL (f : E →L[𝕜] F) (g₁ : G →L[𝕜] H)
+    (g₂ : A →L[𝕜] G) : g₁.lTensor F ∘L mapL f g₂ = mapL f (g₁ ∘L g₂) := by ext; simp
+
+end comp
+
+variable (G) in
+theorem _root_.ContinuousLinearMap.rTensor_eq_mapL (f : E →L[𝕜] F) :
+    f.rTensor G = mapL f (.id 𝕜 G) := by simp [mapL]
+
+variable (E) in
+theorem _root_.ContinuousLinearMap.lTensor_eq_mapL (g : G →L[𝕜] H) :
+    g.lTensor E = mapL (.id 𝕜 E) g := by simp [mapL]
+
+@[simp] lemma _root_.ContinuousLinearMap.lTensor_comp_rTensor (f : E →L[𝕜] F) (g : G →L[𝕜] H) :
+    f.lTensor H ∘L g.rTensor E = mapL g f := by ext; simp [← LinearMap.lTensor_comp_rTensor]
+
+@[simp] lemma _root_.ContinuousLinearMap.rTensor_comp_lTensor (f : E →L[𝕜] F) (g : G →L[𝕜] H) :
+    f.rTensor H ∘L g.lTensor E = mapL f g := rfl
+
+@[simp] theorem adjoint_mapL [CompleteSpace E] [CompleteSpace G] [CompleteSpace (E ⊗[𝕜] G)]
+    [CompleteSpace F] [CompleteSpace H] [CompleteSpace (F ⊗[𝕜] H)]
+    (f : E →L[𝕜] F) (g : G →L[𝕜] H) : (mapL f g).adjoint = mapL f.adjoint g.adjoint := by
+  apply ContinuousLinearMap.coe_inj.mp <| ext' ?_
+  simp [TensorProduct.ext_iff_inner_right, ContinuousLinearMap.adjoint_inner_left]
+
+variable (G) in
+@[simp] theorem _root_.ContinuousLinearMap.adjoint_rTensor [CompleteSpace E] [CompleteSpace G]
+    [CompleteSpace (E ⊗[𝕜] G)] [CompleteSpace (F ⊗[𝕜] G)] [CompleteSpace F] (f : E →L[𝕜] F) :
+    (f.rTensor G).adjoint = f.adjoint.rTensor G := by simp [ContinuousLinearMap.rTensor_eq_mapL]
+
+variable (E) in
+@[simp] theorem _root_.ContinuousLinearMap.adjoint_lTensor [CompleteSpace E] [CompleteSpace G]
+    [CompleteSpace (E ⊗[𝕜] H)] [CompleteSpace (E ⊗[𝕜] G)] [CompleteSpace H] (g : G →L[𝕜] H) :
+    (g.lTensor E).adjoint = g.adjoint.lTensor E := by simp [ContinuousLinearMap.lTensor_eq_mapL]
 
 open LinearMap
 
+@[simp] theorem adjoint_map [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G]
+    [FiniteDimensional 𝕜 H] (f : E →ₗ[𝕜] F) (g : G →ₗ[𝕜] H) :
+    (map f g).adjoint = map f.adjoint g.adjoint :=
+  ext' fun _ _ => by simp [TensorProduct.ext_iff_inner_right, adjoint_inner_left]
+
 @[simp] theorem _root_.LinearMap.adjoint_rTensor [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F]
     [FiniteDimensional 𝕜 G] (f : E →ₗ[𝕜] F) :
-    adjoint (rTensor G f) = rTensor G f.adjoint := by simp [rTensor]
+    (f.rTensor G).adjoint = f.adjoint.rTensor G := by simp [rTensor]
 
 @[simp] theorem _root_.LinearMap.adjoint_lTensor [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F]
     [FiniteDimensional 𝕜 G] (f : E →ₗ[𝕜] F) :
-    adjoint (lTensor G f) = lTensor G f.adjoint := by simp [lTensor]
+    (f.lTensor G).adjoint = f.adjoint.lTensor G := by simp [lTensor]
+
+/-- If `E` and `F` are continuously and linearly equivalent and `G` and `H` are continuously and
+linearly equivalent, then `E ⊗ G` and `F ⊗ H` are continuously and linearly equivalent. -/
+noncomputable def congrL (f : E ≃L[𝕜] F) (g : G ≃L[𝕜] H) : E ⊗[𝕜] G ≃L[𝕜] F ⊗[𝕜] H :=
+  ContinuousLinearEquiv.ofContinuousLinear (mapL f g) (mapL f.symm g.symm)
+    (by ext; simp [← mapL_comp])
+    (by ext; simp [← mapL_comp])
+
+@[simp]
+theorem congrL_tmul (f : E ≃L[𝕜] F) (g : G ≃L[𝕜] H) (x : E) (y : G) :
+    congrL f g (x ⊗ₜ y) = f x ⊗ₜ g y :=
+  rfl
+
+@[simp]
+theorem congrL_symm_tmul (f : E ≃L[𝕜] F) (g : G ≃L[𝕜] H) (x : F) (y : H) :
+    (congrL f g).symm (x ⊗ₜ y) = f.symm x ⊗ₜ g.symm y :=
+  rfl
+
+theorem congrL_symm (f : E ≃L[𝕜] F) (g : G ≃L[𝕜] H) :
+    (congrL f g).symm = congrL f.symm g.symm :=
+  rfl
+
+@[simp]
+lemma toContinuousLinearMap_congrL (f : E ≃L[𝕜] F) (g : G ≃L[𝕜] H) :
+    (congrL f g).toContinuousLinearMap = mapL f g :=
+  rfl
+
+@[simp]
+lemma toLinearMap_congrL (f : E ≃L[𝕜] F) (g : G ≃L[𝕜] H) : (congrL f g).toLinearMap = map f g := by
+  ext; simp
+
+@[simp]
+theorem congrL_refl_refl : congrL (.refl 𝕜 E) (.refl 𝕜 G) = .refl 𝕜 _ :=
+  ContinuousLinearEquiv.toLinearEquiv_injective <| (by simp [congrL]; rfl)
+
+section congr_congr
+variable {F₂ H₂ : Type*} [NormedAddCommGroup F₂] [InnerProductSpace 𝕜 F₂] [NormedAddCommGroup H₂]
+  [InnerProductSpace 𝕜 H₂] (f₂ : F ≃L[𝕜] F₂) (g₂ : H ≃L[𝕜] H₂) (f₁ : E ≃L[𝕜] F) (g₁ : G ≃L[𝕜] H)
+
+theorem congrL_trans : congrL (f₁.trans f₂) (g₁.trans g₂) = (congrL f₁ g₁).trans (congrL f₂ g₂) :=
+  ContinuousLinearEquiv.toLinearEquiv_injective <| (by ext; simp [congrL, map_map])
+
+theorem congrL_congr (x : E ⊗[𝕜] G) :
+    congrL f₂ g₂ (congrL f₁ g₁ x) = congrL (f₁.trans f₂) (g₁.trans g₂) x :=
+  DFunLike.congr_fun (congrL_trans ..).symm x
+
+end congr_congr
+
+theorem congrL_mul (f : E ≃L[𝕜] E) (g : G ≃L[𝕜] G) (f' : E ≃L[𝕜] E) (g' : G ≃L[𝕜] G) :
+    congrL (f * f') (g * g') = congrL f g * congrL f' g' := congrL_trans ..
+
+@[simp]
+theorem congrL_pow (f : E ≃L[𝕜] E) (g : G ≃L[𝕜] G) (n : ℕ) :
+    congrL f g ^ n = congrL (f ^ n) (g ^ n) := by
+  induction n with
+  | zero => exact congrL_refl_refl.symm
+  | succ n ih => simp_rw [pow_succ, ih, congrL_mul]
+
+@[simp]
+theorem congrL_zpow (f : E ≃L[𝕜] E) (g : G ≃L[𝕜] G) (n : ℤ) :
+    congrL f g ^ n = congrL (f ^ n) (g ^ n) := by
+  cases n with
+  | ofNat n => exact congrL_pow _ _ _
+  | negSucc n => simp_rw [zpow_negSucc, congrL_pow]; exact congrL_symm _ _
 
 /-- Given `x, y : E ⊗ (F ⊗ G)`, `x = y` iff `⟪x, a ⊗ₜ (b ⊗ₜ c)⟫ = ⟪y, a ⊗ₜ (b ⊗ₜ c)⟫` for all
 `a, b, c`.

Mathlib/Analysis/Normed/Operator/LinearIsometry.lean

@@ -284,6 +284,9 @@ theorem diam_range : Metric.diam (range f) = Metric.diam (univ : Set E) :=
 def toContinuousLinearMap : E →SL[σ₁₂] E₂ :=
   ⟨f.toLinearMap, f.continuous⟩
 
+@[simp] lemma toLinearMap_toContinuousLinearMap (f : E →ₛₗᵢ[σ₁₂] E₂) :
+  f.toContinuousLinearMap.toLinearMap = f.toLinearMap := rfl
+
 theorem toContinuousLinearMap_injective :
     Function.Injective (toContinuousLinearMap : _ → E →SL[σ₁₂] E₂) := fun x _ h =>
   coe_injective (congr_arg _ h : ⇑x.toContinuousLinearMap = _)