{B : Type u_2} →
  {F : Type u_3} →
    [inst : TopologicalSpace B] →
      [inst_1 : TopologicalSpace F] →
        {E : B → Type u_5} →
          [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] →
            [inst_3 : (b : B) → TopologicalSpace (E b)] →
              {motive : FiberBundle F E → Sort u} →
                (t : FiberBundle F E) →
                  ((totalSpaceMk_isInducing' : ∀ (b : B), Topology.IsInducing (Bundle.TotalSpace.mk b)) →
                      (trivializationAtlas' : Set (Trivialization F Bundle.TotalSpace.proj)) →
                        (trivializationAt' : B → Trivialization F Bundle.TotalSpace.proj) →
                          (mem_baseSet_trivializationAt' : ∀ (b : B), b ∈ (trivializationAt' b).baseSet) →
                            (trivialization_mem_atlas' : ∀ (b : B), trivializationAt' b ∈ trivializationAtlas') →
                              motive
                                { totalSpaceMk_isInducing' := totalSpaceMk_isInducing',
                                  trivializationAtlas' := trivializationAtlas', trivializationAt' := trivializationAt',
                                  mem_baseSet_trivializationAt' := mem_baseSet_trivializationAt',
                                  trivialization_mem_atlas' := trivialization_mem_atlas' }) →
                    motive t