-- Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
/-- The composition of the derivative of the inverse of `extChartAt` with the derivative of
`extChartAt` gives the identity.
Version where the basepoint belongs to `(extChartAt I x).target`. -/
lemma mfderivWithin_extChartAt_symm_comp_mfderiv_extChartAt
    {y : E} (hy : y ∈ (extChartAt I x).target) :
    (mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) y) ∘L
      (mfderiv I 𝓘(𝕜, E) (extChartAt I x) ((extChartAt I x).symm y))
      = ContinuousLinearMap.id _ _

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
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source (↑(extChartAt I x).symm y)
⊢ (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) y).comp
      (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm y)) =
    ContinuousLinearMap.id 𝕜 (TangentSpace I (↑(extChartAt I x).symm y))

Tactic:
have : mfderiv I 𝓘(𝕜, E) (extChartAt I x) ((extChartAt I x).symm y)
    = mfderivWithin I 𝓘(𝕜, E) (extChartAt I x) (extChartAt I x).source
    ((extChartAt I x).symm y) := by
  rw [mfderivWithin_eq_mfderiv U']
  exact mdifferentiableAt_extChartAt h''y

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
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source (↑(extChartAt I x).symm y)
this :
  mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm y) =
    mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x)) (extChartAt I x).source (↑(extChartAt I x).symm y)
⊢ (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) y).comp
      (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm y)) =
    ContinuousLinearMap.id 𝕜 (TangentSpace I (↑(extChartAt I x).symm y))

Proof state:
case hL
𝕜 : 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
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source (↑(extChartAt I x).symm y)
this :
  mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm y) =
    mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x)) (extChartAt I x).source (↑(extChartAt I x).symm y)
⊢ ↑(extChartAt I x).symm ∘ ↑(extChartAt I x) =ᶠ[𝓝[(extChartAt I x).source] ↑(extChartAt I x).symm y] id

Tactic:
filter_upwards [extChartAt_source_mem_nhdsWithin' h'y] with z hz

Result:
case 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
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source (↑(extChartAt I x).symm y)
this :
  mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm y) =
    mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x)) (extChartAt I x).source (↑(extChartAt I x).symm y)
z : M
hz : z ∈ (extChartAt I x).source
⊢ (↑(extChartAt I x).symm ∘ ↑(extChartAt I x)) z = id z

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
x : M
y : E
hy : y ∈ (extChartAt I x).target
⊢ (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) y).comp
      (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm y)) =
    ContinuousLinearMap.id 𝕜 (TangentSpace I (↑(extChartAt I x).symm y))

Tactic:
have h'y : (extChartAt I x).symm y ∈ (extChartAt I x).source := (extChartAt I x).map_target hy

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
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
⊢ (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) y).comp
      (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm y)) =
    ContinuousLinearMap.id 𝕜 (TangentSpace I (↑(extChartAt I x).symm y))

Proof state:
case hxs
𝕜 : 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
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source (↑(extChartAt I x).symm y)
this :
  mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm y) =
    mfderivWithin I 𝓘(𝕜, E) (↑(extChartAt I x)) (extChartAt I x).source (↑(extChartAt I x).symm y)
⊢ UniqueMDiffWithinAt I (extChartAt I x).source (↑(extChartAt I x).symm y)

Tactic:
exact U'

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
inst✝ : IsManifold I 1 M
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
⊢ (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) y).comp
      (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm y)) =
    ContinuousLinearMap.id 𝕜 (TangentSpace I (↑(extChartAt I x).symm y))

Tactic:
have h''y : (extChartAt I x).symm y ∈ (chartAt H x).source := by
  rwa [← extChartAt_source (I := I)]

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
x : M
y : E
hy : y ∈ (extChartAt I x).target
h'y : ↑(extChartAt I x).symm y ∈ (extChartAt I x).source
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
⊢ (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) y).comp
      (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm y)) =
    ContinuousLinearMap.id 𝕜 (TangentSpace I (↑(extChartAt I x).symm y))