-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem hasMFDerivAt_id (x : M) :
    HasMFDerivAt I I (@id M) 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
x : M
⊢ ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, (↑(extChartAt I x) ∘ ↑(extChartAt I x).symm) y = y

Tactic:
apply Filter.mem_of_superset (extChartAt_target_mem_nhdsWithin x)

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
x : M
⊢ (extChartAt I x).target ⊆ {x_1 | (fun y => (↑(extChartAt I x) ∘ ↑(extChartAt I x).symm) y = y) x_1}

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
x : M
⊢ (extChartAt I x).target ⊆ {x_1 | (fun y => (↑(extChartAt I x) ∘ ↑(extChartAt I x).symm) y = y) x_1}

Tactic:
mfld_set_tac

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
x : M
this : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, (↑(extChartAt I x) ∘ ↑(extChartAt I x).symm) y = y
⊢ (↑(extChartAt I x) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x) = id (↑(extChartAt I x) x)

Tactic:
simp only [mfld_simps]

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
x : M
this : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, (↑(extChartAt I x) ∘ ↑(extChartAt I x).symm) y = y
⊢ HasFDerivWithinAt (writtenInExtChartAt I I x id) (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) (range ↑I)
    (↑(extChartAt I x) x)

Tactic:
apply HasFDerivWithinAt.congr_of_eventuallyEq (hasFDerivWithinAt_id _ _) this

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
x : M
this : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, (↑(extChartAt I x) ∘ ↑(extChartAt I x).symm) y = y
⊢ (↑(extChartAt I x) ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x) x) = id (↑(extChartAt I x) 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
x : M
⊢ HasMFDerivAt I I id x (ContinuousLinearMap.id 𝕜 (TangentSpace I x))

Tactic:
refine ⟨continuousAt_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
x : M
⊢ HasFDerivWithinAt (writtenInExtChartAt I I x id) (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) (range ↑I)
    (↑(extChartAt I x) 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
x : M
⊢ HasFDerivWithinAt (writtenInExtChartAt I I x id) (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) (range ↑I)
    (↑(extChartAt I x) x)

Tactic:
have : ∀ᶠ y in 𝓝[range I] (extChartAt I x) x, (extChartAt I x ∘ (extChartAt I x).symm) y = y := by
  apply Filter.mem_of_superset (extChartAt_target_mem_nhdsWithin x)
  mfld_set_tac

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
x : M
this : ∀ᶠ (y : E) in 𝓝[range ↑I] ↑(extChartAt I x) x, (↑(extChartAt I x) ∘ ↑(extChartAt I x).symm) y = y
⊢ HasFDerivWithinAt (writtenInExtChartAt I I x id) (ContinuousLinearMap.id 𝕜 (TangentSpace I x)) (range ↑I)
    (↑(extChartAt I x) x)