awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x : M
y : M'
hs : s ⊆ (extChartAt I x).source
h2s : MapsTo f s (extChartAt I' y).source
hs₁ : s ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ MapsTo f s (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source

Tactic:
rw [extChartAt_source] at hs h2s

Premises used: extChartAt_source
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x : M
y : M'
hs : s ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
h2s : MapsTo f s (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
⊢ MDifferentiableOn I I' f s ↔
    DifferentiableOn 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x) : M → E) '' s)

Tactic:
mdifferentiableOn_iff_of_mem_maximalAtlas' (chart_mem_maximalAtlas x)
    (chart_mem_maximalAtlas y) hs h2s

Premises used: IsManifold.chart_mem_maximalAtlas, mdifferentiableOn_iff_of_mem_maximalAtlas'
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x : M
y : M'
hs : s ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
h2s : MapsTo f s (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
⊢ MDifferentiableOn I I' f s ↔
    DifferentiableOn 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x) : M → E) '' s)

Tactic:
exact mdifferentiableOn_iff_of_mem_maximalAtlas' (chart_mem_maximalAtlas x)
    (chart_mem_maximalAtlas y) hs h2s

Premises used: IsManifold.chart_mem_maximalAtlas, mdifferentiableOn_iff_of_mem_maximalAtlas'
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
mp :
  MDifferentiableOn I I' f s →
    ContinuousOn f s ∧
      ∀ (x : M) (y : M'),
        DifferentiableOn 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
          ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
mpr :
  (ContinuousOn f s ∧
      ∀ (x : M) (y : M'),
        DifferentiableOn 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
          ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))) →
    MDifferentiableOn I I' f s
⊢ MDifferentiableOn I I' f s ↔
    ContinuousOn f s ∧
      ∀ (x : M) (y : M'),
        DifferentiableOn 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
          ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))

Tactic:
constructor
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
h : MDifferentiableOn I I' f s
⊢ ContinuousOn f s ∧
    ∀ (x : M) (y : M'),
      DifferentiableOn 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))

Tactic:
⟨fun x hx => (h x hx).1, fun x y z hz => ?_⟩

Premises used: ChartedSpace.LiftPropWithinAt.continuousWithinAt, And.intro
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
h : MDifferentiableOn I I' f s
mp :
  ∀ (x : M) (y : M') (z : E)
    (hz : z ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)),
    DifferentiableWithinAt 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) z
⊢ ContinuousOn f s ∧
    ∀ (x : M) (y : M'),
      DifferentiableOn 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))

