generalize hε₁_def : (ε / 2) / (2 + ‖f 0‖) = ε₁
case succ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
IH :
  ∀ {E : Fin n → Type u_2} [inst : (i : Fin n) → NormedAddCommGroup (E i)] [inst_1 : (i : Fin n) → NormedSpace 𝕜 (E i)]
    {E₁ : Fin n → Type u_3} [inst_2 : (i : Fin n) → NormedAddCommGroup (E₁ i)]
    [inst_3 : (i : Fin n) → NormedSpace 𝕜 (E₁ i)] (f : (i : Fin n) → E i →L[𝕜] E₁ i),
    ∀ ε > 0,
      ∃ δ > 0,
        ∀ (a : (i : Fin n) → E i →L[𝕜] E₁ i),
          ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
⊢ ∃ δ > 0,
    ∀ (a : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i),
      ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
case succ
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
G : Type u_4
inst✝⁵ : NormedAddCommGroup G
inst✝⁴ : NormedSpace 𝕜 G
n : ℕ
IH :
  ∀ {E : Fin n → Type u_2} [inst : (i : Fin n) → NormedAddCommGroup (E i)] [inst_1 : (i : Fin n) → NormedSpace 𝕜 (E i)]
    {E₁ : Fin n → Type u_3} [inst_2 : (i : Fin n) → NormedAddCommGroup (E₁ i)]
    [inst_3 : (i : Fin n) → NormedSpace 𝕜 (E₁ i)] (f : (i : Fin n) → E i →L[𝕜] E₁ i),
    ∀ ε > 0,
      ∃ δ > 0,
        ∀ (a : (i : Fin n) → E i →L[𝕜] E₁ i),
          ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε
E : Fin (Nat.succ n) → Type u_2
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_3
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
ε : ℝ
hε_pos : ε > 0
ε₁ : ℝ
hε₁_def : ε / 2 / (2 + ‖f 0‖) = ε₁
⊢ ∃ δ > 0,
    ∀ (a : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i),
      ‖a - f‖ < δ → ‖compContinuousLinearMapL a - compContinuousLinearMapL f‖ < ε