-- Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
theorem symm_comp_deriv {x : M} (hx : x ∈ e.source) :
    (mfderiv I' I e.symm (e x)).comp (mfderiv I I' e x) =
      ContinuousLinearMap.id 𝕜 (TangentSpace I x)

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
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'
e : PartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this : mfderiv I I (↑e.symm ∘ ↑e) x = (mfderiv I' I (↑e.symm) (↑e x)).comp (mfderiv I I' (↑e) x)
⊢ mfderiv I I (↑e.symm ∘ ↑e) x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)

Tactic:
have : mfderiv I I (_root_.id : M → M) x = ContinuousLinearMap.id _ _ := mfderiv_id

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
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'
e : PartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this✝ : mfderiv I I (↑e.symm ∘ ↑e) x = (mfderiv I' I (↑e.symm) (↑e x)).comp (mfderiv I I' (↑e) x)
this : mfderiv I I id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
⊢ mfderiv I I (↑e.symm ∘ ↑e) x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)

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
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'
e : PartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this✝ : mfderiv I I (↑e.symm ∘ ↑e) x = (mfderiv I' I (↑e.symm) (↑e x)).comp (mfderiv I I' (↑e) x)
this : mfderiv I I id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
⊢ mfderiv I I (↑e.symm ∘ ↑e) x = mfderiv I I id x

Tactic:
apply Filter.EventuallyEq.mfderiv_eq

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
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'
e : PartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this✝ : mfderiv I I (↑e.symm ∘ ↑e) x = (mfderiv I' I (↑e.symm) (↑e x)).comp (mfderiv I I' (↑e) x)
this : mfderiv I I id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
⊢ ↑e.symm ∘ ↑e =ᶠ[𝓝 x] id

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
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'
e : PartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this✝ : mfderiv I I (↑e.symm ∘ ↑e) x = (mfderiv I' I (↑e.symm) (↑e x)).comp (mfderiv I I' (↑e) x)
this : mfderiv I I id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
⊢ ↑e.symm ∘ ↑e =ᶠ[𝓝 x] id

Tactic:
have : e.source ∈ 𝓝 x := e.open_source.mem_nhds hx

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
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'
e : PartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this✝¹ : mfderiv I I (↑e.symm ∘ ↑e) x = (mfderiv I' I (↑e.symm) (↑e x)).comp (mfderiv I I' (↑e) x)
this✝ : mfderiv I I id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
this : e.source ∈ 𝓝 x
⊢ ↑e.symm ∘ ↑e =ᶠ[𝓝 x] 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
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'
e : PartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
⊢ (mfderiv I' I (↑e.symm) (↑e x)).comp (mfderiv I I' (↑e) x) = ContinuousLinearMap.id 𝕜 (TangentSpace I x)

Tactic:
have : mfderiv I I (e.symm ∘ e) x = (mfderiv I' I e.symm (e x)).comp (mfderiv I I' e x) :=
  mfderiv_comp x (he.mdifferentiableAt_symm (e.map_source hx)) (he.mdifferentiableAt hx)

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
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'
e : PartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this : mfderiv I I (↑e.symm ∘ ↑e) x = (mfderiv I' I (↑e.symm) (↑e x)).comp (mfderiv I I' (↑e) x)
⊢ (mfderiv I' I (↑e.symm) (↑e x)).comp (mfderiv I I' (↑e) x) = ContinuousLinearMap.id 𝕜 (TangentSpace I x)

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
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'
e : PartialHomeomorph M M'
he : MDifferentiable I I' e
x : M
hx : x ∈ e.source
this✝¹ : mfderiv I I (↑e.symm ∘ ↑e) x = (mfderiv I' I (↑e.symm) (↑e x)).comp (mfderiv I I' (↑e) x)
this✝ : mfderiv I I id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
this : e.source ∈ 𝓝 x
⊢ ↑e.symm ∘ ↑e =ᶠ[𝓝 x] id

Tactic:
exact Filter.mem_of_superset this (by mfld_set_tac)

Result:
no goals