∀ {E : Type u_1} {X : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X}
  [inst_2 : Nonempty (X → E)] {ι : Type u_2} [inst_3 : Nonempty ι] [inst_4 : TopologicalSpace ι] (U : ι → Set E)
  (V : Set X),
  IsOpen V →
    (∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen W ↔ IsOpen (f ⁻¹' W ∩ U i))) →
      ∀ (inj : ∀ (i : ι), Set.InjOn f (U i)) (disjoint : Pairwise (Function.onFun Disjoint U))
        (idx : (x : E) → x ∈ f ⁻¹' V → ι) (idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a))
        (inv : ι → ⦃a : X⦄ → a ∈ V → E) (x : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i ∧ f (inv i a_1) = a),
        ContinuousOn f
            { toFun := fun e => (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι),
                invFun := fun x => if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1,
                source := f ⁻¹' V, target := V ×ˢ Set.univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯,
                right_inv' := ⋯ }.source →
          ContinuousOn (fun x => (f x, if he : f x ∈ V then idx x he else Classical.arbitrary ι))
            { toFun := fun e => (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι),
                invFun := fun x => if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1,
                source := f ⁻¹' V, target := V ×ˢ Set.univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯,
                right_inv' := ⋯ }.source