-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_1
F₁ : Type u_2
F₂ : Type u_3
B₁ : Type u_4
B₂ : Type u_5
M : Type u_6
E₁ : B₁ → Type u_7
E₂ : B₂ → Type u_8
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B₁) → AddCommGroup (E₁ x)
inst_2 : (x : B₁) → Module.{u_1, u_7} 𝕜 (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_1, u_8} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B₂) → TopologicalSpace (E₂ x)
EB₁ : Type u_9
inst_13 : NormedAddCommGroup EB₁
inst_14 : NormedSpace 𝕜 EB₁
HB₁ : Type u_10
inst_15 : TopologicalSpace HB₁
IB₁ : ModelWithCorners 𝕜 EB₁ HB₁
inst_16 : TopologicalSpace B₁
inst_17 : ChartedSpace HB₁ B₁
EB₂ : Type u_11
inst_18 : NormedAddCommGroup EB₂
inst_19 : NormedSpace 𝕜 EB₂
HB₂ : Type u_12
inst_20 : TopologicalSpace HB₂
IB₂ : ModelWithCorners 𝕜 EB₂ HB₂
inst_21 : TopologicalSpace B₂
inst_22 : ChartedSpace HB₂ B₂
EM : Type u_13
inst_23 : NormedAddCommGroup EM
inst_24 : NormedSpace 𝕜 EM
HM : Type u_14
inst_25 : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
inst_26 : TopologicalSpace M
inst_27 : ChartedSpace HM M
n : WithTop ℕ∞
inst_28 : FiberBundle F₁ E₁
inst_29 : VectorBundle 𝕜 F₁ E₁
inst_30 : FiberBundle F₂ E₂
inst_31 : VectorBundle 𝕜 F₂ E₂
b₁ : M → B₁
b₂ : M → B₂
m₀ : M
ϕ : (m : M) → ContinuousLinearMap.{u_1, u_1, u_7, u_8} (RingHom.id 𝕜) (E₁ (b₁ m)) (E₂ (b₂ m))
v : (m : M) → E₁ (b₁ m)
s : Set M
hϕ :
  ContMDiffWithinAt IM (E' := F₁ →L[𝕜] F₂) 𝓘(𝕜, F₁ →L[𝕜] F₂) (M' := F₁ →L[𝕜] F₂) n
    (fun (m : M) ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) (insert m₀ s) m₀
hv :
  ContMDiffWithinAt.{u_1, u_13, u_14, u_6, u_9, u_10, u_4} IM IB₁ (M' := B₁) n
      (fun (x : M) ↦ TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ x, v x⟩) (insert m₀ s) m₀ ∧
    ContMDiffWithinAt IM 𝓘(𝕜, F₁) (M' := F₁) n
      (fun (x : M) ↦
        ((↑(trivializationAt F₁ E₁ (TotalSpace.proj.{u_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ m₀, v m₀⟩)) :
              TotalSpace F₁ E₁ → B₁ × F₁)
            ⟨b₁ x, v x⟩).2)
      (insert m₀ s) m₀
hb₂ : ContMDiffWithinAt IM IB₂ n b₂ (insert m₀ s) m₀
⊢ ContMDiffWithinAt IM 𝓘(𝕜, F₂) (M' := F₂) n
    (fun (x : M) ↦
      ((↑(trivializationAt F₂ E₂
                (TotalSpace.proj.{u_5, u_3, u_8} (F := F₂) (E := E₂)
                  ⟨b₂ m₀, (ϕ m₀ : (a : E₁ (b₁ m₀)) → E₂ (b₂ m₀)) (v m₀)⟩)) :
            TotalSpace F₂ E₂ → B₂ × F₂)
          ⟨b₂ x, (ϕ x : (a : E₁ (b₁ x)) → E₂ (b₂ x)) (v x)⟩).2)
    (insert m₀ s) m₀
have apply : Filter.EventuallyEq.{u_6, u_3} (β := F₂) (𝓝[insert m₀ s] m₀)
  (fun (x : M) ↦
    ((↑(trivializationAt F₂ E₂
              (TotalSpace.proj.{u_5, u_3, u_8} (F := F₂) (E := E₂)
                ⟨b₂ m₀, (ϕ m₀ : (a : E₁ (b₁ m₀)) → E₂ (b₂ m₀)) (v m₀)⟩)) :
          TotalSpace F₂ E₂ → B₂ × F₂)
        ⟨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_4, u_2, u_7} (F := F₁) (E := E₁) ⟨b₁ m₀, v m₀⟩)) :
          TotalSpace F₁ E₁ → B₁ × F₁)
        ⟨b₁ x, v x⟩).2
Tactic: apply (ContMDiffWithinAt.clm_apply hϕ hv.2).congr_of_eventuallyEq_of_mem ?_ (mem_insert m₀ s)