∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : NontriviallyNormedField 𝕜₂]
  {σ₁₂ : 𝕜₁ →+* 𝕜₂} [inst_2 : RingHomIsometric σ₁₂] {M₁ : Type u_3} {M₂ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommGroup M₁] [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommGroup M₂] [inst_7 : Module 𝕜₁ M₁]
  [inst_8 : Module 𝕜₂ M₂] [inst_9 : IsTopologicalAddGroup M₁] [inst_10 : ContinuousConstSMul 𝕜₁ M₁]
  [inst_11 : IsTopologicalAddGroup M₂] [inst_12 : ContinuousSMul 𝕜₂ M₂] {f : M₁ →ₛₗ[σ₁₂] M₂}
  (hf : IsCompactOperator ⇑f), ⇑(ContinuousLinearMap.mkOfIsCompactOperator hf) = ⇑f