-- 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)
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 I I (↑(extChartAt I x).symm ∘ ↑(extChartAt I x)) (extChartAt I x).source (↑(extChartAt I x).symm y) =
    ContinuousLinearMap.id 𝕜 (TangentSpace I (↑(extChartAt I x).symm y))

Tactic:
rw [← mfderivWithin_id 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)
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 I I (↑(extChartAt I x).symm ∘ ↑(extChartAt I x)) (extChartAt I x).source (↑(extChartAt I x).symm y) =
    mfderivWithin I I id (extChartAt I x).source (↑(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
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 I I (↑(extChartAt I x).symm ∘ ↑(extChartAt I x)) (extChartAt I x).source (↑(extChartAt I x).symm y) =
    mfderivWithin I I id (extChartAt I x).source (↑(extChartAt I x).symm y)

Tactic:
apply Filter.EventuallyEq.mfderivWithin_eq U'

Result:
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

case hx
𝕜 : 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).symm y) = id (↑(extChartAt I x).symm y)

Proof state:
case hx
𝕜 : 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).symm y) = id (↑(extChartAt I x).symm y)

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

Result:
no goals

Proof state:
case h.a
𝕜 : 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) z ∈ (extChartAt I x).target

Tactic:
exact PartialEquiv.map_source (extChartAt I x) hz

Result:
no goals

Proof state:
case hy
𝕜 : 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) (↑(extChartAt I x).symm y) = y

Tactic:
exact PartialEquiv.right_inv (extChartAt I x) hy

Result:
no goals