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
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
refine :
  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') ↔
    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')
⊢ 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:
refine (mdifferentiableWithinAt_iff_of_mem_source hx hy).trans ?_

Premises used: Iff.trans, 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'
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
⊢ x' ∈ (extChartAt I x).source

Tactic:
rw [← extChartAt_source I] at hx

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

Tactic:
rw [← extChartAt_source I] at hx

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'
x : M
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x' : M
y : M'
hx : x' ∈ (extChartAt I x).source
hy : f x' ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
⊢ 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'
x : M
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x' : M
y : M'
hx : x' ∈ (extChartAt I x).source
hy : f x' ∈ (extChartAt I' y).source
rw :
  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') ↔
      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'))
⊢ 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') ↔
    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:
rw [and_congr_right_iff]

Premises used: 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'
x : M
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x' : M
y : M'
hx : x' ∈ (extChartAt I x).source
hy : f x' ∈ (extChartAt I' y).source
set :
  let e := extChartAt I x;
  ∀ (hx : x' ∈ e.source),
    ContinuousWithinAt f s x' →
      (DifferentiableWithinAt 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑e.symm : E → M))
          ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑e : M → E) x') ↔
        DifferentiableWithinAt 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑e.symm : E → M))
          (e.target ∩ (↑e.symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) ((↑e : M → E) 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') ↔
      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:
set e := extChartAt I x

Premises used: extChartAt
-- 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'
hy : f x' ∈ (extChartAt I' y).source
e : PartialEquiv M E := extChartAt I x
hx : x' ∈ e.source
e' : PartialEquiv M' E' := extChartAt I' (f x)
⊢ ContinuousWithinAt f s x' →
    (DifferentiableWithinAt 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑e.symm : E → M))
        ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑e : M → E) x') ↔
      DifferentiableWithinAt 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑e.symm : E → M))
        (e.target ∩ (↑e.symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) ((↑e : M → E) x'))

Tactic:
fun hc => 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'
x : M
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x' : M
y : M'
hy : f x' ∈ (extChartAt I' y).source
e : PartialEquiv M E := extChartAt I x
hx : x' ∈ e.source
e' : PartialEquiv M' E' := extChartAt I' (f x)
refine :
  ∀ (hc : ContinuousWithinAt f s x'),
    𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x' =
      𝓝[e.target ∩ (↑e.symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)] (↑e : M → E) x'
⊢ ContinuousWithinAt f s x' →
    (DifferentiableWithinAt 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑e.symm : E → M))
        ((↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑e : M → E) x') ↔
      DifferentiableWithinAt 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑e.symm : E → M))
        (e.target ∩ (↑e.symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) ((↑e : M → E) x'))

Tactic:
refine fun hc => 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'
x : M
s : Set M
inst_11 : IsManifold I 1 M
inst_12 : IsManifold I' 1 M'
x' : M
y : M'
hy : f x' ∈ (extChartAt I' y).source
e : PartialEquiv M E := extChartAt I x
hx : x' ∈ e.source
e' : PartialEquiv M' E' := extChartAt I' (f x)
hc : ContinuousWithinAt f s x'
rw : f ⁻¹' (extChartAt I' y).source ∈ 𝓝[s] x'
⊢ 𝓝[(↑e.symm : E → M) ⁻¹' s ∩ range (↑I : H → E)] (↑e : M → E) x' =
    𝓝[e.target ∩ (↑e.symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)] (↑e : M → E) x'

Tactic:
rw [← e.image_source_inter_eq', ← map_extChartAt_nhdsWithin_eq_image' hx,
    ← map_extChartAt_nhdsWithin' hx, inter_comm, nhdsWithin_inter_of_mem]

Premises used: map_extChartAt_nhdsWithin', nhdsWithin_inter_of_mem, Set.inter_comm, PartialEquiv.image_source_inter_eq', map_extChartAt_nhdsWithin_eq_image'
-- 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'
hy : f x' ∈ (extChartAt I' y).source
e : PartialEquiv M E := extChartAt I x
hx : x' ∈ e.source
e' : PartialEquiv M' E' := extChartAt I' (f x)
hc : ContinuousWithinAt f s x'
⊢ f ⁻¹' (extChartAt I' y).source ∈ 𝓝[s] x'

