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'
x : M
inst_11 : IsManifold I 1 M
x' : M
hx' : x' ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
simp_rw :
  MDifferentiableWithinAt I I' f univ x' ↔
    MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x')
simp_rw₁ :
  MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' univ ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x') ↔
    MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x')
simp_rw₂ :
  MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (↑(extChartAt I x).symm : E → M)) (univ ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x') ↔
    MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x')
⊢ MDifferentiableAt I I' f x' ↔
    MDifferentiableWithinAt 𝓘(𝕜, E) I' (f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x')

Tactic:
simp_rw [← mdifferentiableWithinAt_univ, mdifferentiableWithinAt_iff_source_of_mem_source hx',
    preimage_univ, univ_inter]

Premises used: mdifferentiableWithinAt_univ, Set.univ_inter, Set.preimage_univ, mdifferentiableWithinAt_iff_source_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'
x : M
y : M'
hy : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
rw :
  ContinuousWithinAt f s x →
    (LiftPropWithinAt (DifferentiableWithinAtProp I I') ((↑(chartAt H' y) : M' → H') ∘ f) s x ↔
      LiftPropWithinAt (DifferentiableWithinAtProp I 𝓘(𝕜, E')) ((↑(extChartAt I' y) : M' → E') ∘ f) s x)
⊢ LiftPropWithinAt (DifferentiableWithinAtProp I I') f s x ↔
    ContinuousWithinAt f s x ∧
      LiftPropWithinAt (DifferentiableWithinAtProp I 𝓘(𝕜, E')) ((↑(extChartAt I' y) : M' → E') ∘ f) s x

Tactic:
rw [differentiableWithinAt_localInvariantProp.liftPropWithinAt_indep_chart_target
      (chart_mem_maximalAtlas y) hy,
    and_congr_right]

