-- Lean 4 proof step from Mathlib.Geometry.Manifold.VectorBundle.Tangent (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_4
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
⊢ PartialEquiv.source (β := ModelProd H E) (toPartialEquiv (chartAt (ModelProd H E) p)) =
    (TotalSpace.toProd H E).toPartialEquiv.source
have hs : PartialEquiv.source
    (toPartialEquiv
      ({
          toFun :=
            fun
              (p_1 :
                FiberBundleCore.TotalSpace (ι := (↑(atlas H H) : Type u_4))
                  (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H))) ↦
            (p_1.proj (E :=
                FiberBundleCore.Fiber (ι := (↑(atlas H H) : Type u_4))
                  (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H))),
              FiberBundleCore.coordChange (ι := (↑(atlas H H) : Type u_4))
                (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H))
                (FiberBundleCore.indexAt (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H))
                  (p_1.proj (E :=
                    FiberBundleCore.Fiber (ι := (↑(atlas H H) : Type u_4))
                      (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H)))))
                (achart H (p.proj (E := TangentSpace I)))
                (p_1.proj (E :=
                  FiberBundleCore.Fiber (ι := (↑(atlas H H) : Type u_4))
                    (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H))))
                (p_1.snd (E :=
                  FiberBundleCore.Fiber (ι := (↑(atlas H H) : Type u_4))
                    (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H))))),
          invFun := fun (p_1 : H × E) ↦
            ⟨p_1.1,
              FiberBundleCore.coordChange (ι := (↑(atlas H H) : Type u_4))
                (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H)) (achart H (p.proj (E := TangentSpace I)))
                (FiberBundleCore.indexAt (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H)) p_1.1) p_1.1
                p_1.2⟩,
          source :=
            FiberBundleCore.proj (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H)) ⁻¹'
              (toPartialEquiv (↑(achart H (p.proj (E := TangentSpace I))) : OpenPartialHomeomorph H H)).source,
          target :=
            SProd.sprod (β := Set E)
              (toPartialEquiv (↑(achart H (p.proj (E := TangentSpace I))) : OpenPartialHomeomorph H H)).source univ,
          map_source' := sorry, map_target' := sorry, left_inv' := sorry, right_inv' := sorry, open_source := sorry, open_target := sorry,
          continuousOn_toFun := sorry, continuousOn_invFun := sorry :
          OpenPartialHomeomorph
            (FiberBundleCore.TotalSpace (ι := (↑(atlas H H) : Type u_4))
              (VectorBundleCore.toFiberBundleCore (tangentBundleCore I H)))
            (H × E) } ≫ₕ
        OpenPartialHomeomorph.prod (chartAt H (p.proj (E := TangentSpace I))) (OpenPartialHomeomorph.refl E))) =
  (TotalSpace.toProd H E).toPartialEquiv.source
Tactic: simp_rw [TangentBundle.chartAt, FiberBundleCore.localTriv,
    FiberBundleCore.localTrivAsPartialEquiv, VectorBundleCore.toFiberBundleCore_baseSet,
    tangentBundleCore_baseSet]