∀ {ι : Type uι} [inst : Fintype ι] {𝕜 : Type u𝕜} [inst_1 : NontriviallyNormedField 𝕜] {E : ι → Type uE}
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (F : Type uF)
  [inst_4 : SeminormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F],
  PiTensorProduct.toDualContinuousMultilinearMap F =
    {
      toFun := fun x =>
        ((↑PiTensorProduct.lift).flip x ∘ₗ ContinuousMultilinearMap.toMultilinearMapLinear).mkContinuous
          (PiTensorProduct.projectiveSeminorm x) ⋯,
      map_add' := ⋯, map_smul' := ⋯ }