Premises used: IsManifold.chart_mem_maximalAtlas, and_congr_right, differentiableWithinAt_localInvariantProp, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target
-- 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'
x : M
y : M'
hy : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
hf : ContinuousWithinAt f s x
simp_rw :
  ContinuousWithinAt ((↑(chartAt H' y) : M' → H') ∘ f) s x ∧
      DifferentiableWithinAtProp I I'
        (((↑(chartAt H' y) : M' → H') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    ContinuousWithinAt ((↑(extChartAt I' y) : M' → E') ∘ f) s x ∧
      DifferentiableWithinAtProp I 𝓘(𝕜, E')
        (((↑(extChartAt I' y) : M' → E') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)
⊢ LiftPropWithinAt (DifferentiableWithinAtProp I I') ((↑(chartAt H' y) : M' → H') ∘ f) s x ↔
    LiftPropWithinAt (DifferentiableWithinAtProp I 𝓘(𝕜, E')) ((↑(extChartAt I' y) : M' → E') ∘ f) s x

Tactic:
simp_rw [StructureGroupoid.liftPropWithinAt_self_target]

Premises used: StructureGroupoid.liftPropWithinAt_self_target
-- 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'
x : M
y : M'
hy : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
hf : ContinuousWithinAt f s x
simp_rw :
  True ∧
      DifferentiableWithinAtProp I I'
        (((↑(chartAt H' y) : M' → H') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    ContinuousWithinAt ((↑(extChartAt I' y) : M' → E') ∘ f) s x ∧
      DifferentiableWithinAtProp I 𝓘(𝕜, E')
        (((↑(extChartAt I' y) : M' → E') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)
⊢ ContinuousWithinAt ((↑(chartAt H' y) : M' → H') ∘ f) s x ∧
      DifferentiableWithinAtProp I I'
        (((↑(chartAt H' y) : M' → H') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    ContinuousWithinAt ((↑(extChartAt I' y) : M' → E') ∘ f) s x ∧
      DifferentiableWithinAtProp I 𝓘(𝕜, E')
        (((↑(extChartAt I' y) : M' → E') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)

Tactic:
simp_rw [((chartAt H' y).continuousAt hy).comp_continuousWithinAt hf]

Premises used: OpenPartialHomeomorph.continuousAt, chartAt, ContinuousAt.comp_continuousWithinAt
-- 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'
x : M
y : M'
hy : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
hf : ContinuousWithinAt f s x
⊢ f x ∈ (extChartAt I' y).source

Tactic:
rw [← extChartAt_source I'] at hy

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'
x : M
y : M'
hy : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
hf : ContinuousWithinAt f s x
hy₁ : f x ∈ (extChartAt I' y).source
⊢ ContinuousWithinAt f s x

Tactic:
rw [← extChartAt_source I'] at hy

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'
x : M
y : M'
hy : f x ∈ (extChartAt I' y).source
hf : ContinuousWithinAt f s x
simp_rw :
  True ∧
      DifferentiableWithinAtProp I I'
        (((↑(chartAt H' y) : M' → H') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    True ∧
      DifferentiableWithinAtProp I 𝓘(𝕜, E')
        (((↑(extChartAt I' y) : M' → E') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)
⊢ True ∧
      DifferentiableWithinAtProp I I'
        (((↑(chartAt H' y) : M' → H') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    ContinuousWithinAt ((↑(extChartAt I' y) : M' → E') ∘ f) s x ∧
      DifferentiableWithinAtProp I 𝓘(𝕜, E')
        (((↑(extChartAt I' y) : M' → E') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)

Tactic:
simp_rw [(continuousAt_extChartAt' hy).comp_continuousWithinAt hf]

Premises used: continuousAt_extChartAt', ContinuousAt.comp_continuousWithinAt
-- 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'
x : M
y : M'
hy : f x ∈ (extChartAt I' y).source
hf : ContinuousWithinAt f s x
⊢ True ∧
      DifferentiableWithinAtProp I I'
        (((↑(chartAt H' y) : M' → H') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x) ↔
    True ∧
      DifferentiableWithinAtProp I 𝓘(𝕜, E')
        (((↑(extChartAt I' y) : M' → E') ∘ f) ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
        ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s) ((↑(chartAt H x) : M → H) x)

Tactic:
rfl
-- 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'
inst_11 : IsManifold I' 1 M'
x : M
y : M'
hy : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
rw :
  MDifferentiableWithinAt I I' f univ x ↔
    ContinuousAt f x ∧ MDifferentiableAt I 𝓘(𝕜, E') ((↑(extChartAt I' y) : M' → E') ∘ f) x
rw₁ :
  ContinuousWithinAt f univ x ∧ MDifferentiableWithinAt I 𝓘(𝕜, E') ((↑(extChartAt I' y) : M' → E') ∘ f) univ x ↔
    ContinuousAt f x ∧ MDifferentiableAt I 𝓘(𝕜, E') ((↑(extChartAt I' y) : M' → E') ∘ f) x
rw₂ :
  ContinuousAt f x ∧ MDifferentiableWithinAt I 𝓘(𝕜, E') ((↑(extChartAt I' y) : M' → E') ∘ f) univ x ↔
    ContinuousAt f x ∧ MDifferentiableAt I 𝓘(𝕜, E') ((↑(extChartAt I' y) : M' → E') ∘ f) x
rw₃ rw₄ :
  ContinuousAt f x ∧ MDifferentiableWithinAt I 𝓘(𝕜, E') ((↑(extChartAt I' y) : M' → E') ∘ f) univ x ↔
    ContinuousAt f x ∧ MDifferentiableWithinAt I 𝓘(𝕜, E') ((↑(extChartAt I' y) : M' → E') ∘ f) univ x
⊢ MDifferentiableAt I I' f x ↔ ContinuousAt f x ∧ MDifferentiableAt I 𝓘(𝕜, E') ((↑(extChartAt I' y) : M' → E') ∘ f) x

Tactic:
rw [← mdifferentiableWithinAt_univ, mdifferentiableWithinAt_iff_target_of_mem_source hy,
    continuousWithinAt_univ, ← mdifferentiableWithinAt_univ]

Premises used: mdifferentiableWithinAt_univ, continuousWithinAt_univ, mdifferentiableWithinAt_iff_target_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
e : OpenPartialHomeomorph M H
e' : OpenPartialHomeomorph M' H'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x : M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I 1 M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas I' 1 M') e'
hx : x ∈ e.source
hy : f x ∈ e'.source
⊢ MDifferentiableWithinAt I I' f s x ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 ((↑(e'.extend I') : M' → E') ∘ f ∘ (↑(e.extend I).symm : E → M))
        ((↑(e.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(e.extend I) : M → E) x)

Tactic:
differentiableWithinAt_localInvariantProp.liftPropWithinAt_indep_chart he hx he' hy

Premises used: Set.Mem, setOf, PartialEquiv.trans, OpenPartialHomeomorph.toFun', ModelWithCorners.toFun', Set.preimage, differentiableWithinAt_localInvariantProp, DifferentiableWithinAtProp, PartialEquiv.trans', MDifferentiableWithinAt, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart, OpenPartialHomeomorph.extend
-- 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
e : OpenPartialHomeomorph M H
e' : OpenPartialHomeomorph M' H'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x : M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I 1 M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas I' 1 M') e'
hs : s ⊆ e.source
hx : x ∈ e.source
hy : f x ∈ e'.source
rw :
  ContinuousWithinAt f s x →
    (DifferentiableWithinAt 𝕜 ((↑(e'.extend I') : M' → E') ∘ f ∘ (↑(e.extend I).symm : E → M))
        ((↑(e.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(e.extend I) : M → E) x) ↔
      DifferentiableWithinAt 𝕜 ((↑(e'.extend I') : M' → E') ∘ f ∘ (↑(e.extend I).symm : E → M))
        ((↑(e.extend I) : M → E) '' s) ((↑(e.extend I) : M → E) x))
⊢ MDifferentiableWithinAt I I' f s x ↔
    ContinuousWithinAt f s x ∧
      DifferentiableWithinAt 𝕜 ((↑(e'.extend I') : M' → E') ∘ f ∘ (↑(e.extend I).symm : E → M))
        ((↑(e.extend I) : M → E) '' s) ((↑(e.extend I) : M → E) x)

Tactic:
rw [mdifferentiableWithinAt_iff_of_mem_maximalAtlas he he' hx hy, and_congr_right_iff]

Premises used: mdifferentiableWithinAt_iff_of_mem_maximalAtlas, and_congr_right_iff
-- 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
e : OpenPartialHomeomorph M H
e' : OpenPartialHomeomorph M' H'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x : M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I 1 M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas I' 1 M') e'
hs : s ⊆ e.source
hx : x ∈ e.source
hy : f x ∈ e'.source
⊢ ContinuousWithinAt f s x →
    (DifferentiableWithinAt 𝕜 ((↑(e'.extend I') : M' → E') ∘ f ∘ (↑(e.extend I).symm : E → M))
        ((↑(e.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(e.extend I) : M → E) x) ↔
      DifferentiableWithinAt 𝕜 ((↑(e'.extend I') : M' → E') ∘ f ∘ (↑(e.extend I).symm : E → M))
        ((↑(e.extend I) : M → E) '' s) ((↑(e.extend I) : M → E) x))

Tactic:
fun _ => differentiableWithinAt_congr_nhds ?_

Premises used: differentiableWithinAt_congr_nhds
-- 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
e : OpenPartialHomeomorph M H
e' : OpenPartialHomeomorph M' H'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x : M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I 1 M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas I' 1 M') e'
hs : s ⊆ e.source
hx : x ∈ e.source
hy : f x ∈ e'.source
refine :
  ContinuousWithinAt f s x →
    𝓝[(↑(e.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(e.extend I) : M → E) x =
      𝓝[(↑(e.extend I) : M → E) '' s] (↑(e.extend I) : M → E) x
⊢ ContinuousWithinAt f s x →
    (DifferentiableWithinAt 𝕜 ((↑(e'.extend I') : M' → E') ∘ f ∘ (↑(e.extend I).symm : E → M))
        ((↑(e.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(e.extend I) : M → E) x) ↔
      DifferentiableWithinAt 𝕜 ((↑(e'.extend I') : M' → E') ∘ f ∘ (↑(e.extend I).symm : E → M))
        ((↑(e.extend I) : M → E) '' s) ((↑(e.extend I) : M → E) x))

Tactic:
refine fun _ => differentiableWithinAt_congr_nhds ?_

Premises used: differentiableWithinAt_congr_nhds
-- 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
e : OpenPartialHomeomorph M H
e' : OpenPartialHomeomorph M' H'
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x : M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I 1 M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas I' 1 M') e'
hs : s ⊆ e.source
hx : x ∈ e.source
hy : f x ∈ e'.source
h : ContinuousWithinAt f s x
simp_rw :
  (↑(e.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E) =ᶠ[𝓝 ((↑(e.extend I) : M → E) x)] (↑(e.extend I) : M → E) '' s
⊢ 𝓝[(↑(e.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑(e.extend I) : M → E) x =
    𝓝[(↑(e.extend I) : M → E) '' s] (↑(e.extend I) : M → E) x

Tactic:
simp_rw [nhdsWithin_eq_iff_eventuallyEq, e.extend_symm_preimage_inter_range_eventuallyEq hs hx]

Premises used: nhdsWithin_eq_iff_eventuallyEq, OpenPartialHomeomorph.extend_symm_preimage_inter_range_eventuallyEq
-- 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'
x : M
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x' : M
y : M'
hx : x' ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
hy : f x' ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
⊢ MDifferentiableWithinAt I I' f s x' ↔
    ContinuousWithinAt f s x' ∧
      DifferentiableWithinAt 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x')

Tactic:
mdifferentiableWithinAt_iff_of_mem_maximalAtlas (chart_mem_maximalAtlas x)
    (chart_mem_maximalAtlas y) hx hy

Premises used: mdifferentiableWithinAt_iff_of_mem_maximalAtlas, extChartAt, IsManifold.chart_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'
x : M
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x' : M
y : M'
hx : x' ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
hy : f x' ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
⊢ MDifferentiableWithinAt I I' f s x' ↔
    ContinuousWithinAt f s x' ∧
      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) x')

Tactic:
(mdifferentiableWithinAt_iff_of_mem_source hx hy).trans ?_

Premises used: Iff.trans, mdifferentiableWithinAt_iff_of_mem_source