-- Module: Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear
Goal:
𝕜 : 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 : ℕ∞ω
e : OpenPartialHomeomorph (B × F) (B × F)
h :
  ∀ (x : (↑e.source : Type (max u_2 u_3))),
    ∃ (s : Set (B × F)),
      IsOpen[instTopologicalSpaceProd] s ∧
        (↑x : B × F) ∈ s ∧
          ∃ (φ : B → F ≃L[𝕜] F) (u : Set B) (hu : IsOpen[inst] u) (hφ :
            ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
              (fun (x : B) ↦ (↑(φ x) : F →L[𝕜] F)) u)
            (h2φ :
            ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
              (fun (x : B) ↦ (↑(φ x).symm : F →L[𝕜] F)) u),
            (e.restr s).EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := u) φ hu ⋯ ⋯)
choose :
  ∀ (s : (x : (↑e.source : Type (max u_2 u_3))) → Set (B × F))
    (hs : ∀ (x : (↑e.source : Type (max u_2 u_3))), IsOpen[instTopologicalSpaceProd] (s x))
    (hsp : ∀ (x : (↑e.source : Type (max u_2 u_3))), (↑x : B × F) ∈ s x)
    (φ : (x : (↑e.source : Type (max u_2 u_3))) → B → F ≃L[𝕜] F) (u : (x : (↑e.source : Type (max u_2 u_3))) → Set B)
    (hu : ∀ (x : (↑e.source : Type (max u_2 u_3))), IsOpen[inst] (u x))
    (hφ :
      ∀ (x : (↑e.source : Type (max u_2 u_3))),
        ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
          (fun (x_1 : B) ↦ (↑(φ x x_1) : F →L[𝕜] F)) (u x))
    (h2φ :
      ∀ (x : (↑e.source : Type (max u_2 u_3))),
        ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
          (fun (x_1 : B) ↦ (↑(φ x x_1).symm : F →L[𝕜] F)) (u x))
    (heφ :
      ∀ (x : (↑e.source : Type (max u_2 u_3))),
        (e.restr (s x)).EqOnSource (FiberwiseLinear.openPartialHomeomorph (U := u x) (φ x) ⋯ ⋯ ⋯)),
    ∃ (U : Set B),
      e.source = SProd.sprod (β := Set F) U univ ∧
        ∀ x ∈ U,
          ∃ (φ : B → F ≃L[𝕜] F) (u : Set B) (hu : IsOpen[inst] u) (_ : u ⊆ U) (_ : x ∈ u) (hφ :
            ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
              (fun (x : B) ↦ (↑(φ x) : F →L[𝕜] F)) u)
            (h2φ :
            ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
              (fun (x : B) ↦ (↑(φ x).symm : F →L[𝕜] F)) u),
            (e.restr (SProd.sprod (β := Set F) u univ)).EqOnSource
              (FiberwiseLinear.openPartialHomeomorph (U := u) φ hu ⋯ ⋯)
⊢ ∃ (U : Set B),
    e.source = SProd.sprod (β := Set F) U univ ∧
      ∀ x ∈ U,
        ∃ (φ : B → F ≃L[𝕜] F) (u : Set B) (hu : IsOpen[inst] u) (_ : u ⊆ U) (_ : x ∈ u) (hφ :
          ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
            (fun (x : B) ↦ (↑(φ x) : F →L[𝕜] F)) u)
          (h2φ :
          ContMDiffOn.{u_1, u_4, u_5, u_2, u_3, u_3, u_3} IB (E' := F →L[𝕜] F) 𝓘(𝕜, F →L[𝕜] F) (M' := F →L[𝕜] F) n
            (fun (x : B) ↦ (↑(φ x).symm : F →L[𝕜] F)) u),
          (e.restr (SProd.sprod (β := Set F) u univ)).EqOnSource
            (FiberwiseLinear.openPartialHomeomorph (U := u) φ hu ⋯ ⋯)

Tactic:
choose s hs hsp φ u hu hφ h2φ heφ using h