-- 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')
refine_1 :
  ContMDiffAt (I.tangent.prod I'.tangent) (I.prod I') (M' := M × M') n
    (fun (x : TangentBundle I M × TangentBundle I' M') ↦
      (x.1.proj (E := TangentSpace I), x.2.proj (E := TangentSpace I')))
    (a, b)
refine_2 :
  ContMDiffAt (I.tangent.prod I'.tangent) 𝓘(𝕜, E) (M' := E) n
    (Function.comp (β := E × E') Prod.fst fun (x : TangentBundle I M × TangentBundle I' M') ↦
      (fderivWithin 𝕜
            (((fun (p : H × H') ↦ ((↑I : H → E) p.1, (↑I' : H' → E') p.2)) ∘ fun (p : M × M') ↦
                ((↑(chartAt H (a.proj (E := TangentSpace I))) : M → H) p.1,
                  (↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H') p.2)) ∘
              (↑((OpenPartialHomeomorph.toPartialEquiv (chartAt H (x.1.proj (E := TangentSpace I)))).prod
                        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (x.2.proj (E := TangentSpace I'))))).symm :
                  ModelProd H H' → M × M') ∘
                (↑(I.prod I'.toPartialEquiv).symm : E × E' → ModelProd H H'))
            (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
            ((↑I : H → E) ((↑(chartAt H (x.1.proj (E := TangentSpace I))) : M → H) (x.1.proj (E := TangentSpace I))),
              (↑I' : H' → E')
                ((↑(chartAt H' (x.2.proj (E := TangentSpace I'))) : M' → H') (x.2.proj (E := TangentSpace I')))) :
          (a : E × E') → E × E')
        (x.1.snd (E := TangentSpace I), x.2.snd (E := TangentSpace I')))
    (a, b)
refine_3 :
  ContMDiffAt (I.tangent.prod I'.tangent) 𝓘(𝕜, E') (M' := E') n
    (Function.comp (β := E × E') Prod.snd fun (x : TangentBundle I M × TangentBundle I' M') ↦
      (fderivWithin 𝕜
            (((fun (p : H × H') ↦ ((↑I : H → E) p.1, (↑I' : H' → E') p.2)) ∘ fun (p : M × M') ↦
                ((↑(chartAt H (a.proj (E := TangentSpace I))) : M → H) p.1,
                  (↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H') p.2)) ∘
              (↑((OpenPartialHomeomorph.toPartialEquiv (chartAt H (x.1.proj (E := TangentSpace I)))).prod
                        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (x.2.proj (E := TangentSpace I'))))).symm :
                  ModelProd H H' → M × M') ∘
                (↑(I.prod I'.toPartialEquiv).symm : E × E' → ModelProd H H'))
            (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
            ((↑I : H → E) ((↑(chartAt H (x.1.proj (E := TangentSpace I))) : M → H) (x.1.proj (E := TangentSpace I))),
              (↑I' : H' → E')
                ((↑(chartAt H' (x.2.proj (E := TangentSpace I'))) : M' → H') (x.2.proj (E := TangentSpace I')))) :
          (a : E × E') → E × E')
        (x.1.snd (E := TangentSpace I), x.2.snd (E := TangentSpace I')))
    (a, b)
⊢ ContMDiffAt (I.tangent.prod I'.tangent) (I.prod I') (M' := M × M') n
      (fun (x : TangentBundle I M × TangentBundle I' M') ↦
        (x.1.proj (E := TangentSpace I), x.2.proj (E := TangentSpace I')))
      (a, b) ∧
    ContMDiffAt (I.tangent.prod I'.tangent) (E' := E × E') 𝓘(𝕜, E × E') (M' := E × E') n
      (fun (x : TangentBundle I M × TangentBundle I' M') ↦
        (fderivWithin 𝕜
              (((fun (p : H × H') ↦ ((↑I : H → E) p.1, (↑I' : H' → E') p.2)) ∘ fun (p : M × M') ↦
                  ((↑(chartAt H (a.proj (E := TangentSpace I))) : M → H) p.1,
                    (↑(chartAt H' (b.proj (E := TangentSpace I'))) : M' → H') p.2)) ∘
                (↑((OpenPartialHomeomorph.toPartialEquiv (chartAt H (x.1.proj (E := TangentSpace I)))).prod
                          (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (x.2.proj (E := TangentSpace I'))))).symm :
                    ModelProd H H' → M × M') ∘
                  (↑(I.prod I'.toPartialEquiv).symm : E × E' → ModelProd H H'))
              (range (Prod.map (↑I : H → E) (↑I' : H' → E')))
              ((↑I : H → E) ((↑(chartAt H (x.1.proj (E := TangentSpace I))) : M → H) (x.1.proj (E := TangentSpace I))),
                (↑I' : H' → E')
                  ((↑(chartAt H' (x.2.proj (E := TangentSpace I'))) : M' → H') (x.2.proj (E := TangentSpace I')))) :
            (a : E × E') → E × E')
          (x.1.snd (E := TangentSpace I), x.2.snd (E := TangentSpace I')))
      (a, b)

Tactic:
refine ⟨?_, (contMDiffAt_prod_module_iff _).2 ⟨?_, ?_⟩⟩