∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : ContinuousSMul 𝕜 E] {F : Type u_3}
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] [inst_8 : Module 𝕜 F]
  {𝕜' : Type u_4} [inst_9 : NontriviallyNormedField 𝕜'] [inst_10 : NormedAlgebra 𝕜' 𝕜] [inst_11 : Module 𝕜' E]
  [inst_12 : IsScalarTower 𝕜' 𝕜 E] [inst_13 : Module 𝕜' F] [inst_14 : IsScalarTower 𝕜' 𝕜 F] {𝕜'' : Type u_5}
  [inst_15 : Ring 𝕜''] [inst_16 : Module 𝕜'' F] [inst_17 : ContinuousConstSMul 𝕜'' F] [inst_18 : SMulCommClass 𝕜 𝕜'' F]
  [inst_19 : SMulCommClass 𝕜' 𝕜'' F],
  ↑(ContinuousLinearMap.restrictScalarsL 𝕜 E F 𝕜' 𝕜'') = ContinuousLinearMap.restrictScalarsₗ 𝕜 E F 𝕜' 𝕜''