-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Basic (goal)
Goal:
n : ℕ∞ω
𝕜 : Type u_1
B : Type u_2
B' : Type u_3
F : Type u_4
M : Type u_5
E : B → Type u_6
inst : NontriviallyNormedField 𝕜
EB : Type u_7
inst_1 : NormedAddCommGroup EB
inst_2 : NormedSpace 𝕜 EB
HB : Type u_8
inst_3 : TopologicalSpace HB
IB : ModelWithCorners 𝕜 EB HB
inst_4 : TopologicalSpace B
inst_5 : ChartedSpace HB B
EM : Type u_9
inst_6 : NormedAddCommGroup EM
inst_7 : NormedSpace 𝕜 EM
HM : Type u_10
inst_8 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_9 : TopologicalSpace M
inst_10 : ChartedSpace HM M
inst_11 : (x : B) → AddCommMonoid (E x)
inst_12 : (x : B) → Module.{u_1, u_6} 𝕜 (E x)
inst_13 : NormedAddCommGroup F
inst_14 : NormedSpace 𝕜 F
inst_15 : TopologicalSpace (TotalSpace F E)
inst_16 : (x : B) → TopologicalSpace (E x)
inst_17 : FiberBundle F E
inst_18 : VectorBundle 𝕜 F E
inst_19 : ContMDiffVectorBundle n F E IB
inst_20 : IsManifold IB n B
e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he :
  Membership.mem (γ := Set (Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))))
    (trivializationAtlas F E) e
e' : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))
he' :
  Membership.mem (γ := Set (Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))))
    (trivializationAtlas F E) e'
this_1 : MemTrivializationAtlas (E := E) e
this : MemTrivializationAtlas (E := E) e'
refine_1 :
  (FiberwiseLinear.openPartialHomeomorph (U := e.baseSet ∩ e'.baseSet) (Trivialization.coordChangeL 𝕜 (E := E) e e') ⋯ ⋯
        ⋯).source =
    PartialEquiv.source (β := B × F)
      (toPartialEquiv
        (OpenPartialHomeomorph.trans (Y := TotalSpace F E)
          (OpenPartialHomeomorph.symm
            ((fun (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) ↦
                e.toOpenPartialHomeomorph)
              e))
          ((fun (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) ↦
              e.toOpenPartialHomeomorph)
            e')))
⊢ EqOnSource
    (OpenPartialHomeomorph.trans (Y := TotalSpace F E)
      (OpenPartialHomeomorph.symm
        ((fun (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) ↦
            e.toOpenPartialHomeomorph)
          e))
      ((fun (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) ↦
          e.toOpenPartialHomeomorph)
        e'))
    (FiberwiseLinear.openPartialHomeomorph (U := e.baseSet ∩ e'.baseSet) (Trivialization.coordChangeL 𝕜 (E := E) e e') ⋯
      ⋯ ⋯)
have refine_2 : EqOn
  (↑(FiberwiseLinear.openPartialHomeomorph (U := e.baseSet ∩ e'.baseSet) (Trivialization.coordChangeL 𝕜 (E := E) e e') sorry
        sorry sorry) :
    B × F → B × F)
  (↑(OpenPartialHomeomorph.trans (Y := TotalSpace F E)
        (OpenPartialHomeomorph.symm
          ((fun (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) ↦
              e.toOpenPartialHomeomorph)
            e))
        ((fun (e : Trivialization (B := B) F (Z := TotalSpace F E) (TotalSpace.proj (E := E))) ↦
            e.toOpenPartialHomeomorph)
          e')) :
    B × F → B × F)
  (FiberwiseLinear.openPartialHomeomorph (U := e.baseSet ∩ e'.baseSet) (Trivialization.coordChangeL 𝕜 (E := E) e e') sorry sorry
      sorry).source
Tactic: refine OpenPartialHomeomorph.eqOnSourceSetoid.symm ⟨?_, ?_⟩