-- Mathlib/Geometry/Manifold/MFDeriv/Tangent.lean
/-- To write a linear map between tangent spaces in coordinates amounts to precomposing and
postcomposing it with derivatives of extended charts.
Concrete version of `inTangentCoordinates_eq`. -/
lemma inTangentCoordinates_eq_mfderiv_comp
    {N : Type*} {f : N → M} {g : N → M'}
    {ϕ : Π x : N, TangentSpace I (f x) →L[𝕜] TangentSpace I' (g x)} {x₀ : N} {x : N}
    (hx : f x ∈ (chartAt H (f x₀)).source) (hy : g x ∈ (chartAt H' (g x₀)).source) :
    inTangentCoordinates I I' f g ϕ x₀ x =
    (mfderiv I' 𝓘(𝕜, E') (extChartAt I' (g x₀)) (g x)) ∘L (ϕ x) ∘L
      (mfderivWithin 𝓘(𝕜, E) I (extChartAt I (f x₀)).symm (range I)
        (extChartAt I (f x₀) (f x)))

Proof state:
case e_f.e_f.hc.h
𝕜 : 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
inst✝⁶ : IsManifold I 1 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'
inst✝ : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → TangentSpace I (f x) →L[𝕜] TangentSpace I' (g x)
x₀ x : N
hx : f x ∈ (chartAt H (f x₀)).source
hy : g x ∈ (chartAt H' (g x₀)).source
⊢ f x ∈ (extChartAt I (f x₀)).source

Tactic:
simpa using hx

Result:
no goals

Proof state:
case e_f.e_f.hc
𝕜 : 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
inst✝⁶ : IsManifold I 1 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'
inst✝ : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → TangentSpace I (f x) →L[𝕜] TangentSpace I' (g x)
x₀ x : N
hx : f x ∈ (chartAt H (f x₀)).source
hy : g x ∈ (chartAt H' (g x₀)).source
⊢ MDifferentiableWithinAt 𝓘(𝕜, E) I (↑(extChartAt I (f x₀)).symm) (range ↑I) (↑(extChartAt I (f x₀)) (f x))

Tactic:
apply mdifferentiableWithinAt_extChartAt_symm

Result:
case e_f.e_f.hc.h
𝕜 : 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
inst✝⁶ : IsManifold I 1 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'
inst✝ : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → TangentSpace I (f x) →L[𝕜] TangentSpace I' (g x)
x₀ x : N
hx : f x ∈ (chartAt H (f x₀)).source
hy : g x ∈ (chartAt H' (g x₀)).source
⊢ ↑(extChartAt I (f x₀)) (f x) ∈ (extChartAt I (f x₀)).target

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
inst✝⁶ : IsManifold I 1 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'
inst✝ : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → TangentSpace I (f x) →L[𝕜] TangentSpace I' (g x)
x₀ x : N
hx : f x ∈ (chartAt H (f x₀)).source
hy : g x ∈ (chartAt H' (g x₀)).source
⊢ inTangentCoordinates I I' f g ϕ x₀ x =
    (mfderiv I' 𝓘(𝕜, E') (↑(extChartAt I' (g x₀))) (g x)).comp
      ((ϕ x).comp (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I (f x₀)).symm) (range ↑I) (↑(extChartAt I (f x₀)) (f x))))

Tactic:
rw [inTangentCoordinates_eq _ _ _ hx hy, tangentBundleCore_coordChange]

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
inst✝⁶ : IsManifold I 1 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'
inst✝ : IsManifold I' 1 M'
N : Type u_8
f : N → M
g : N → M'
ϕ : (x : N) → TangentSpace I (f x) →L[𝕜] TangentSpace I' (g x)
x₀ x : N
hx : f x ∈ (chartAt H (f x₀)).source
hy : g x ∈ (chartAt H' (g x₀)).source
⊢ (fderivWithin 𝕜 (↑((↑(achart H' (g x₀))).extend I') ∘ ↑((↑(achart H' (g x))).extend I').symm) (range ↑I')
          (↑((↑(achart H' (g x))).extend I') (g x))).comp
      ((ϕ x).comp ((tangentBundleCore I M).coordChange (achart H (f x₀)) (achart H (f x)) (f x))) =
    (mfderiv I' 𝓘(𝕜, E') (↑(extChartAt I' (g x₀))) (g x)).comp
      ((ϕ x).comp (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I (f x₀)).symm) (range ↑I) (↑(extChartAt I (f x₀)) (f x))))