-- Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
theorem ContMDiffWithinAt.mfderivWithin {x₀ : N} {f : N → M → M'} {g : N → M}
    {t : Set N} {u : Set M}
    (hf : ContMDiffWithinAt (J.prod I) I' n (Function.uncurry f) (t ×ˢ u) (x₀, g x₀))
    (hg : ContMDiffWithinAt J I m g t x₀) (hx₀ : x₀ ∈ t)
    (hu : MapsTo g t u) (hmn : m + 1 ≤ n) (h'u : UniqueMDiffOn I u) :
    haveI : IsManifold I 1 M := .of_le (le_trans le_add_self hmn)
    haveI : IsManifold I' 1 M' := .of_le (le_trans le_add_self hmn)
    ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
      (inTangentCoordinates I I' g (fun x => f x (g x))
        (fun x => mfderivWithin I I' (f x) u (g x)) x₀) t x₀

Proof state:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m 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'
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J n N
Is : IsManifold I n M
I's : IsManifold I' n M'
x₀ : N
f : N → M → M'
g : N → M
t : Set N
u : Set M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (t ×ˢ u) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g t x₀
hx₀ : x₀ ∈ t
hu : MapsTo g t u
hmn : m + 1 ≤ n
h'u : UniqueMDiffOn I u
this✝² : IsManifold I 1 M
this✝¹ : IsManifold I' 1 M'
this✝ : IsManifold J 1 N
this : IsManifold J m N
t' : Set N := t ∩ g ⁻¹' (extChartAt I (g x₀)).source
ht't : t' ⊆ t
hx₀gx₀ : (x₀, g x₀) ∈ t ×ˢ u
h4f✝ : ContinuousWithinAt (fun x => f x (g x)) t x₀
h4f : (fun x => f x (g x)) ⁻¹' (extChartAt I' (f x₀ (g x₀))).source ∈ 𝓝[t] x₀
h3f : ∀ᶠ (x' : N × M) in 𝓝[t ×ˢ u] (x₀, g x₀), ContMDiffWithinAt (J.prod I) I' 1 (uncurry f) (t ×ˢ u) x'
h2f : ∀ᶠ (x₂ : N) in 𝓝[t] x₀, ContMDiffWithinAt I I' 1 (f x₂) u (g x₂)
h2g : g ⁻¹' (extChartAt I (g x₀)).source ∈ 𝓝[t] x₀
hg' :
  ContinuousWithinAt g t' x₀ ∧
    ContDiffWithinAt 𝕜 m (↑(extChartAt I (g x₀)) ∘ g ∘ ↑(extChartAt J x₀).symm)
      (↑(extChartAt J x₀).symm ⁻¹' t' ∩ range ↑J) (↑(extChartAt J x₀) x₀)
hf' :
  ContinuousWithinAt (uncurry f) (t' ×ˢ u) (x₀, g x₀) ∧
    ContDiffWithinAt 𝕜 n
      (fun x => ↑(extChartAt I' (f x₀ (g x₀))) (f (↑(extChartAt J x₀).symm x.1) (↑(extChartAt I (g x₀)).symm x.2)))
      ((fun p => (↑(extChartAt J x₀).symm p.1, ↑(extChartAt I (g x₀)).symm p.2)) ⁻¹' t' ×ˢ u ∩ range ↑J ×ˢ range ↑I)
      (↑((extChartAt J x₀).prod (extChartAt I (g x₀))) (x₀, g x₀))
⊢ UniqueDiffOn 𝕜 ((extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u)

Tactic:
exact UniqueMDiffOn.uniqueDiffOn_target_inter h'u (g x₀)

Result:
no goals

Proof state:
case h.hg
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
m 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'
F : Type u_8
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_9
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_10
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
Js : IsManifold J n N
Is : IsManifold I n M
I's : IsManifold I' n M'
x₀ : N
f : N → M → M'
g : N → M
t : Set N
u : Set M
hf : ContMDiffWithinAt (J.prod I) I' n (uncurry f) (t ×ˢ u) (x₀, g x₀)
hg : ContMDiffWithinAt J I m g t x₀
hx₀ : x₀ ∈ t
hu : MapsTo g t u
hmn : m + 1 ≤ n
h'u : UniqueMDiffOn I u
this✝⁴ : IsManifold I 1 M
this✝³ : IsManifold I' 1 M'
this✝² : IsManifold J 1 N
this✝¹ : IsManifold J m N
t' : Set N := t ∩ g ⁻¹' (extChartAt I (g x₀)).source
ht't : t' ⊆ t
hx₀gx₀ : (x₀, g x₀) ∈ t ×ˢ u
h4f✝ : ContinuousWithinAt (fun x => f x (g x)) t x₀
h4f : (fun x => f x (g x)) ⁻¹' (extChartAt I' (f x₀ (g x₀))).source ∈ 𝓝[t] x₀
h3f : ∀ᶠ (x' : N × M) in 𝓝[t ×ˢ u] (x₀, g x₀), ContMDiffWithinAt (J.prod I) I' 1 (uncurry f) (t ×ˢ u) x'
h2f : ∀ᶠ (x₂ : N) in 𝓝[t] x₀, ContMDiffWithinAt I I' 1 (f x₂) u (g x₂)
h2g : g ⁻¹' (extChartAt I (g x₀)).source ∈ 𝓝[t] x₀
this✝ :
  ContDiffWithinAt 𝕜 m
    (fun x =>
      fderivWithin 𝕜 (↑(extChartAt I' (f x₀ (g x₀))) ∘ f (↑(extChartAt J x₀).symm x) ∘ ↑(extChartAt I (g x₀)).symm)
        ((extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u)
        (↑(extChartAt I (g x₀)) (g (↑(extChartAt J x₀).symm x))))
    (↑(extChartAt J x₀).symm ⁻¹' t' ∩ range ↑J) (↑(extChartAt J x₀) x₀)
this :
  ContMDiffWithinAt J 𝓘(𝕜, E →L[𝕜] E') m
    (fun x =>
      fderivWithin 𝕜 (↑(extChartAt I' (f x₀ (g x₀))) ∘ f x ∘ ↑(extChartAt I (g x₀)).symm)
        ((extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u) (↑(extChartAt I (g x₀)) (g x)))
    t' x₀
x : N
hx : ContMDiffWithinAt I I' 1 (f x) u (g x)
h'x : x ∈ (fun x => f x (g x)) ⁻¹' (extChartAt I' (f x₀ (g x₀))).source
h2 : x ∈ g ⁻¹' (extChartAt I (g x₀)).source
hxt : x ∈ t
h1 : g x ∈ u
h3 :
  UniqueMDiffWithinAt 𝓘(𝕜, E) ((extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u)
    (↑(extChartAt I (g x₀)) (g x))
A :
  mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I (g x₀)).symm) (range ↑I) (↑(extChartAt I (g x₀)) (g x)) =
    mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I (g x₀)).symm)
      ((extChartAt I (g x₀)).target ∩ ↑(extChartAt I (g x₀)).symm ⁻¹' u) (↑(extChartAt I (g x₀)) (g x))
⊢ MDifferentiableAt I' 𝓘(𝕜, E') (↑(extChartAt I' (f x₀ (g x₀)))) (f x (g x))

Tactic:
exact mdifferentiableAt_extChartAt (by simpa using h'x)

Result:
no goals