-- Lean 4 proof step from Mathlib.Topology.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_8
F₁ : Type u_9
F₂ : Type u_10
B₁ : Type u_11
B₂ : Type u_12
M : Type u_13
E₁ : B₁ → Type u_14
E₂ : B₂ → Type u_15
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_8, u_14} 𝕜 (E₁ x)
inst_3 : NormedAddCommGroup F₁
inst_4 : NormedSpace 𝕜 F₁
inst_5 : TopologicalSpace (TotalSpace F₁ E₁)
inst_6 : (x : B₁) → TopologicalSpace (E₁ x)
inst_7 : (x : B₂) → AddCommGroup (E₂ x)
inst_8 : (x : B₂) → Module.{u_8, u_15} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
inst_13 : TopologicalSpace B₁
inst_14 : TopologicalSpace B₂
inst_15 : TopologicalSpace M
inst_16 : FiberBundle F₁ E₁
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : FiberBundle F₂ E₂
inst_19 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_8, u_8, u_14, u_15} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ :
  ContinuousWithinAt (Y := F₁ →L[𝕜] F₂) (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m))
    (insert m₀ s) m₀
hv :
  ContinuousWithinAt.{u_13, u_11} (Y := B₁)
      (fun (x : M) ↦ TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ x) (v x)))
      (insert m₀ s) m₀ ∧
    ContinuousWithinAt.{u_13, u_9} (Y := F₁)
      (fun (x : M) ↦
        ((↑(trivializationAt F₁ E₁
                  (TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ m₀) (v m₀)))) :
              TotalSpace F₁ E₁ → B₁ × F₁)
            (TotalSpace.mk (E := E₁) (b₁ x) (v x))).2)
      (insert m₀ s) m₀
hb₂ : ContinuousWithinAt b₂ (insert m₀ s) m₀
A : ∀ᶠ (m : M) in 𝓝[insert m₀ s] m₀, b₁ m ∈ Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀))
A' : ∀ᶠ (m : M) in 𝓝[insert m₀ s] m₀, b₂ m ∈ Trivialization.baseSet (trivializationAt F₂ E₂ (b₂ m₀))
h :
  ∀ (a : M),
    Membership.mem (γ := Set M)
      {x : M |
        Membership.mem (γ := Set M)
            {x : M | (fun (m : M) ↦ b₁ m ∈ Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀))) x} x →
          Membership.mem (γ := Set M)
            {x : M |
              Membership.mem (γ := Set M)
                  {x : M | (fun (m : M) ↦ b₂ m ∈ Trivialization.baseSet (trivializationAt F₂ E₂ (b₂ m₀))) x} x →
                Membership.mem (γ := Set M)
                  {x : M |
                    (fun (x : M) ↦
                        Eq.{u_10 + 1} (α := F₂)
                          ((fun (x : M) ↦
                              ((↑(trivializationAt F₂ E₂
                                        (TotalSpace.proj.{u_12, u_10, u_15} (F := F₂) (E := E₂)
                                          (TotalSpace.mk (E := E₂) (b₂ m₀)
                                            ((ϕ m₀ : (a : E₁ (b₁ m₀)) → E₂ (b₂ m₀)) (v m₀))))) :
                                    TotalSpace F₂ E₂ → B₂ × F₂)
                                  (TotalSpace.mk (E := E₂) (b₂ x) ((ϕ x : (a : E₁ (b₁ x)) → E₂ (b₂ x)) (v x)))).2)
                            x)
                          ((fun (x : M) ↦
                              ((inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ x) (b₂ m₀) (b₂ x) (ϕ x) : (a : F₁) → F₂)
                                  ((↑(trivializationAt F₁ E₁
                                            (TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁)
                                              (TotalSpace.mk (E := E₁) (b₁ m₀) (v m₀)))) :
                                        TotalSpace F₁ E₁ → B₁ × F₁)
                                      (TotalSpace.mk (E := E₁) (b₁ x) (v x))).2 :
                                F₂))
                            x))
                      x}
                  x}
            x}
      a
⊢ Filter.EventuallyEq.{u_13, u_10} (β := F₂) (𝓝[insert m₀ s] m₀)
    (fun (x : M) ↦
      ((↑(trivializationAt F₂ E₂
                (TotalSpace.proj.{u_12, u_10, u_15} (F := F₂) (E := E₂)
                  (TotalSpace.mk (E := E₂) (b₂ m₀) ((ϕ m₀ : (a : E₁ (b₁ m₀)) → E₂ (b₂ m₀)) (v m₀))))) :
            TotalSpace F₂ E₂ → B₂ × F₂)
          (TotalSpace.mk (E := E₂) (b₂ x) ((ϕ x : (a : E₁ (b₁ x)) → E₂ (b₂ x)) (v x)))).2)
    fun (x : M) ↦
    (inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ x) (b₂ m₀) (b₂ x) (ϕ x) : (a : F₁) → F₂)
      ((↑(trivializationAt F₁ E₁
                (TotalSpace.proj.{u_11, u_9, u_14} (F := F₁) (E := E₁) (TotalSpace.mk (E := E₁) (b₁ m₀) (v m₀)))) :
            TotalSpace F₁ E₁ → B₁ × F₁)
          (TotalSpace.mk (E := E₁) (b₁ x) (v x))).2
have h₁ : ∀ (a : M),
  b₁ a ∈ Trivialization.baseSet (trivializationAt F₁ E₁ (b₁ m₀)) →
    b₂ a ∈ Trivialization.baseSet (trivializationAt F₂ E₂ (b₂ m₀)) →
      ((↑(trivializationAt F₂ E₂ (b₂ m₀)) : TotalSpace F₂ E₂ → B₂ × F₂)
            (TotalSpace.mk (E := E₂) (b₂ a) ((ϕ a : (a_3 : E₁ (b₁ a)) → E₂ (b₂ a)) (v a)))).2 =
        (inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ a) (b₂ m₀) (b₂ a) (ϕ a) : (a : F₁) → F₂)
          ((↑(trivializationAt F₁ E₁ (b₁ m₀)) : TotalSpace F₁ E₁ → B₁ × F₁) (TotalSpace.mk (E := E₁) (b₁ a) (v a))).2
Tactic: filter_upwards [A, A'] with m hm h'm using by simp [inCoordinates_eq hm h'm, hm]