-- Mathlib/Geometry/Manifold/MFDeriv/Atlas.lean
theorem mdifferentiableWithinAt_extChartAt_symm (h : z ∈ (extChartAt I x).target) :
    MDifferentiableWithinAt 𝓘(𝕜, E) I (extChartAt I x).symm (range I) z

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
x : M
z : E
Z : MDifferentiableWithinAt 𝓘(𝕜, E) I (↑I.symm) (range ↑I) z
h : (∃ y, ↑I y = z) ∧ ↑I.symm z ∈ (chartAt H x).target
⊢ ↑I.symm z ∈ (ChartedSpace.chartAt x).target

Tactic:
exact h.2

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
x : M
z : E
h : z ∈ (extChartAt I x).target
Z : MDifferentiableWithinAt 𝓘(𝕜, E) I (↑I.symm) (range ↑I) z
⊢ ↑I.symm z ∈ (ChartedSpace.chartAt x).target

Tactic:
simp only [extChartAt, PartialHomeomorph.extend, PartialEquiv.trans_target,
  ModelWithCorners.target_eq, ModelWithCorners.toPartialEquiv_coe_symm, mem_inter_iff, mem_range,
  mem_preimage] at 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
x : M
z : E
Z : MDifferentiableWithinAt 𝓘(𝕜, E) I (↑I.symm) (range ↑I) z
h : (∃ y, ↑I y = z) ∧ ↑I.symm z ∈ (chartAt H x).target
⊢ ↑I.symm z ∈ (ChartedSpace.chartAt x).target

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
x : M
z : E
h : z ∈ (extChartAt I x).target
⊢ MDifferentiableWithinAt 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) z

Tactic:
have Z := I.mdifferentiableWithinAt_symm (extChartAt_target_subset_range 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
x : M
z : E
h : z ∈ (extChartAt I x).target
Z : MDifferentiableWithinAt 𝓘(𝕜, E) I (↑I.symm) (range ↑I) z
⊢ MDifferentiableWithinAt 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) z

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
x : M
z : E
h : z ∈ (extChartAt I x).target
Z : MDifferentiableWithinAt 𝓘(𝕜, E) I (↑I.symm) (range ↑I) z
⊢ MDifferentiableWithinAt 𝓘(𝕜, E) I (↑(extChartAt I x).symm) (range ↑I) z

Tactic:
apply MDifferentiableAt.comp_mdifferentiableWithinAt (I' := I) _ _ Z

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
x : M
z : E
h : z ∈ (extChartAt I x).target
Z : MDifferentiableWithinAt 𝓘(𝕜, E) I (↑I.symm) (range ↑I) z
⊢ MDifferentiableAt I I (chartAt H x).toPartialEquiv.2 (↑I.symm z)

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
x : M
z : E
h : z ∈ (extChartAt I x).target
Z : MDifferentiableWithinAt 𝓘(𝕜, E) I (↑I.symm) (range ↑I) z
⊢ MDifferentiableAt I I (chartAt H x).toPartialEquiv.2 (↑I.symm z)

Tactic:
apply mdifferentiableAt_atlas_symm (ChartedSpace.chart_mem_atlas 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
inst✝ : IsManifold I 1 M
x : M
z : E
h : z ∈ (extChartAt I x).target
Z : MDifferentiableWithinAt 𝓘(𝕜, E) I (↑I.symm) (range ↑I) z
⊢ ↑I.symm z ∈ (ChartedSpace.chartAt x).target