-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
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'
f : M → M'
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
h : ContinuousOn f s
mp :
  (∀ (x : M) (y : M'),
      DifferentiableOn 𝕜
        ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘
          f ∘ (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
        ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
          (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
            (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source))) →
    ∀ (y : M'),
      ContinuousOn ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘ f)
          (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source) ∧
        ∀ (x : M) (y_1 : E'),
          DifferentiableOn 𝕜
            ((↑(ModelWithCorners.toPartialEquiv 𝓘(𝕜, E')) : E' → E') ∘
              ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘ f) ∘
                (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
            ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
              (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
                (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source))
mpr :
  (∀ (y : M'),
      ContinuousOn ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘ f)
          (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source) ∧
        ∀ (x : M) (y_1 : E'),
          DifferentiableOn 𝕜
            ((↑(ModelWithCorners.toPartialEquiv 𝓘(𝕜, E')) : E' → E') ∘
              ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘ f) ∘
                (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
            ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
              (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
                (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source))) →
    ∀ (x : M) (y : M'),
      DifferentiableOn 𝕜
        ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘
          f ∘ (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
        ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
          (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
            (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source))
⊢ (∀ (x : M) (y : M'),
      DifferentiableOn 𝕜
        ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘
          f ∘ (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
        ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
          (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
            (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source))) ↔
    ∀ (y : M'),
      ContinuousOn ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘ f)
          (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source) ∧
        ∀ (x : M) (y_1 : E'),
          DifferentiableOn 𝕜
            ((↑(ModelWithCorners.toPartialEquiv 𝓘(𝕜, E')) : E' → E') ∘
              ((↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv) : M' → E') ∘ f) ∘
                (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M))
            ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).target ∩
              (↑(OpenPartialHomeomorph.toPartialEquiv (chartAt H x) ≫ I.toPartialEquiv).symm : E → M) ⁻¹'
                (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y) ≫ I'.toPartialEquiv).source))

Tactic:
constructor