simp [Subsingleton.elim f g, hε]
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
E : Fin Nat.zero → Type u_2
inst✝³ : (i : Fin Nat.zero) → NormedAddCommGroup (E i)
inst✝² : (i : Fin Nat.zero) → NormedSpace 𝕜 (E i)
E₁ : Fin Nat.zero → Type u_3
inst✝¹ : (i : Fin Nat.zero) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin Nat.zero) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin Nat.zero) → E i →L[𝕜] E₁ i
ε : ℝ
hε : ε > 0
g : (i : Fin Nat.zero) → E i →L[𝕜] E₁ i
x✝ : ‖g - f‖ < 1
⊢ ‖compContinuousLinearMapL g - compContinuousLinearMapL f‖ < ε
no goals