-- Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
/-- The composition of the derivative of `extChartAt` with the derivative of the inverse of
`extChartAt` gives the identity.
Version where the basepoint belongs to `(extChartAt I x).target`. -/
lemma mfderiv_extChartAt_comp_mfderivWithin_extChartAt_symm {x : M}
    {y : E} (hy : y ∈ (extChartAt I x).target) :
    (mfderiv I 𝓘(𝕜, E) (extChartAt I x) ((extChartAt I x).symm y)) ∘L
      (mfderivWithin 𝓘(𝕜, E) I (extChartAt I x).symm (range I) 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
U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range ↑I) y
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
⊢ UniqueMDiffWithinAt 𝓘(𝕜, E) (range ↑I) y

Tactic:
apply I.uniqueMDiffOn

Result:
case 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
⊢ y ∈ range ↑I

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

Tactic:
have U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range ↑I) y := by
  apply I.uniqueMDiffOn
  exact extChartAt_target_subset_range x 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
U : UniqueMDiffWithinAt 𝓘(𝕜, E) (range ↑I) y
⊢ (mfderiv I 𝓘(𝕜, E) (↑(extChartAt I x)) (↑(extChartAt I x).symm y)).comp
      (mfderivWithin 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) y) =
    ContinuousLinearMap.id 𝕜 (TangentSpace 𝓘(𝕜, E) y)