-- Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
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
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U :
  ∀ (w : H) (w' : H'),
    UniqueDiffWithinAt 𝕜 (range (Prod.map (↑I : H → E) (↑I' : H' → E'))) ((↑I : H → E) w, (↑I' : H' → E') w')
smooth_pM : ContMDiffAt (I.tangent.prod I'.tangent) I.tangent n Prod.fst (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp :
  p.1.proj (E := TangentSpace I) ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H (a.proj (E := TangentSpace I)))).source ∧
    p.2.proj (E := TangentSpace I') ∈
      (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (b.proj (E := TangentSpace I')))).source
φ : (x : E) → E :=
  fun (x : E) ↦
    (↑I : H → E)
      ((↑(chartAt H (a.proj (E := TangentSpace I))) : M → H)
        ((↑(OpenPartialHomeomorph.symm (chartAt H (p.1.proj (E := TangentSpace I)))) : H → M) ((↑I.symm : E → H) x)))
D0 :
  DifferentiableWithinAt 𝕜 φ (range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))))
D :
  ∀ (w : TangentBundle I' M'),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.fst) (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
      ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))),
        (↑I' : H' → E') ((↑(chartAt H' (w.proj (E := TangentSpace I'))) : M' → H') (w.proj (E := TangentSpace I'))))
h :
  Eq (α := E)
    (((ContinuousLinearMap.prod
              (fderivWithin 𝕜
                (fun (x : E × E') ↦
                  (↑I : H → E)
                    ((↑(chartAt H (a.proj (E := TangentSpace I))) : M → H)
                      ((↑((OpenPartialHomeomorph.toPartialEquiv (chartAt H (p.1.proj (E := TangentSpace I)))).prod
                                  (OpenPartialHomeomorph.toPartialEquiv
                                    (chartAt H' (p.2.proj (E := TangentSpace I'))))).symm :
                            ModelProd H H' → M × M')
                          ((↑(I.prod I'.toPartialEquiv).symm : E × E' → ModelProd H H') x)).1))
                (range (↑I : H → E) ×ˢ range (↑I' : H' → E'))
                ((↑I : H → E)
                    ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))),
                  (↑I' : H' → E')
                    ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I')))))
              (fderivWithin 𝕜
                (fun (x : E × E') ↦
                  (↑I' : H' → E')
                    ((↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H')
                      ((↑((OpenPartialHomeomorph.toPartialEquiv (chartAt H (p.1.proj (E := TangentSpace I)))).prod
                                  (OpenPartialHomeomorph.toPartialEquiv
                                    (chartAt H' (p.2.proj (E := TangentSpace I'))))).symm :
                            ModelProd H H' → M × M')
                          ((↑(I.prod I'.toPartialEquiv).symm : E × E' → ModelProd H H') x)).2))
                (range (↑I : H → E) ×ˢ range (↑I' : H' → E'))
                ((↑I : H → E)
                    ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))),
                  (↑I' : H' → E')
                    ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))) :
            (a : E × E') → E × E')
          (p.1.snd (E := TangentSpace I), p.2.snd (E := TangentSpace I'))).1 :
      E)
    ((fderivWithin 𝕜
            (((↑I : H → E) ∘ (↑(chartAt H (a.proj (E := TangentSpace I))) : M → H)) ∘
              (↑(OpenPartialHomeomorph.symm (chartAt H (p.1.proj (E := TangentSpace I)))) : H → M) ∘ (↑I.symm : E → H))
            (range (↑I : H → E))
            ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I)))) :
          (a : E) → E)
        (p.1.snd (E := TangentSpace I)) :
      E)
⊢ ((ContinuousLinearMap.prod
            (fderivWithin 𝕜
              (fun (x : E × E') ↦
                (↑I : H → E)
                  ((↑(chartAt H (a.proj (E := TangentSpace I))) : M → H)
                    ((↑((OpenPartialHomeomorph.toPartialEquiv (chartAt H (p.1.proj (E := TangentSpace I)))).prod
                                (OpenPartialHomeomorph.toPartialEquiv
                                  (chartAt H' (p.2.proj (E := TangentSpace I'))))).symm :
                          ModelProd H H' → M × M')
                        ((↑(I.prod I'.toPartialEquiv).symm : E × E' → ModelProd H H') x)).1))
              (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
              ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))),
                (↑I' : H' → E')
                  ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I')))))
            (fderivWithin 𝕜
              (fun (x : E × E') ↦
                (↑I' : H' → E')
                  ((↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H')
                    ((↑((OpenPartialHomeomorph.toPartialEquiv (chartAt H (p.1.proj (E := TangentSpace I)))).prod
                                (OpenPartialHomeomorph.toPartialEquiv
                                  (chartAt H' (p.2.proj (E := TangentSpace I'))))).symm :
                          ModelProd H H' → M × M')
                        ((↑(I.prod I'.toPartialEquiv).symm : E × E' → ModelProd H H') x)).2))
              (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
              ((↑I : H → E) ((↑(chartAt H (p.1.proj (E := TangentSpace I))) : M → H) (p.1.proj (E := TangentSpace I))),
                (↑I' : H' → E')
                  ((↑(chartAt H' (p.2.proj (E := TangentSpace I'))) : M' → H') (p.2.proj (E := TangentSpace I'))))) :
          (a : E × E') → E × E')
        (p.1.snd (E := TangentSpace I), p.2.snd (E := TangentSpace I'))).1 =
    ((↑(trivializationAt E (TangentSpace I) (a.proj (E := TangentSpace I))) : TotalSpace E (TangentSpace I) → M × E)
        p.1).2

Tactic:
simp only [TangentBundle.trivializationAt_apply, mfld_simps]

Premises used: TangentBundle.trivializationAt_apply