-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Hom (goal)
Goal:
𝕜 : Type u_1
B : Type u_2
F₁ : Type u_3
F₂ : Type u_4
E₁ : B → Type u_6
E₂ : B → Type u_7
inst : NontriviallyNormedField 𝕜
inst_1 : (x : B) → AddCommGroup (E₁ x)
inst_2 : (x : B) → Module.{u_1, u_6} 𝕜 (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_7} 𝕜 (E₂ x)
inst_9 : NormedAddCommGroup F₂
inst_10 : NormedSpace 𝕜 F₂
inst_11 : TopologicalSpace (TotalSpace F₂ E₂)
inst_12 : (x : B) → TopologicalSpace (E₂ x)
HB : Type u_9
inst_13 : TopologicalSpace HB
inst_14 : TopologicalSpace B
inst_15 : ChartedSpace HB B
inst_16 : FiberBundle F₁ E₁
inst_17 : VectorBundle 𝕜 F₁ E₁
inst_18 : FiberBundle F₂ E₂
inst_19 : VectorBundle 𝕜 F₂ E₂
inst_20 : ∀ (x : B), IsTopologicalAddGroup.{u_7} (E₂ x)
inst_21 : ∀ (x : B), ContinuousSMul.{u_1, u_7} 𝕜 (E₂ x)
y₀ y : TotalSpace (F₁ →L[𝕜] F₂) fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)
rw :
  (↑(Trivialization.toOpenPartialHomeomorph
              (trivializationAt (F₁ →L[𝕜] F₂)
                (fun (x : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x))
                (y₀.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x)))) ≫ₕ
            OpenPartialHomeomorph.prod
              (chartAt HB
                (y₀.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x))))
              (OpenPartialHomeomorph.refl (F₁ →L[𝕜] F₂))) :
        LE₁E₂ → ModelProd HB (F₁ →L[𝕜] F₂))
      y =
    ((↑(chartAt HB
              (y₀.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))) :
          B → HB)
        (y.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b))),
      inCoordinates F₁ E₁ F₂ E₂
        (y₀.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        (y.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        (y₀.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        (y.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        (y.snd (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b))))
rw₁ :
  (↑(OpenPartialHomeomorph.prod
            (chartAt HB
              (y₀.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x))))
            (OpenPartialHomeomorph.refl (F₁ →L[𝕜] F₂))) :
        B × (F₁ →L[𝕜] F₂) → ModelProd HB (F₁ →L[𝕜] F₂))
      ((↑(Trivialization.toOpenPartialHomeomorph
              (trivializationAt (F₁ →L[𝕜] F₂)
                (fun (x : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x))
                (y₀.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x))))) :
          LE₁E₂ → B × (F₁ →L[𝕜] F₂))
        y) =
    ((↑(chartAt HB
              (y₀.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))) :
          B → HB)
        (y.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b))),
      inCoordinates F₁ E₁ F₂ E₂
        (y₀.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        (y.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        (y₀.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        (y.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        (y.snd (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b))))
rw₂ :
  Eq (α := ModelProd HB (F₁ →L[𝕜] F₂))
    ((fun (p : B × (F₁ →L[𝕜] F₂)) ↦
        ((↑(chartAt HB
                  (y₀.proj (E := fun (x : B) ↦
                    ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x)))) :
              B → HB)
            p.1,
          (↑(OpenPartialHomeomorph.refl (F₁ →L[𝕜] F₂)) : (F₁ →L[𝕜] F₂) → F₁ →L[𝕜] F₂) p.2))
      ((↑(Trivialization.toOpenPartialHomeomorph
              (trivializationAt (F₁ →L[𝕜] F₂)
                (fun (x : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x))
                (y₀.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x))))) :
          LE₁E₂ → B × (F₁ →L[𝕜] F₂))
        y))
    ((↑(chartAt HB
              (y₀.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))) :
          B → HB)
        (y.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b))),
      inCoordinates F₁ E₁ F₂ E₂
        (y₀.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        (y.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        (y₀.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        (y.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        (y.snd (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b))))
rw₃ :
  Eq (α := ModelProd HB (F₁ →L[𝕜] F₂))
    ((fun (p : B × (F₁ →L[𝕜] F₂)) ↦
        ((↑(chartAt HB
                  (y₀.proj (E := fun (x : B) ↦
                    ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x)))) :
              B → HB)
            p.1,
          (↑(OpenPartialHomeomorph.refl (F₁ →L[𝕜] F₂)) : (F₁ →L[𝕜] F₂) → F₁ →L[𝕜] F₂) p.2))
      ((↑(trivializationAt (F₁ →L[𝕜] F₂)
              (fun (x : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x))
              (y₀.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x)))) :
          LE₁E₂ → B × (F₁ →L[𝕜] F₂))
        y))
    ((↑(chartAt HB
              (y₀.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))) :
          B → HB)
        (y.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b))),
      inCoordinates F₁ E₁ F₂ E₂
        (y₀.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        (y.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        (y₀.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        (y.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        (y.snd (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b))))
⊢ Eq (α := ModelProd HB (F₁ →L[𝕜] F₂))
    ((↑(chartAt (ModelProd HB (F₁ →L[𝕜] F₂)) y₀) : LE₁E₂ → ModelProd HB (F₁ →L[𝕜] F₂)) y)
    ((↑(chartAt HB
              (y₀.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))) :
          B → HB)
        (y.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b))),
      inCoordinates F₁ E₁ F₂ E₂
        (y₀.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        (y.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        (y₀.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        (y.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
        (y.snd (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b))))
have rw₄ : Eq (α := ModelProd HB (F₁ →L[𝕜] F₂))
  ((fun (p : B × (F₁ →L[𝕜] F₂)) ↦
      ((↑(chartAt HB
                (y₀.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x)))) :
            B → HB)
          p.1,
        id p.2))
    ((↑(trivializationAt (F₁ →L[𝕜] F₂)
            (fun (x : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x))
            (y₀.proj (E := fun (x : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ x) (E₂ x)))) :
        LE₁E₂ → B × (F₁ →L[𝕜] F₂))
      y))
  ((↑(chartAt HB (y₀.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))) :
        B → HB)
      (y.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b))),
    inCoordinates F₁ E₁ F₂ E₂
      (y₀.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
      (y.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
      (y₀.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
      (y.proj (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b)))
      (y.snd (E := fun (b : B) ↦ ContinuousLinearMap.{u_1, u_1, u_6, u_7} (RingHom.id 𝕜) (E₁ b) (E₂ b))))
Tactic: rw [FiberBundle.chartedSpace_chartAt, trans_apply, OpenPartialHomeomorph.prod_apply,
    Trivialization.coe_coe, OpenPartialHomeomorph.refl_apply, Function.id_def,
    hom_trivializationAt_apply]