∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] (e' : Bundle.Trivialization F Bundle.TotalSpace.proj) {b : B}
  {y : E b}, b ∈ e'.baseSet → (↑e' { proj := b, snd := y }).1 = b