-- Module: Mathlib.Geometry.Manifold.VectorBundle.Tangent
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
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' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯, open_source := ⋯, open_target := ⋯,
            continuousOn_toFun := ⋯, continuousOn_invFun := ⋯ :
            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
⊢ PartialEquiv.source (β := ModelProd H E) (toPartialEquiv (chartAt (ModelProd H E) p)) =
    (TotalSpace.toProd H E).toPartialEquiv.source

Tactic:
simp_rw [TangentBundle.chartAt, FiberBundleCore.localTriv,
    FiberBundleCore.localTrivAsPartialEquiv, VectorBundleCore.toFiberBundleCore_baseSet,
    tangentBundleCore_baseSet]

Premises used: TangentBundle.chartAt, FiberBundleCore.localTriv, FiberBundleCore.localTrivAsPartialEquiv, tangentBundleCore_baseSet, VectorBundleCore.toFiberBundleCore_baseSet