exact fun ε hε ↦ ⟨1, ⟨zero_lt_one, fun g _ ↦ by simp [Subsingleton.elim f g, hε]⟩⟩
case zero
𝕜 : 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
⊢ ∀ ε > 0,
    ∃ δ > 0,
      ∀ (a : (i : Fin Nat.zero) → E i →L[𝕜] E₁ i),
        ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
no goals