∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {s : Set B}
  (hs : IsOpen s) {proj : Z → ↑s} (e : Pretrivialization F proj) [inst_2 : Nonempty (B → F → Z)],
  Pretrivialization.codExtend' hs e =
    { toFun := fun z => (↑(↑e z).1, (↑e z).2),
      invFun := fun x => if h : x.1 ∈ s then e.invFun (⟨x.1, h⟩, x.2) else Classical.arbitrary (B → F → Z) x.1 x.2,
      source := e.source, target := Prod.map Subtype.val id '' e.target, map_source' := ⋯, map_target' := ⋯,
      left_inv' := ⋯, right_inv' := ⋯, open_target := ⋯, baseSet := Subtype.val '' e.baseSet, open_baseSet := ⋯,
      source_eq := ⋯, target_eq := ⋯, proj_toFun := ⋯ }