Module: Mathlib.Geometry.Manifold.ContMDiffMFDeriv

Goal state before:
pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range (Prod.map ↑I ↑I')) (↑I w, ↑I' w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp : p.1.proj ∈ (chartAt H a.proj).source ∧ p.2.proj ∈ (chartAt H' b.proj).source
φ : E' → E' := fun x ↦ ↑I' (↑(chartAt H' b.proj) (↑(chartAt H' p.2.proj).symm (↑I'.symm x)))
D0 : DifferentiableWithinAt 𝕜 φ (range ↑I') (↑I' (↑(chartAt H' p.2.proj) p.2.proj))
D :
  ∀ (w : TangentBundle I M),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.snd) (range (Prod.map ↑I ↑I'))
      (↑I (↑(chartAt H w.proj) w.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj))
⊢ DifferentiableWithinAt 𝕜
    (fun x ↦
      ↑I
        (↑(chartAt H a.proj)
          (↑((chartAt H p.1.proj).prod (chartAt H' p.2.proj).toPartialEquiv).symm
              (↑(I.prod I'.toPartialEquiv).symm x)).1))
    (range (Prod.map ↑I ↑I')) (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj))

pp: 𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range (Prod.map ↑I ↑I')) (↑I w, ↑I' w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp : p.1.proj ∈ (chartAt H a.proj).source ∧ p.2.proj ∈ (chartAt H' b.proj).source
φ : E' → E' := fun x ↦ ↑I' (↑(chartAt H' b.proj) (↑(chartAt H' p.2.proj).symm (↑I'.symm x)))
D0 : DifferentiableWithinAt 𝕜 φ (range ↑I') (↑I' (↑(chartAt H' p.2.proj) p.2.proj))
D :
  ∀ (w : TangentBundle I M),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.snd) (range (Prod.map ↑I ↑I'))
      (↑I (↑(chartAt H w.proj) w.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj))
⊢ (((fderivWithin 𝕜
              (fun x ↦
                ↑I
                  (↑(chartAt H a.proj)
                    (↑((chartAt H p.1.proj).prod (chartAt H' p.2.proj).toPartialEquiv).symm
                        (↑(I.prod I'.toPartialEquiv).symm x)).1))
              (range (Prod.map ↑I ↑I'))
              (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj))).prod
          (fderivWithin 𝕜
            (fun x ↦
              ↑I'
                (↑(chartAt H' b.proj)
                  (↑((chartAt H p.1.proj).prod (chartAt H' p.2.proj).toPartialEquiv).symm
                      (↑(I.prod I'.toPartialEquiv).symm x)).2))
            (range (Prod.map ↑I ↑I')) (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj))))
        (p.1.snd, p.2.snd)).2 =
    (↑(trivializationAt E' (TangentSpace I') b.proj) p.2).2

Tactic:
· let φ' (x : E) := I ((chartAt H a.proj) ((chartAt H p.1.proj).symm (I.symm x)))
      have D0' : DifferentiableWithinAt 𝕜 φ' (Set.range I)
          (I ((chartAt H p.1.proj) p.1.proj)) := by
        apply ContDiffWithinAt.differentiableWithinAt _ one_ne_zero
        apply contDiffWithinAt_ext_coord_change
        simp [hp.1]
      have D' : DifferentiableWithinAt 𝕜 (φ' ∘ Prod.fst) (Set.range (Prod.map I I'))
          (I ((chartAt H p.1.proj) p.1.proj), I' ((chartAt H' p.2.proj) p.2.proj)) :=
        DifferentiableWithinAt.comp (t := Set.range I) _ (by exact D0')
          differentiableWithinAt_fst (by simp [mapsTo_fst_prod])
      exact D'

Goal state after:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
n : WithTop ℕ∞
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
a : TangentBundle I M
b : TangentBundle I' M'
U : ∀ (w : H) (w' : H'), UniqueDiffWithinAt 𝕜 (range (Prod.map ↑I ↑I')) (↑I w, ↑I' w')
smooth_pM' : ContMDiffAt (I.tangent.prod I'.tangent) I'.tangent n Prod.snd (a, b)
p : TangentBundle I M × TangentBundle I' M'
hp : p.1.proj ∈ (chartAt H a.proj).source ∧ p.2.proj ∈ (chartAt H' b.proj).source
φ : E' → E' := fun x ↦ ↑I' (↑(chartAt H' b.proj) (↑(chartAt H' p.2.proj).symm (↑I'.symm x)))
D0 : DifferentiableWithinAt 𝕜 φ (range ↑I') (↑I' (↑(chartAt H' p.2.proj) p.2.proj))
D :
  ∀ (w : TangentBundle I M),
    DifferentiableWithinAt 𝕜 (φ ∘ Prod.snd) (range (Prod.map ↑I ↑I'))
      (↑I (↑(chartAt H w.proj) w.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj))
⊢ (((fderivWithin 𝕜
              (fun x ↦
                ↑I
                  (↑(chartAt H a.proj)
                    (↑((chartAt H p.1.proj).prod (chartAt H' p.2.proj).toPartialEquiv).symm
                        (↑(I.prod I'.toPartialEquiv).symm x)).1))
              (range (Prod.map ↑I ↑I'))
              (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj))).prod
          (fderivWithin 𝕜
            (fun x ↦
              ↑I'
                (↑(chartAt H' b.proj)
                  (↑((chartAt H p.1.proj).prod (chartAt H' p.2.proj).toPartialEquiv).symm
                      (↑(I.prod I'.toPartialEquiv).symm x)).2))
            (range (Prod.map ↑I ↑I')) (↑I (↑(chartAt H p.1.proj) p.1.proj), ↑I' (↑(chartAt H' p.2.proj) p.2.proj))))
        (p.1.snd, p.2.snd)).2 =
    (↑(trivializationAt E' (TangentSpace I') b.proj) p.2).2