-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
n : ℕ
Ei : Fin n.succ → Type wEi
G : Type wG
inst : NontriviallyNormedField 𝕜
inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_2 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
f : Ei 0 →L[𝕜] ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G
m : Ei 0
x : (i : Fin n) → Ei i.succ
h :
  Eq.{wG + 1} (α := G) ((f.uncurryLeft (Ei := Ei) : (a : (i : Fin n.succ) → Ei i) → G) (Fin.cons (α := Ei) m x) : G)
    ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) m :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        x :
      G)
h₁ :
  Eq.{wG + 1} (α := G)
    ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) (Fin.cons (α := Ei) m x 0) :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        (tail (α := Ei) (Fin.cons (α := Ei) m x)) :
      G)
    ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) m :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        x :
      G)
h₂ :
  Eq.{wG + 1} (α := G)
    ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) (Fin.cons (α := Ei) m x 0) :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        x :
      G)
    ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) m :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        x :
      G)
h₃ h₄ :
  Eq.{wG + 1} (α := G)
    ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) m :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        x :
      G)
    ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) m :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        x :
      G)
⊢ Eq.{wG + 1} (α := G)
    ((((f.uncurryLeft (Ei := Ei).curryLeft (Ei := Ei) :
                (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G)
              m :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        x :
      G)
    ((((f : (a : Ei 0) → ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) m :
            ContinuousMultilinearMap.{u, 0, wEi, wG} 𝕜 (fun (i : Fin n) ↦ Ei i.succ) G) :
          (a : (i : Fin n) → Ei i.succ) → G)
        x :
      G)

Tactic:
rw [ContinuousMultilinearMap.curryLeft_apply, ContinuousLinearMap.uncurryLeft_apply, tail_cons,
    cons_zero]

Premises used: ContinuousLinearMap.uncurryLeft_apply, ContinuousMultilinearMap.curryLeft_apply, Fin.cons_zero, Fin.tail_cons