-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear (goal)
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 ⋯ ⋯)
⊢ ∃ (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 ⋯ ⋯)
have 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) sorry sorry sorry)),
  ∃ (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 sorry sorry)
Tactic: choose s hs hsp φ u hu hφ h2φ heφ using h
Cleared hypotheses: h