Bundle Construction Lemma Surrogate

Stream: mathlib4

[Dominic Steinitz]

In my construction of a Riemannian metric, I found myself needing a specialised version of something one gets for free from the Bundle Construction Lemma. Here's a generalised version of what I needed but maybe it already exists?

import Mathlib

open Set Bundle ContDiff Manifold Trivialization SmoothPartitionOfUnity

section foo

variable
  {B : Type*} [TopologicalSpace B]
  {F₁ : Type*} [NormedAddCommGroup F₁] [NormedSpace ℝ F₁]
  {F₂ : Type*} [NormedAddCommGroup F₂] [NormedSpace ℝ F₂]
  {E₁ : B → Type*} [∀ x, NormedAddCommGroup (E₁ x)] [∀ x, NormedSpace ℝ (E₁ x)]
  [TopologicalSpace (TotalSpace F₁ E₁)]
  [FiberBundle F₁ E₁] [VectorBundle ℝ F₁ E₁]
  {E₂ : B → Type*} [∀ x, NormedAddCommGroup (E₂ x)] [∀ x, NormedSpace ℝ (E₂ x)]
  [TopologicalSpace (TotalSpace F₂ E₂)]
  [FiberBundle F₂ E₂] [VectorBundle ℝ F₂ E₂]

/-- The inverse trivialization of the hom-bundle `Hom(E₁, E₂)` at a point `b` acts by
pushing forward the input via the trivialization of `E₁`, applying the linear map,
and pulling back the result via the inverse trivialization of `E₂`. -/
lemma hom_trivializationAt_symm_apply
    (i b : B) (hb : b ∈ (trivializationAt F₁ E₁ i).baseSet)
    (s : F₁ →L[ℝ] F₂) (u : E₁ b) :
    (trivializationAt (F₁ →L[ℝ] F₂) (fun x ↦ E₁ x →L[ℝ] E₂ x) i).symm b s u =
    (trivializationAt F₂ E₂ i).symm b
      (s (trivializationAt F₁ E₁ i |>.continuousLinearMapAt ℝ b u)) := by
  sorry

end foo