-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mdifferentiableOn_iff_target :
    MDifferentiableOn I I' f s ↔
      ContinuousOn f s ∧
        ∀ y : M', MDifferentiableOn I 𝓘(𝕜, E') (extChartAt I' y ∘ f)
          (s ∩ f ⁻¹' (extChartAt I' y).source)

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
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'
f : M → M'
s : Set M
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
⊢ MDifferentiableOn I I' f s ↔
    ContinuousOn f s ∧
      ∀ (y : M'), MDifferentiableOn I 𝓘(𝕜, E') (↑(extChartAt I' y) ∘ f) (s ∩ f ⁻¹' (extChartAt I' y).source)

Tactic:
simp only [mdifferentiableOn_iff, ModelWithCorners.source_eq, chartAt_self_eq,
  PartialHomeomorph.refl_partialEquiv, PartialEquiv.refl_trans, extChartAt,
  PartialHomeomorph.extend, Set.preimage_univ, Set.inter_univ, and_congr_right_iff]

Result:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
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'
f : M → M'
s : Set M
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
⊢ ContinuousOn f s →
    ((∀ (x : M) (y : M'),
        DifferentiableOn 𝕜
          (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘
            f ∘ ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm)
          (((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).target ∩
            ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm ⁻¹'
              (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source))) ↔
      ∀ (y : M'),
        ContinuousOn (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘ f)
            (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source) ∧
          ∀ (x : M),
            E' →
              DifferentiableOn 𝕜
                (↑𝓘(𝕜, E').toPartialEquiv ∘
                  (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘ f) ∘
                    ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm)
                (((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).target ∩
                  ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm ⁻¹'
                    (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source)))

Proof state:
case h.e'_6.h.e'_4.h.e'_4
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
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'
f : M → M'
s : Set M
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
h : ContinuousOn f s
h' :
  ∀ (x : M) (y : M'),
    DifferentiableOn 𝕜
      (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘
        f ∘ ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm)
      (((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).target ∩
        ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm ⁻¹'
          (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source))
y : M'
h'' : ContinuousOn (↑I') univ
⊢ ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source =
    (chartAt H' y).source ∩ ↑(chartAt H' y).toPartialEquiv ⁻¹' univ

Tactic:
simp

Result:
no goals

Proof state:
case mp
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
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'
f : M → M'
s : Set M
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
h : ContinuousOn f s
h' :
  ∀ (x : M) (y : M'),
    DifferentiableOn 𝕜
      (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘
        f ∘ ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm)
      (((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).target ∩
        ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm ⁻¹'
          (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source))
y : M'
h'' : ContinuousOn (↑I') univ
⊢ ContinuousOn (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘ f)
    (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source)

Tactic:
convert (h''.comp_inter (chartAt H' y).continuousOn_toFun).comp_inter h

Result:
case h.e'_6.h.e'_4.h.e'_4
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
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'
f : M → M'
s : Set M
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
h : ContinuousOn f s
h' :
  ∀ (x : M) (y : M'),
    DifferentiableOn 𝕜
      (↑((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv) ∘
        f ∘ ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm)
      (((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).target ∩
        ↑((chartAt H x).toPartialEquiv ≫ I.toPartialEquiv).symm ⁻¹'
          (s ∩ f ⁻¹' ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source))
y : M'
h'' : ContinuousOn (↑I') univ
⊢ ((chartAt H' y).toPartialEquiv ≫ I'.toPartialEquiv).source =
    (chartAt H' y).source ∩ ↑(chartAt H' y).toPartialEquiv ⁻¹' univ