-- 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
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)

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 : 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)

𝕜 : 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.symm ⁻¹' e.target ∩ ↑I.symm ⁻¹' (↑e.symm ⁻¹' (chartAt H (↑e.symm x)).source))) (↑I x)
⊢ ↑I.symm ⁻¹' e.target ∩ ↑I.symm ⁻¹' (↑e.symm ⁻¹' (chartAt H (↑e.symm x)).source) ∈ 𝓝 (↑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
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)

Tactic:
have A :
  ContDiffOn 𝕜 1 (I ∘ e.symm.trans (chartAt H (e.symm x)) ∘ I.symm)
    (I.symm ⁻¹' (e.symm.trans (chartAt H (e.symm x))).source ∩ range I) :=
  this.1

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)
⊢ 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
⊢ DifferentiableWithinAt 𝕜 (writtenInExtChartAt I I x ↑e.symm) (range ↑I) (↑(extChartAt I x) x)

Tactic:
have mem : I x ∈ I.symm ⁻¹' (e.symm ≫ₕ chartAt H (e.symm x)).source ∩ range I := by
  simp only [hx, mfld_simps]

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
⊢ 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
⊢ ↑I x ∈ ↑I.symm ⁻¹' (e.symm ≫ₕ chartAt H (↑e.symm x)).source ∩ range ↑I

Tactic:
simp only [hx, 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
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.symm ⁻¹' e.target ∩ ↑I.symm ⁻¹' (↑e.symm ⁻¹' (chartAt H (↑e.symm x)).source))) (↑I x)
⊢ ↑I.symm ⁻¹' e.target ∩ ↑I.symm ⁻¹' (↑e.symm ⁻¹' (chartAt H (↑e.symm x)).source) ∈ 𝓝 (↑I x)

Tactic:
apply IsOpen.mem_nhds ((PartialHomeomorph.open_source _).preimage I.continuous_symm) mem.1

Result:
no goals