Tactic:
hc (extChartAt_source_mem_nhds' hy)

Premises used: Set.Mem, setOf, extChartAt_source_mem_nhds', Set.preimage
-- 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'
hy : f x' ∈ (extChartAt I' y).source
e : PartialEquiv M E := extChartAt I x
hx : x' ∈ e.source
e' : PartialEquiv M' E' := extChartAt I' (f x)
hc : ContinuousWithinAt f s x'
⊢ f ⁻¹' (extChartAt I' y).source ∈ 𝓝[s] x'

Tactic:
exact hc (extChartAt_source_mem_nhds' hy)

Premises used: extChartAt_source_mem_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'
x : 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
rw :
  ContinuousAt f x' ∧
      DifferentiableWithinAt 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' univ ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x') ↔
    ContinuousAt f x' ∧
      DifferentiableWithinAt 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x')
rw₁ :
  ContinuousAt f x' ∧
      DifferentiableWithinAt 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        (univ ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x') ↔
    ContinuousAt f x' ∧
      DifferentiableWithinAt 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x')
rw₂ rw₃ :
  ContinuousAt f x' ∧
      DifferentiableWithinAt 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x') ↔
    ContinuousAt f x' ∧
      DifferentiableWithinAt 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x')
⊢ ContinuousWithinAt f univ x' ∧
      DifferentiableWithinAt 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' univ ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x') ↔
    ContinuousAt f x' ∧
      DifferentiableWithinAt 𝕜 ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        (range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x')

Tactic:
rw [continuousWithinAt_univ, preimage_univ, univ_inter]

Premises used: continuousWithinAt_univ, Set.univ_inter, Set.preimage_univ
-- 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'
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
h2s : MapsTo f s e'.source
simp_rw :
  (∀ x ∈ s, MDifferentiableWithinAt I I' f s x) ↔
    ∀ (x : M) (x_1 : x ∈ s),
      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)
⊢ MDifferentiableOn I I' f s ↔
    ContinuousOn f s ∧
      DifferentiableOn 𝕜 ((↑(e'.extend I') : M' → E') ∘ f ∘ (↑(e.extend I).symm : E → M)) ((↑(e.extend I) : M → E) '' s)

Tactic:
simp_rw [ContinuousOn, DifferentiableOn, Set.forall_mem_image, ← forall_and, MDifferentiableOn]

Premises used: MDifferentiableOn, DifferentiableOn, ContinuousOn, Set.forall_mem_image, forall_and
-- 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'
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
h2s : MapsTo f s e'.source
⊢ (∀ x ∈ s, MDifferentiableWithinAt I I' f s x) ↔
    ∀ (x : M) (x_1 : x ∈ s),
      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:
forall₂_congr fun x hx => mdifferentiableWithinAt_iff_image he he' hs (hs hx) (h2s hx)

Premises used: mdifferentiableWithinAt_iff_image, forall₂_congr
-- 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'
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
h2s : MapsTo f s e'.source
⊢ (∀ x ∈ s, MDifferentiableWithinAt I I' f s x) ↔
    ∀ (x : M) (x_1 : x ∈ s),
      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:
exact forall₂_congr fun x hx => mdifferentiableWithinAt_iff_image he he' hs (hs hx) (h2s hx)

Premises used: mdifferentiableWithinAt_iff_image, forall₂_congr
-- 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'
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
h2s : MapsTo f s e'.source
⊢ MDifferentiableOn I I' f s ↔
    DifferentiableOn 𝕜 ((↑(e'.extend I') : M' → E') ∘ f ∘ (↑(e.extend I).symm : E → M)) ((↑(e.extend I) : M → E) '' s)

Tactic:
(mdifferentiableOn_iff_of_mem_maximalAtlas he he' hs h2s).trans <| and_iff_right_of_imp fun h ↦
    (e.continuousOn_writtenInExtend_iff hs h2s).1 h.continuousOn

Premises used: DifferentiableOn.continuousOn, OpenPartialHomeomorph.continuousOn_writtenInExtend_iff, Iff.mp, Iff.trans, and_iff_right_of_imp, 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 ↔
    ContinuousOn 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 ⊆ (extChartAt I x).source
h2s : MapsTo f s (extChartAt I' y).source
⊢ s ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source

Tactic:
rw [extChartAt_source] at hs h2s

Premises used: extChartAt_source