-- Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
/-- Given an `A`-valued operation `Φ` on sections of vector bundles `V` and `V'` which is tensorial
at `x` in each argument, the construction `TensorialAt.mkHom₂` provides the associated continuous
linear map `V x →L[𝕜] V' x →L[𝕜] A`.  -/
TensorialAt.mkHom₂ : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [inst_10 : (x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [inst_12 : FiberBundle F V] →
                                        {F' : Type u_7} →
                                          [inst_13 : NormedAddCommGroup F'] →
                                            [inst_14 : NormedSpace 𝕜 F'] →
                                              {V' : M → Type u_8} →
                                                [inst_15 : TopologicalSpace (Bundle.TotalSpace F' V')] →
                                                  [inst_16 : (x : M) → AddCommGroup (V' x)] →
                                                    [inst_17 : (x : M) → Module 𝕜 (V' x)] →
                                                      [inst_18 : (x : M) → TopologicalSpace (V' x)] →
                                                        [inst_19 : FiberBundle F' V'] →
                                                          {A : Type u_9} →
                                                            [inst_20 : AddCommGroup A] →
                                                              [inst_21 : Module 𝕜 A] →
                                                                [inst_22 : VectorBundle 𝕜 F V] →
                                                                  [inst_23 : VectorBundle 𝕜 F' V'] →
                                                                    [CompleteSpace 𝕜] →
                                                                      [FiniteDimensional 𝕜 F] →
                                                                        [FiniteDimensional 𝕜 F'] →
                                                                          [ContMDiffVectorBundle 1 F V I] →
                                                                            [ContMDiffVectorBundle 1 F' V' I] →
                                                                              [inst_29 : TopologicalSpace A] →
                                                                                [inst_30 : IsTopologicalAddGroup A] →
                                                                                  [inst_31 : ContinuousSMul 𝕜 A] →
                                                                                    (Φ :
                                                                                        ((x : M) → V x) →
                                                                                          ((x : M) → V' x) → A) →
                                                                                      (x : M) →
                                                                                        (∀ (τ : (x : M) → V' x),
                                                                                            MDiffAt (T% τ) x →
                                                                                              TensorialAt I F
                                                                                                (fun x => Φ x τ) x) →
                                                                                          (∀ (σ : (x : M) → V x),
                                                                                              MDiffAt (T% σ) x →
                                                                                                TensorialAt I F' (Φ σ)
                                                                                                  x) →
                                                                                            V x →L[𝕜] V' x →L[𝕜] A