∀ (𝕜 : Type u_2) {B : Type u_3} {F : Type u_4} {E : B → Type u_5} {B' : Type u_6} [inst : TopologicalSpace B']
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : NontriviallyNormedField 𝕜]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : TopologicalSpace B]
  [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)] {K : Type u_7} [inst_8 : FunLike K B' B]
  [inst_9 : ContinuousMapClass K B' B] (e : Bundle.Trivialization F Bundle.TotalSpace.proj)
  [Bundle.Trivialization.IsLinear 𝕜 e] (f : K), Bundle.Trivialization.IsLinear 𝕜 (e.pullback f)