-- Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
theorem mdifferentiableAt_atlas (h : e ∈ atlas H M) {x : M} (hx : x ∈ e.source) :
    MDifferentiableAt I I e 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
inst✝ : IsManifold I 1 M
e : PartialHomeomorph M H
h : e ∈ atlas H M
x : M
hx : x ∈ e.source
mem : ↑I (↑(chartAt H x) x) ∈ ↑I.symm ⁻¹' ((chartAt H x).symm ≫ₕ e).source ∩ range ↑I
this : (chartAt H x).symm ≫ₕ e ∈ contDiffGroupoid 1 I
A : ContDiffOn 𝕜 1 (↑I ∘ ↑((chartAt H x).symm ≫ₕ e) ∘ ↑I.symm) (↑I.symm ⁻¹' ((chartAt H x).symm ≫ₕ e).source ∩ range ↑I)
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e) (range ↑I) (↑(extChartAt I x) x)

Tactic:
have B := A.differentiableOn le_rfl (I ((chartAt H x : M → H) x)) mem

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
e : PartialHomeomorph M H
h : e ∈ atlas H M
x : M
hx : x ∈ e.source
mem : ↑I (↑(chartAt H x) x) ∈ ↑I.symm ⁻¹' ((chartAt H x).symm ≫ₕ e).source ∩ range ↑I
this : (chartAt H x).symm ≫ₕ e ∈ contDiffGroupoid 1 I
A : ContDiffOn 𝕜 1 (↑I ∘ ↑((chartAt H x).symm ≫ₕ e) ∘ ↑I.symm) (↑I.symm ⁻¹' ((chartAt H x).symm ≫ₕ e).source ∩ range ↑I)
B :
  DifferentiableWithinAt 𝕜 (↑I ∘ ↑((chartAt H x).symm ≫ₕ e) ∘ ↑I.symm)
    (↑I.symm ⁻¹' ((chartAt H x).symm ≫ₕ e).source ∩ range ↑I) (↑I (↑(chartAt H x) x))
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e) (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
inst✝ : IsManifold I 1 M
e : PartialHomeomorph M H
h : e ∈ atlas H M
x : M
hx : x ∈ e.source
mem : ↑I (↑(chartAt H x) x) ∈ ↑I.symm ⁻¹' ((chartAt H x).symm ≫ₕ e).source ∩ range ↑I
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e) (range ↑I) (↑(extChartAt I x) x)

Tactic:
have : (chartAt H x).symm.trans e ∈ contDiffGroupoid 1 I :=
  HasGroupoid.compatible (chart_mem_atlas H x) h

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
e : PartialHomeomorph M H
h : e ∈ atlas H M
x : M
hx : x ∈ e.source
mem : ↑I (↑(chartAt H x) x) ∈ ↑I.symm ⁻¹' ((chartAt H x).symm ≫ₕ e).source ∩ range ↑I
this : (chartAt H x).symm ≫ₕ e ∈ contDiffGroupoid 1 I
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e) (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
inst✝ : IsManifold I 1 M
e : PartialHomeomorph M H
h : e ∈ atlas H M
x : M
hx : x ∈ e.source
⊢ MDifferentiableAt I I (↑e) x

Tactic:
rw [mdifferentiableAt_iff]

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
e : PartialHomeomorph M H
h : e ∈ atlas H M
x : M
hx : x ∈ e.source
⊢ ContinuousAt (↑e) x ∧ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e) (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
inst✝ : IsManifold I 1 M
e : PartialHomeomorph M H
h : e ∈ atlas H M
x : M
hx : x ∈ e.source
mem : ↑I (↑(chartAt H x) x) ∈ ↑I.symm ⁻¹' ((chartAt H x).symm ≫ₕ e).source ∩ range ↑I
this : (chartAt H x).symm ≫ₕ e ∈ contDiffGroupoid 1 I
A : ContDiffOn 𝕜 1 (↑I ∘ ↑((chartAt H x).symm ≫ₕ e) ∘ ↑I.symm) (↑I.symm ⁻¹' ((chartAt H x).symm ≫ₕ e).source ∩ range ↑I)
B :
  DifferentiableWithinAt 𝕜 (↑I ∘ (↑e ∘ ↑(chartAt H x).symm) ∘ ↑I.symm)
    (↑I.symm ⁻¹' (chartAt H x).target ∩ ↑I.symm ⁻¹' (↑(chartAt H x).symm ⁻¹' e.source) ∩ range ↑I)
    (↑I (↑(chartAt H x) x))
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e) (range ↑I) (↑(extChartAt I x) x)

Tactic:
rw [inter_comm, differentiableWithinAt_inter] at B

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
e : PartialHomeomorph M H
h : e ∈ atlas H M
x : M
hx : x ∈ e.source
mem : ↑I (↑(chartAt H x) x) ∈ ↑I.symm ⁻¹' ((chartAt H x).symm ≫ₕ e).source ∩ range ↑I
this : (chartAt H x).symm ≫ₕ e ∈ contDiffGroupoid 1 I
A : ContDiffOn 𝕜 1 (↑I ∘ ↑((chartAt H x).symm ≫ₕ e) ∘ ↑I.symm) (↑I.symm ⁻¹' ((chartAt H x).symm ≫ₕ e).source ∩ range ↑I)
B : DifferentiableWithinAt 𝕜 (↑I ∘ (↑e ∘ ↑(chartAt H x).symm) ∘ ↑I.symm) (range ↑I) (↑I (↑(chartAt H x) x))
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e) (range ↑I) (↑(extChartAt I x) x)

𝕜 : 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
e : PartialHomeomorph M H
h : e ∈ atlas H M
x : M
hx : x ∈ e.source
mem : ↑I (↑(chartAt H x) x) ∈ ↑I.symm ⁻¹' ((chartAt H x).symm ≫ₕ e).source ∩ range ↑I
this : (chartAt H x).symm ≫ₕ e ∈ contDiffGroupoid 1 I
A : ContDiffOn 𝕜 1 (↑I ∘ ↑((chartAt H x).symm ≫ₕ e) ∘ ↑I.symm) (↑I.symm ⁻¹' ((chartAt H x).symm ≫ₕ e).source ∩ range ↑I)
B :
  DifferentiableWithinAt 𝕜 (↑I ∘ (↑e ∘ ↑(chartAt H x).symm) ∘ ↑I.symm)
    (range ↑I ∩ (↑I.symm ⁻¹' (chartAt H x).target ∩ ↑I.symm ⁻¹' (↑(chartAt H x).symm ⁻¹' e.source)))
    (↑I (↑(chartAt H x) x))
⊢ ↑I.symm ⁻¹' (chartAt H x).target ∩ ↑I.symm ⁻¹' (↑(chartAt H x).symm ⁻¹' e.source) ∈ 𝓝 (↑I (↑(chartAt H x) x))