-- Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean
theorem ContMDiffOn.contMDiffOn_tangentMapWithin
    (hf : ContMDiffOn I I' n f s) (hmn : m + 1 ≤ n)
    (hs : UniqueMDiffOn I s) :
    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)
    ContMDiffOn I.tangent I'.tangent m (tangentMapWithin I I' f s)
      (π E (TangentSpace I) ⁻¹' s)

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 : M → M'
s : Set M
Is : IsManifold I n M
I's : IsManifold I' n M'
hf : ContMDiffOn I I' n f s
hmn : m + 1 ≤ n
hs : UniqueMDiffOn I s
this✝ : IsManifold I 1 M
this : IsManifold I' 1 M'
x₀ : TangentBundle I M
hx₀ : x₀ ∈ TotalSpace.proj ⁻¹' s
s' : Set (TangentBundle I M) := TotalSpace.proj ⁻¹' s
b₁ : TangentBundle I M → M := fun p => p.proj
v : (y : TangentBundle I M) → TangentSpace I (b₁ y) := fun y => y.snd
hv : ContMDiffWithinAt I.tangent I.tangent m (fun y => { proj := b₁ y, snd := v y }) s' x₀
⊢ ContMDiffWithinAt I.tangent I'.tangent m (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s) x₀

Tactic:
let b₂ : TangentBundle I M → M' := f ∘ b₁

Result:
𝕜 : 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 : M → M'
s : Set M
Is : IsManifold I n M
I's : IsManifold I' n M'
hf : ContMDiffOn I I' n f s
hmn : m + 1 ≤ n
hs : UniqueMDiffOn I s
this✝ : IsManifold I 1 M
this : IsManifold I' 1 M'
x₀ : TangentBundle I M
hx₀ : x₀ ∈ TotalSpace.proj ⁻¹' s
s' : Set (TangentBundle I M) := TotalSpace.proj ⁻¹' s
b₁ : TangentBundle I M → M := fun p => p.proj
v : (y : TangentBundle I M) → TangentSpace I (b₁ y) := fun y => y.snd
hv : ContMDiffWithinAt I.tangent I.tangent m (fun y => { proj := b₁ y, snd := v y }) s' x₀
b₂ : TangentBundle I M → M' := f ∘ b₁
⊢ ContMDiffWithinAt I.tangent I'.tangent m (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s) 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 : M → M'
s : Set M
Is : IsManifold I n M
I's : IsManifold I' n M'
hf : ContMDiffOn I I' n f s
hmn : m + 1 ≤ n
hs : UniqueMDiffOn I s
this✝ : IsManifold I 1 M
this : IsManifold I' 1 M'
x₀ : TangentBundle I M
hx₀ : x₀ ∈ TotalSpace.proj ⁻¹' s
s' : Set (TangentBundle I M) := TotalSpace.proj ⁻¹' s
b₁ : TangentBundle I M → M := fun p => p.proj
v : (y : TangentBundle I M) → TangentSpace I (b₁ y) := fun y => y.snd
hv : ContMDiffWithinAt I.tangent I.tangent m (fun y => { proj := b₁ y, snd := v y }) s' x₀
b₂ : TangentBundle I M → M' := f ∘ b₁
hb₂ : ContMDiffWithinAt I.tangent I' m b₂ s' x₀
ϕ : (y : TangentBundle I M) → TangentSpace I (b₁ y) →L[𝕜] TangentSpace I' (b₂ y) :=
  fun y => mfderivWithin I I' f s (b₁ y)
⊢ ContMDiffWithinAt I.tangent I'.tangent m (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s) x₀

Tactic:
have hϕ : ContMDiffWithinAt I.tangent 𝓘(𝕜, E →L[𝕜] E') m
    (fun y ↦ ContinuousLinearMap.inCoordinates E (TangentSpace I (M := M)) E'
      (TangentSpace I' (M := M')) (b₁ x₀) (b₁ y) (b₂ x₀) (b₂ y) (ϕ y))
    s' x₀ := by
  have A : ContMDiffWithinAt I 𝓘(𝕜, E →L[𝕜] E') m
      (fun y ↦ ContinuousLinearMap.inCoordinates E (TangentSpace I (M := M)) E'
        (TangentSpace I' (M := M')) (b₁ x₀) y (b₂ x₀) (f y) (mfderivWithin I I' f s y))
      s (b₁ x₀) :=
    ContMDiffWithinAt.mfderivWithin_const (hf _ hx₀) hmn hx₀ hs
  exact A.comp _ (contMDiffWithinAt_proj (TangentSpace I)) (fun x h ↦ h)

Result:
𝕜 : 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 : M → M'
s : Set M
Is : IsManifold I n M
I's : IsManifold I' n M'
hf : ContMDiffOn I I' n f s
hmn : m + 1 ≤ n
hs : UniqueMDiffOn I s
this✝ : IsManifold I 1 M
this : IsManifold I' 1 M'
x₀ : TangentBundle I M
hx₀ : x₀ ∈ TotalSpace.proj ⁻¹' s
s' : Set (TangentBundle I M) := TotalSpace.proj ⁻¹' s
b₁ : TangentBundle I M → M := fun p => p.proj
v : (y : TangentBundle I M) → TangentSpace I (b₁ y) := fun y => y.snd
hv : ContMDiffWithinAt I.tangent I.tangent m (fun y => { proj := b₁ y, snd := v y }) s' x₀
b₂ : TangentBundle I M → M' := f ∘ b₁
hb₂ : ContMDiffWithinAt I.tangent I' m b₂ s' x₀
ϕ : (y : TangentBundle I M) → TangentSpace I (b₁ y) →L[𝕜] TangentSpace I' (b₂ y) :=
  fun y => mfderivWithin I I' f s (b₁ y)
hϕ :
  ContMDiffWithinAt I.tangent 𝓘(𝕜, E →L[𝕜] E') m
    (fun y =>
      ContinuousLinearMap.inCoordinates E (TangentSpace I) E' (TangentSpace I') (b₁ x₀) (b₁ y) (b₂ x₀) (b₂ y) (ϕ y))
    s' x₀
⊢ ContMDiffWithinAt I.tangent I'.tangent m (tangentMapWithin I I' f s) (TotalSpace.proj ⁻¹' s) x₀