-- 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
⊢ (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 U' : UniqueMDiffWithinAt I (extChartAt I x).source ((extChartAt I x).symm y) :=
  (isOpen_extChartAt_source x).uniqueMDiffWithinAt 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)
⊢ (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 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

Tactic:
simp only [Function.comp_def, PartialEquiv.left_inv (extChartAt I x) hz, id_eq]

Result:
no goals

Proof state:
case hf
𝕜 : 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)
⊢ MDifferentiableWithinAt I 𝓘(𝕜, E) (↑(extChartAt I x)) (extChartAt I x).source (↑(extChartAt I x).symm y)

Tactic:
exact (mdifferentiableAt_extChartAt h''y).mdifferentiableWithinAt

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
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source (↑(extChartAt I x).symm y)
⊢ 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)

Tactic:
rw [mfderivWithin_eq_mfderiv U']

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)
⊢ MDifferentiableAt I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm y)

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
⊢ ↑(extChartAt I x).symm y ∈ (chartAt H x).source

Tactic:
rwa [← extChartAt_source (I := I)]

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
h''y : ↑(extChartAt I x).symm y ∈ (chartAt H x).source
U' : UniqueMDiffWithinAt I (extChartAt I x).source (↑(extChartAt I x).symm y)
⊢ MDifferentiableAt I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm y)

Tactic:
exact mdifferentiableAt_extChartAt h''y

Result:
no goals