-- Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean
theorem UniqueMDiffOn.uniqueDiffOn_inter_preimage (hs : UniqueMDiffOn I s) (x : M) (y : M'')
    {f : M → M''} (hf : ContinuousOn f s) :
    UniqueDiffOn 𝕜
      ((extChartAt I x).target ∩ (extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) :=
  haveI : UniqueMDiffOn I (s ∩ f ⁻¹' (extChartAt I' y).source)

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
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M'' : Type u_8
inst✝² : TopologicalSpace M''
inst✝¹ : ChartedSpace H' M''
s : Set M
inst✝ : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
y : M''
f : M → M''
hf : ContinuousOn f s
z : M
hz : z ∈ s ∩ f ⁻¹' (extChartAt I' y).source
⊢ UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' y).source) z

Tactic:
apply (hs z hz.1).inter'

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
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M'' : Type u_8
inst✝² : TopologicalSpace M''
inst✝¹ : ChartedSpace H' M''
s : Set M
inst✝ : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
y : M''
f : M → M''
hf : ContinuousOn f s
z : M
hz : z ∈ s ∩ f ⁻¹' (extChartAt I' y).source
⊢ f ⁻¹' (extChartAt I' y).source ∈ nhdsWithin z s

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
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M'' : Type u_8
inst✝² : TopologicalSpace M''
inst✝¹ : ChartedSpace H' M''
s : Set M
inst✝ : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
y : M''
f : M → M''
hf : ContinuousOn f s
⊢ UniqueMDiffOn I (s ∩ f ⁻¹' (extChartAt I' y).source)

Tactic:
intro z hz

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
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M'' : Type u_8
inst✝² : TopologicalSpace M''
inst✝¹ : ChartedSpace H' M''
s : Set M
inst✝ : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
y : M''
f : M → M''
hf : ContinuousOn f s
z : M
hz : z ∈ s ∩ f ⁻¹' (extChartAt I' y).source
⊢ UniqueMDiffWithinAt I (s ∩ f ⁻¹' (extChartAt I' y).source) 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
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M'' : Type u_8
inst✝² : TopologicalSpace M''
inst✝¹ : ChartedSpace H' M''
s : Set M
inst✝ : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
y : M''
f : M → M''
hf : ContinuousOn f s
z : M
hz : z ∈ s ∩ f ⁻¹' (extChartAt I' y).source
⊢ (extChartAt I' y).source ∈ nhds (f z)

Tactic:
exact (isOpen_extChartAt_source y).mem_nhds hz.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
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M'' : Type u_8
inst✝² : TopologicalSpace M''
inst✝¹ : ChartedSpace H' M''
s : Set M
inst✝ : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
y : M''
f : M → M''
hf : ContinuousOn f s
z : M
hz : z ∈ s ∩ f ⁻¹' (extChartAt I' y).source
⊢ f ⁻¹' (extChartAt I' y).source ∈ nhdsWithin z s

Tactic:
apply (hf z hz.1).preimage_mem_nhdsWithin

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
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M'' : Type u_8
inst✝² : TopologicalSpace M''
inst✝¹ : ChartedSpace H' M''
s : Set M
inst✝ : IsManifold I 1 M
hs : UniqueMDiffOn I s
x : M
y : M''
f : M → M''
hf : ContinuousOn f s
z : M
hz : z ∈ s ∩ f ⁻¹' (extChartAt I' y).source
⊢ (extChartAt I' y).source ∈ nhds (f z)