refine Fin.cases ?_ ?_ i <;> simp
case h.H.h.e_6.h.h
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : Fintype ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝⁷ : (i : ι) → NormedAddCommGroup (M i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : ℕ
M₁ : Fin (n + 1) → Type u_6
inst✝³ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁ i)
inst✝² : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁ i)
M₁' : Fin (n + 1) → Type u_7
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁' i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁' i)
g : ContinuousMultilinearMap 𝕜 M₁' F
f : (i : Fin (n + 1)) → M₁ i →L[𝕜] M₁' i
u : M₁ 0
m : (i : Fin n) → M₁ (Fin.succ i)
i : Fin (n + 1)
⊢ (f i) (Fin.cons u m i) = Fin.cons ((f 0) u) (fun i => (f (Fin.succ i)) (m i)) i
no goals