-- Lean 4 proof step from Mathlib.Geometry.Manifold.MFDeriv.Tangent (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
inst_6 : IsManifold I 1 M
p : TangentBundle I M
q : TangentBundle I H
h :
  q.proj (E := TangentSpace I) ∈
    (OpenPartialHomeomorph.toPartialEquiv (chartAt H (p.proj (E := TangentSpace I)))).target
⊢ ⟨(↑(OpenPartialHomeomorph.symm (chartAt H (p.proj (E := TangentSpace I)))) : H → M) (q.proj (E := TangentSpace I)),
      (fderivWithin 𝕜
            (writtenInExtChartAt I I (q.proj (E := TangentSpace I))
              (↑(OpenPartialHomeomorph.symm (chartAt H (p.proj (E := TangentSpace I)))) : H → M))
            (range (↑I : H → E))
            ((↑(extChartAt I (q.proj (E := TangentSpace I))) : H → E) (q.proj (E := TangentSpace I))) :
          (a : TangentSpace I q.proj) → TangentSpace I ((↑(chartAt H p.proj).symm : H → M) q.proj))
        (q.snd (E := TangentSpace I))⟩ =
    (↑(OpenPartialHomeomorph.symm (chartAt (ModelProd H E) p) :
            OpenPartialHomeomorph (ModelProd H E) (TangentBundle I M)) :
        ModelProd H E → TangentBundle I M)
      ((TotalSpace.toProd H E : (a : TotalSpace E fun (x : H) ↦ E) → H × E) q : H × E)
have simp : Eq (α := TangentBundle I M)
  (⟨(↑(OpenPartialHomeomorph.symm (chartAt H (p.proj (E := TangentSpace I)))) : H → M) (q.proj (E := TangentSpace I)),
      (fderivWithin 𝕜
            (((↑I : H → E) ∘
                (↑(chartAt H
                      ((↑(OpenPartialHomeomorph.symm (chartAt H (p.proj (E := TangentSpace I)))) : H → M)
                        (q.proj (E := TangentSpace I)))) :
                  M → H)) ∘
              (↑(OpenPartialHomeomorph.symm (chartAt H (p.proj (E := TangentSpace I)))) : H → M) ∘ (↑I.symm : E → H))
            (range (↑I : H → E)) ((↑I : H → E) (q.proj (E := TangentSpace I))) :
          (a : TangentSpace I q.proj) → TangentSpace I ((↑(chartAt H p.proj).symm : H → M) q.proj))
        (q.snd (E := TangentSpace I))⟩ :
    TotalSpace.{u_4, u_2, u_2} (B := M) E (TangentSpace I))
  ((↑(OpenPartialHomeomorph.symm
            (Trivialization.toOpenPartialHomeomorph
                (FiberBundleCore.localTriv
                  (VectorBundleCore.toFiberBundleCore
                    {
                      baseSet := fun (i : (↑(atlas H M) : Type (max u_3 u_4))) ↦
                        (↑i : OpenPartialHomeomorph M H).source,
                      isOpen_baseSet := sorry, indexAt := achart H, mem_baseSet_at := sorry,
                      coordChange := fun (i j : (↑(atlas H M) : Type (max u_3 u_4))) (x : M) ↦
                        fderivWithin 𝕜
                          (((↑I : H → E) ∘ (↑(↑j : OpenPartialHomeomorph M H) : M → H)) ∘
                            (↑(↑i : OpenPartialHomeomorph M H).symm : H → M) ∘ (↑I.symm : E → H))
                          (range (↑I : H → E)) ((↑I : H → E) ((↑(↑i : OpenPartialHomeomorph M H) : M → H) x)),
                      coordChange_self := sorry, continuousOn_coordChange := sorry, coordChange_comp := sorry :
                      VectorBundleCore 𝕜 M E (↑(atlas H M) : Type (max u_3 u_4)) })
                  (achart H (p.proj (E := TangentSpace I)))) ≫ₕ
              OpenPartialHomeomorph.prod (chartAt H (p.proj (E := TangentSpace I))) (OpenPartialHomeomorph.refl E))) :
        ModelProd H E → TangentBundle I M)
      (q.proj (E := fun (x : H) ↦ E), q.snd (E := fun (x : H) ↦ E)) :
    TangentBundle I M)
Tactic: simp only [TangentBundle.chartAt, tangentBundleCore,
    mfld_simps, (· ∘ ·)]