simp [Subsingleton.elim _ (0 : (i : Fin 0) → E i →L[𝕜] E₁ i), hasFDerivAt_const]
case zero
𝕜 : Type u_1
inst✝¹⁸ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹⁷ : NormedAddCommGroup α
inst✝¹⁶ : NormedSpace 𝕜 α
D : Type u_3
inst✝¹⁵ : NormedAddCommGroup D
inst✝¹⁴ : NormedSpace 𝕜 D
ι : Type u_4
inst✝¹³ : Fintype ι
inst✝¹² : DecidableEq ι
E✝ : ι → Type u_5
inst✝¹¹ : (i : ι) → NormedAddCommGroup (E✝ i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E✝ i)
E₁✝ : ι → Type u_6
inst✝⁹ : (i : ι) → NormedAddCommGroup (E₁✝ i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E₁✝ i)
G : Type u_7
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_8
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
E : Fin Nat.zero → Type u_9
inst✝³ : (i : Fin Nat.zero) → NormedAddCommGroup (E i)
inst✝² : (i : Fin Nat.zero) → NormedSpace 𝕜 (E i)
E₁ : Fin Nat.zero → Type u_10
inst✝¹ : (i : Fin Nat.zero) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin Nat.zero) → NormedSpace 𝕜 (E₁ i)
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : Fin Nat.zero) → E i →L[𝕜] E₁ i
⊢ HasFDerivAt (fun f => compContinuousLinearMap g f)
    (∑ i : Fin Nat.zero, ContinuousLinearMap.comp (compContinuousLinearMapUpdate g i f) (ContinuousLinearMap.proj i)) f
no goals