-- Module: Mathlib.Geometry.Manifold.MFDeriv.Tangent
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
⊢ 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 := ⋯, 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)) }))
                      (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 := ⋯, 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)))))))
                    ⋯)).symm :
            H × E → M × E)
          (q.proj (E := fun (x : H) ↦ E), q.snd (E := fun (x : H) ↦ E))).1

Tactic:
exact ((chartAt H (TotalSpace.proj p)).right_inv h).symm

Premises used: chartAt, Bundle.TotalSpace.proj, Eq.symm, OpenPartialHomeomorph.right_inv