Apply suggestions from code review

Co-authored-by: Monica Omar <23701951+themathqueen@users.noreply.github.com>

Author: mpacholski

Mathlib/Topology/Algebra/Module/Spaces/ContinuousLinearMap.lean

@@ -300,13 +300,13 @@ theorem map_smulₛₗ₂ (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (c : R) (x
 
 /-- Send a continuous sesquilinear map to an abstract sesquilinear map (forgetting continuity). -/
 @[simps!]
-def toLinearMap₁₂ : (E →SL[σ₁₃] F →SL[σ₂₃] G) →ₗ[𝕜₃] (E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) :=
-  { toFun L := (coeLMₛₗ σ₂₃).comp L.toLinearMap
-    map_add' _ _ := by ext; rfl
-    map_smul' _ _ := by ext; rfl}
+def toLinearMap₁₂ : (E →SL[σ₁₃] F →SL[σ₂₃] G) →ₗ[𝕜₃] (E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) where
+  toFun L := (coeLMₛₗ σ₂₃).comp L.toLinearMap
+  map_add' _ _ := by ext; rfl
+  map_smul' _ _ := by ext; rfl
 
 lemma toLinearMap₁₂_injective :
-    Function.Injective (toLinearMap₁₂ (E := E) (F := F) (G := G) (σ₁₃ := σ₁₃) (σ₂₃ := σ₂₃)) := by
+    (toLinearMap₁₂ (E := E) (F := F) (G := G) (σ₁₃ := σ₁₃) (σ₂₃ := σ₂₃) : _ → _).Injective := by
   simp [Function.Injective, LinearMap.ext_iff, ← ContinuousLinearMap.ext_iff]
 
 lemma toLinearMap₁₂_inj (L₁ L₂ : E →SL[σ₁₃] F →SL[σ₂₃] G) :