-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mdifferentiableOn_iff_of_mem_maximalAtlas (he : e ∈ maximalAtlas I 1 M)
    (he' : e' ∈ maximalAtlas I' 1 M') (hs : s ⊆ e.source) (h2s : MapsTo f s e'.source) :
    MDifferentiableOn I I' f s ↔
      ContinuousOn f s ∧
        DifferentiableOn 𝕜 (e'.extend I' ∘ f ∘ (e.extend I).symm) (e.extend I '' s)

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
e : PartialHomeomorph M H
e' : PartialHomeomorph M' H'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
he : e ∈ maximalAtlas I 1 M
he' : e' ∈ maximalAtlas I' 1 M'
hs : s ⊆ e.source
h2s : MapsTo f s e'.source
⊢ (∀ x ∈ s, MDifferentiableWithinAt I I' f s x) ↔
    ∀ x ∈ s,
      ContinuousWithinAt f s x ∧
        DifferentiableWithinAt 𝕜 (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s) (↑(e.extend I) x)

Tactic:
exact forall₂_congr fun x hx => mdifferentiableWithinAt_iff_image he he' hs (hs hx) (h2s hx)

Result:
no goals

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
e : PartialHomeomorph M H
e' : PartialHomeomorph M' H'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
he : e ∈ maximalAtlas I 1 M
he' : e' ∈ maximalAtlas I' 1 M'
hs : s ⊆ e.source
h2s : MapsTo f s e'.source
⊢ MDifferentiableOn I I' f s ↔
    ContinuousOn f s ∧ DifferentiableOn 𝕜 (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s)

Tactic:
simp_rw [ContinuousOn, DifferentiableOn, Set.forall_mem_image, ← forall_and, MDifferentiableOn]

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
e : PartialHomeomorph M H
e' : PartialHomeomorph M' H'
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
he : e ∈ maximalAtlas I 1 M
he' : e' ∈ maximalAtlas I' 1 M'
hs : s ⊆ e.source
h2s : MapsTo f s e'.source
⊢ (∀ x ∈ s, MDifferentiableWithinAt I I' f s x) ↔
    ∀ x ∈ s,
      ContinuousWithinAt f s x ∧
        DifferentiableWithinAt 𝕜 (↑(e'.extend I') ∘ f ∘ ↑(e.extend I).symm) (↑(e.extend I) '' s) (↑(e.extend I) x)