-- 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
⊢ 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 := ⋯, indexAt := achart H, mem_baseSet_at := ⋯,
                        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 := ⋯, continuousOn_coordChange := ⋯, coordChange_comp := ⋯ :
                        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)
have e_snd : q.proj (E := TangentSpace I) =
  (↑(↑(achart H (p.proj (E := TangentSpace I))) : OpenPartialHomeomorph M H) : M → H)
    ((↑(OpenPartialHomeomorph.toPartialEquiv
                (OpenPartialHomeomorph.restrOpen
                  (OpenPartialHomeomorph.prod (chartAt H (p.proj (E := TangentSpace I))) (OpenPartialHomeomorph.refl E))
                  (PartialEquiv.target (α :=
                    FiberBundleCore.TotalSpace (ι := (↑(atlas H M) : Type (max u_3 u_4)))
                      (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)) }))
                    (OpenPartialHomeomorph.toPartialEquiv
                      (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)))))))
                  sorry)).symm :
          H × E → M × E)
        (q.proj (E := fun (x : H) ↦ E), q.snd (E := fun (x : H) ↦ E))).1
Tactic: congr