-- Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
theorem mdifferentiableAt_atlas_symm (h : e ∈ atlas H M) {x : H} (hx : x ∈ e.target) :
    MDifferentiableAt I I e.symm 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 : H
hx : x ∈ e.target
⊢ ContinuousAt (↑e.symm) x ∧
    DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e.symm) (range ↑I) (↑(extChartAt I x) x)

Tactic:
refine ⟨(e.continuousOn_symm x hx).continuousAt (e.open_target.mem_nhds 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
inst✝ : IsManifold I 1 M
e : PartialHomeomorph M H
h : e ∈ atlas H M
x : H
hx : x ∈ e.target
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e.symm) (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 : H
hx : x ∈ e.target
mem : ↑I x ∈ ↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e.symm) (range ↑I) (↑(extChartAt I x) x)

Tactic:
have : e.symm.trans (chartAt H (e.symm x)) ∈ contDiffGroupoid 1 I :=
  HasGroupoid.compatible h (chart_mem_atlas 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 : H
hx : x ∈ e.target
mem : ↑I x ∈ ↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I
this : e.symm ≫ₕ chartAt H (↑e.symm x) ∈ contDiffGroupoid 1 I
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e.symm) (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 : H
hx : x ∈ e.target
mem : ↑I x ∈ ↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I
this : e.symm ≫ₕ chartAt H (↑e.symm x) ∈ contDiffGroupoid 1 I
A :
  ContDiffOn 𝕜 1 (↑I ∘ ↑(e.symm ≫ₕ chartAt H (↑e.symm x)) ∘ ↑I.symm)
    (↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I)
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e.symm) (range ↑I) (↑(extChartAt I x) x)

Tactic:
have B := A.differentiableOn le_rfl (I 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 : H
hx : x ∈ e.target
mem : ↑I x ∈ ↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I
this : e.symm ≫ₕ chartAt H (↑e.symm x) ∈ contDiffGroupoid 1 I
A :
  ContDiffOn 𝕜 1 (↑I ∘ ↑(e.symm ≫ₕ chartAt H (↑e.symm x)) ∘ ↑I.symm)
    (↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I)
B :
  DifferentiableWithinAt 𝕜 (↑I ∘ ↑(e.symm ≫ₕ chartAt H (↑e.symm x)) ∘ ↑I.symm)
    (↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I) (↑I x)
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e.symm) (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 : H
hx : x ∈ e.target
⊢ MDifferentiableAt I I (↑e.symm) 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 : H
hx : x ∈ e.target
⊢ ContinuousAt (↑e.symm) x ∧
    DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e.symm) (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 : H
hx : x ∈ e.target
mem : ↑I x ∈ ↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I
this : e.symm ≫ₕ chartAt H (↑e.symm x) ∈ contDiffGroupoid 1 I
A :
  ContDiffOn 𝕜 1 (↑I ∘ ↑(e.symm ≫ₕ chartAt H (↑e.symm x)) ∘ ↑I.symm)
    (↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I)
B :
  DifferentiableWithinAt 𝕜 (↑I ∘ ↑(e.symm ≫ₕ chartAt H (↑e.symm x)) ∘ ↑I.symm)
    (↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I) (↑I x)
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e.symm) (range ↑I) (↑(extChartAt I x) x)

Tactic:
simp only [mfld_simps] 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 : H
hx : x ∈ e.target
mem : ↑I x ∈ ↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I
this : e.symm ≫ₕ chartAt H (↑e.symm x) ∈ contDiffGroupoid 1 I
A :
  ContDiffOn 𝕜 1 (↑I ∘ ↑(e.symm ≫ₕ chartAt H (↑e.symm x)) ∘ ↑I.symm)
    (↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I)
B :
  DifferentiableWithinAt 𝕜 (↑I ∘ (↑(chartAt H (↑e.symm x)) ∘ ↑e.symm) ∘ ↑I.symm)
    (↑I.symm ⁻¹' e.target ∩ ↑I.symm ⁻¹' (↑e.symm ⁻¹' (chartAt H (↑e.symm x)).source) ∩ range ↑I) (↑I x)
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e.symm) (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 : H
hx : x ∈ e.target
mem : ↑I x ∈ ↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I
this : e.symm ≫ₕ chartAt H (↑e.symm x) ∈ contDiffGroupoid 1 I
A :
  ContDiffOn 𝕜 1 (↑I ∘ ↑(e.symm ≫ₕ chartAt H (↑e.symm x)) ∘ ↑I.symm)
    (↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I)
B : DifferentiableWithinAt 𝕜 (↑I ∘ (↑(chartAt H (↑e.symm x)) ∘ ↑e.symm) ∘ ↑I.symm) (range ↑I) (↑I x)
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e.symm) (range ↑I) (↑(extChartAt I x) x)

Tactic:
simpa only [mfld_simps]

Result:
no goals