∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {EB : Type u_4} [inst_4 : NormedAddCommGroup EB]
  [inst_5 : NormedSpace 𝕜 EB] {HB : Type u_5} [inst_6 : TopologicalSpace HB] [inst_7 : ChartedSpace HB B]
  {IB : ModelWithCorners 𝕜 EB HB} (n : WithTop ℕ∞) (e : OpenPartialHomeomorph (B × F) (B × F)) (U : Set B),
  e.source = U ×ˢ Set.univ →
    (∀ x ∈ U,
        ∃ φ u,
          ∃ (hu : IsOpen u) (_ : u ⊆ U) (_ : x ∈ u) (hφ :
            ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun x => ↑(φ x)) u) (h2φ :
            ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun x => ↑(φ x).symm) u),
            (e.restr (u ×ˢ Set.univ)).EqOnSource (FiberwiseLinear.openPartialHomeomorph φ hu ⋯ ⋯)) →
      ∃ Φ U,
        ∃ (hU₀ : IsOpen U) (hΦ : ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun x => ↑(Φ x)) U) (h2Φ :
          ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n (fun x => ↑(Φ x).symm) U),
          e.EqOnSource (FiberwiseLinear.openPartialHomeomorph Φ hU₀ ⋯ ⋯)