Tactic:
refine ⟨fun x hx => (h x hx).1, fun x y z hz => ?_⟩
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
h : MDifferentiableOn I I' f s
x : M
y : M'
z : E
hz : z ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)
⊢ (z ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source

Tactic:
simp only [mfld_simps] at hz
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
h : MDifferentiableOn I I' f s
x : M
y : M'
z : E
hz :
  (z ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
w : M := (↑(extChartAt I x).symm : E → M) z
⊢ w ∈ s

Tactic:
simp only [w, hz, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
h : MDifferentiableOn I I' f s
x : M
y : M'
z : E
hz :
  (z ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
w : M := (↑(extChartAt I x).symm : E → M) z
⊢ w ∈ s

Tactic:
have : w ∈ s := by simp only [w, hz, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
h : MDifferentiableOn I I' f s
x : M
y : M'
z : E
hz :
  (z ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
w : M := (↑(extChartAt I x).symm : E → M) z
this : w ∈ s
⊢ MDifferentiableWithinAt I I' f s w

Tactic:
specialize h w this
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x : M
y : M'
z : E
hz :
  (z ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
w : M := (↑(extChartAt I x).symm : E → M) z
this : w ∈ s
h : MDifferentiableWithinAt I I' f s w
⊢ w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source

Tactic:
simp only [w, hz, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x : M
y : M'
z : E
hz :
  (z ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
w : M := (↑(extChartAt I x).symm : E → M) z
this : w ∈ s
h : MDifferentiableWithinAt I I' f s w
⊢ w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source

Tactic:
have w1 : w ∈ (chartAt H x).source := by simp only [w, hz, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x : M
y : M'
z : E
hz :
  (z ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
w : M := (↑(extChartAt I x).symm : E → M) z
this : w ∈ s
h : MDifferentiableWithinAt I I' f s w
w1 : w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ f w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source

Tactic:
simp only [w, hz, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x : M
y : M'
z : E
hz :
  (z ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
w : M := (↑(extChartAt I x).symm : E → M) z
this : w ∈ s
h : MDifferentiableWithinAt I I' f s w
w1 : w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ f w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source

Tactic:
have w2 : f w ∈ (chartAt H' y).source := by simp only [w, hz, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x : M
y : M'
z : E
hz :
  (z ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
w : M := (↑(extChartAt I x).symm : E → M) z
this : w ∈ s
h : MDifferentiableWithinAt I I' f s w
w1 : w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
w2 : f w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
⊢ DifferentiableWithinAt 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
    ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
    ((↑(extChartAt I x) : M → E) w)

Tactic:
((mdifferentiableWithinAt_iff_of_mem_source w1 w2).mp h).2.mono _

Premises used: DifferentiableWithinAt.mono, And.right, Iff.mp, mdifferentiableWithinAt_iff_of_mem_source
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x : M
y : M'
z : E
hz :
  (z ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
w : M := (↑(extChartAt I x).symm : E → M) z
this : w ∈ s
h : MDifferentiableWithinAt I I' f s w
w1 : w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
w2 : f w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
h₁ : z = (↑(extChartAt I x) : M → E) w
mp :
  (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source) ⊆
    (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
⊢ DifferentiableWithinAt 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
    ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) z

Tactic:
convert! ((mdifferentiableWithinAt_iff_of_mem_source w1 w2).mp h).2.mono _

Premises used: DifferentiableWithinAt.mono, And.right, Iff.mp, mdifferentiableWithinAt_iff_of_mem_source
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x : M
y : M'
z : E
hz :
  (z ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
w : M := (↑(extChartAt I x).symm : E → M) z
this : w ∈ s
h : MDifferentiableWithinAt I I' f s w
w1 : w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
w2 : f w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
⊢ z = (↑(extChartAt I x) : M → E) w

Tactic:
simp only [w, hz, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x : M
y : M'
z : E
hz :
  (z ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
w : M := (↑(extChartAt I x).symm : E → M) z
this : w ∈ s
h : MDifferentiableWithinAt I I' f s w
w1 : w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
w2 : f w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
mp mp₁ mp₂ :
  ∀ ⦃my_y : E⦄,
    my_y ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source) →
      my_y ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
mp₃ mp₄ :
  ∀ ⦃my_y : E⦄,
    (my_y ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) my_y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
        (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) my_y) ∈ s ∧
          f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) my_y)) ∈
            (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source →
      my_y ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
⊢ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source) ⊆
    (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)

Tactic:
mfld_set_tac
-- Module: Mathlib.Geometry.Manifold.MFDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H : Type u_3
inst_3 : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H M
E' : Type u_5
inst_6 : NormedAddCommGroup E'
inst_7 : NormedSpace 𝕜 E'
H' : Type u_6
inst_8 : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst_9 : TopologicalSpace M'
inst_10 : ChartedSpace H' M'
f : M → M'
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
hcont : ContinuousOn f s
hdiff :
  ∀ (x : M) (y : M'),
    DifferentiableOn 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
x : M
hx : x ∈ s
⊢ MDifferentiableWithinAt I I' f s x

Tactic:
differentiableWithinAt_localInvariantProp.liftPropWithinAt_iff.mpr ?_

Premises used: Iff.mpr, differentiableWithinAt_localInvariantProp, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_iff, MDifferentiableWithinAt