{ι : Type u_5} →
  {B : Type u_6} →
    [inst : TopologicalSpace B] →
      {F : Type u_7} →
        [inst_1 : TopologicalSpace F] →
          {motive : FiberBundleCore ι B F → Sort u} →
            (t : FiberBundleCore ι B F) →
              ((baseSet : ι → Set B) →
                  (isOpen_baseSet : ∀ (i : ι), IsOpen (baseSet i)) →
                    (indexAt : B → ι) →
                      (mem_baseSet_at : ∀ (x : B), x ∈ baseSet (indexAt x)) →
                        (coordChange : ι → ι → B → F → F) →
                          (coordChange_self : ∀ (i : ι), ∀ x ∈ baseSet i, ∀ (v : F), coordChange i i x v = v) →
                            (continuousOn_coordChange :
                                ∀ (i j : ι),
                                  ContinuousOn (fun p => coordChange i j p.1 p.2)
                                    ((baseSet i ∩ baseSet j) ×ˢ Set.univ)) →
                              (coordChange_comp :
                                  ∀ (i j k : ι),
                                    ∀ x ∈ baseSet i ∩ baseSet j ∩ baseSet k,
                                      ∀ (v : F), coordChange j k x (coordChange i j x v) = coordChange i k x v) →
                                motive
                                  { baseSet := baseSet, isOpen_baseSet := isOpen_baseSet, indexAt := indexAt,
                                    mem_baseSet_at := mem_baseSet_at, coordChange := coordChange,
                                    coordChange_self := coordChange_self,
                                    continuousOn_coordChange := continuousOn_coordChange,
                                    coordChange_comp := coordChange_comp }) →
                motive t