awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
x : M
n : ℕ∞ω
refine_1 :
  ∀ (h : ContinuousWithinAt f s x),
    ContinuousWithinAt (f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
refine_2 :
  ∀
    (h :
      ContinuousWithinAt (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
⊢ ContinuousWithinAt f s x ↔
    ContinuousWithinAt (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:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
x : M
n : ℕ∞ω
h : ContinuousWithinAt f s x
refine_1 :
  ContinuousWithinAt (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x)
refine_1₁ : MapsTo (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) s
refine_1₂ : (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) = x
⊢ ContinuousWithinAt (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:
apply h.comp_of_eq

Premises used: ContinuousWithinAt.comp_of_eq
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
x : M
n : ℕ∞ω
h : ContinuousWithinAt f s x
⊢ ContinuousWithinAt (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x)

Tactic:
(continuousAt_extChartAt_symm x).continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, continuousAt_extChartAt_symm
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
x : M
n : ℕ∞ω
h : ContinuousWithinAt f s x
⊢ ContinuousWithinAt (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
    ((↑(extChartAt I x) : M → E) x)

Tactic:
exact (continuousAt_extChartAt_symm x).continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, continuousAt_extChartAt_symm
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
x : M
n : ℕ∞ω
h : ContinuousWithinAt f s x
⊢ MapsTo (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) s

Tactic:
(mapsTo_preimage _ _).mono_left inter_subset_left

Premises used: Set.inter_subset_left, Set.mapsTo_preimage, Set.MapsTo.mono_left
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
x : M
n : ℕ∞ω
h : ContinuousWithinAt f s x
⊢ MapsTo (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) s

Tactic:
exact (mapsTo_preimage _ _).mono_left inter_subset_left

Premises used: Set.inter_subset_left, Set.mapsTo_preimage, Set.MapsTo.mono_left
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
x : M
n : ℕ∞ω
h : ContinuousWithinAt f s x
⊢ (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) = x

Tactic:
extChartAt_to_inv x

Premises used: extChartAt_to_inv
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
x : M
n : ℕ∞ω
h : ContinuousWithinAt f s x
⊢ (↑(extChartAt I x).symm : E → M) ((↑(extChartAt I x) : M → E) x) = x

Tactic:
exact extChartAt_to_inv x

Premises used: extChartAt_to_inv
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
x : M
n : ℕ∞ω
h :
  ContinuousWithinAt (f ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
refine_2 : ContinuousWithinAt f (s ∩ (extChartAt I x).source) x
⊢ ContinuousWithinAt f s x

Tactic:
rw [← continuousWithinAt_inter (extChartAt_source_mem_nhds (I := I) x)]

Premises used: extChartAt_source_mem_nhds, continuousWithinAt_inter
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
x : M
n : ℕ∞ω
h :
  ContinuousWithinAt (f ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
apply :
  MapsTo (↑(extChartAt I x) : M → E) (s ∩ (extChartAt I x).source)
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E))
⊢ ContinuousWithinAt ((f ∘ (↑(extChartAt I x).symm : E → M)) ∘ (↑(extChartAt I x) : M → E))
    (s ∩ (extChartAt I x).source) x

Tactic:
apply h.comp (continuousAt_extChartAt x).continuousWithinAt

Premises used: continuousAt_extChartAt, ContinuousAt.continuousWithinAt, ContinuousWithinAt.comp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
x : M
n : ℕ∞ω
h :
  ContinuousWithinAt (f ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
y : M
hy : y ∈ s ∩ (extChartAt I x).source
⊢ y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source

Tactic:
simpa using hy.2

Premises used: And.right
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
x : M
n : ℕ∞ω
h :
  ContinuousWithinAt (f ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
y : M
hy : y ∈ s ∩ (extChartAt I x).source
⊢ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑(chartAt H x) : M → H) y) = y

Tactic:
have : (chartAt H x).symm ((chartAt H x) y) = y :=
          OpenPartialHomeomorph.left_inv _ (by simpa using hy.2)
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
x : M
n : ℕ∞ω
h :
  ContinuousWithinAt (f ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
y : M
hy : y ∈ s ∩ (extChartAt I x).source
this : (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑(chartAt H x) : M → H) y) = y
⊢ (↑(extChartAt I x) : M → E) y ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)

Tactic:
simpa [this] using hy.1

Premises used: And.left
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
x : M
n : ℕ∞ω
h :
  ContinuousWithinAt (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 ∘ (↑(extChartAt I x).symm : E → M)) ∘ (↑(extChartAt I x) : M → E))
    (s ∩ (extChartAt I x).source) x

Tactic:
have : ContinuousWithinAt ((f ∘ ↑(extChartAt I x).symm) ∘ ↑(extChartAt I x))
          (s ∩ (extChartAt I x).source) x := by
        apply h.comp (continuousAt_extChartAt x).continuousWithinAt
        intro y hy
        have : (chartAt H x).symm ((chartAt H x) y) = y :=
          OpenPartialHomeomorph.left_inv _ (by simpa using hy.2)
        simpa [this] using hy.1
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
x : M
n : ℕ∞ω
h :
  ContinuousWithinAt (f ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
this :
  ContinuousWithinAt ((f ∘ (↑(extChartAt I x).symm : E → M)) ∘ (↑(extChartAt I x) : M → E))
    (s ∩ (extChartAt I x).source) x
refine_2 :
  ∀ y ∈ s ∩ (extChartAt I x).source, f y = ((f ∘ (↑(extChartAt I x).symm : E → M)) ∘ (↑(extChartAt I x) : M → E)) y
refine_2₁ : f x = ((f ∘ (↑(extChartAt I x).symm : E → M)) ∘ (↑(extChartAt I x) : M → E)) x
⊢ ContinuousWithinAt f (s ∩ (extChartAt I x).source) x

Tactic:
apply this.congr

Premises used: ContinuousWithinAt.congr
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
x : M
n : ℕ∞ω
h :
  ContinuousWithinAt (f ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
this :
  ContinuousWithinAt ((f ∘ (↑(extChartAt I x).symm : E → M)) ∘ (↑(extChartAt I x) : M → E))
    (s ∩ (extChartAt I x).source) x
y : M
hy : y ∈ s ∩ (extChartAt I x).source
⊢ y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source

Tactic:
simpa using hy.2

Premises used: And.right
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
x : M
n : ℕ∞ω
h :
  ContinuousWithinAt (f ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
this :
  ContinuousWithinAt ((f ∘ (↑(extChartAt I x).symm : E → M)) ∘ (↑(extChartAt I x) : M → E))
    (s ∩ (extChartAt I x).source) x
y : M
hy : y ∈ s ∩ (extChartAt I x).source
⊢ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑(chartAt H x) : M → H) y) = y

Tactic:
have : (chartAt H x).symm ((chartAt H x) y) = y :=
          OpenPartialHomeomorph.left_inv _ (by simpa using hy.2)
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
x : M
n : ℕ∞ω
h :
  ContinuousWithinAt (f ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
this_1 :
  ContinuousWithinAt ((f ∘ (↑(extChartAt I x).symm : E → M)) ∘ (↑(extChartAt I x) : M → E))
    (s ∩ (extChartAt I x).source) x
y : M
hy : y ∈ s ∩ (extChartAt I x).source
this : (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑(chartAt H x) : M → H) y) = y
⊢ f y = ((f ∘ (↑(extChartAt I x).symm : E → M)) ∘ (↑(extChartAt I x) : M → E)) y

Tactic:
simp [this]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
x : M
n : ℕ∞ω
h :
  ContinuousWithinAt (f ∘ (↑(extChartAt I x).symm : E → M))
    ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
this :
  ContinuousWithinAt ((f ∘ (↑(extChartAt I x).symm : E → M)) ∘ (↑(extChartAt I x) : M → E))
    (s ∩ (extChartAt I x).source) x
⊢ f x = ((f ∘ (↑(extChartAt I x).symm : E → M)) ∘ (↑(extChartAt I x) : M → E)) x

Tactic:
simp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
x : M
n : ℕ∞ω
⊢ ContinuousWithinAt f s x ↔
    ContinuousWithinAt (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:
have : ContinuousWithinAt f s x
      ↔ ContinuousWithinAt (f ∘ ↑(extChartAt I x).symm) (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I)
        (extChartAt I x x) := by
    refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
    · apply h.comp_of_eq
      · exact (continuousAt_extChartAt_symm x).continuousWithinAt
      · exact (mapsTo_preimage _ _).mono_left inter_subset_left
      · exact extChartAt_to_inv x
    · rw [← continuousWithinAt_inter (extChartAt_source_mem_nhds (I := I) x)]
      have : ContinuousWithinAt ((f ∘ ↑(extChartAt I x).symm) ∘ ↑(extChartAt I x))
          (s ∩ (extChartAt I x).source) x := by
        apply h.comp (continuousAt_extChartAt x).continuousWithinAt
        intro y hy
        have : (chartAt H x).symm ((chartAt H x) y) = y :=
          OpenPartialHomeomorph.left_inv _ (by simpa using hy.2)
        simpa [this] using hy.1
      apply this.congr
      · intro y hy
        have : (chartAt H x).symm ((chartAt H x) y) = y :=
          OpenPartialHomeomorph.left_inv _ (by simpa using hy.2)
        simp [this]
      · simp
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Defs
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
x : M
n : ℕ∞ω
this :
  ContinuousWithinAt f s x ↔
    ContinuousWithinAt (f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x)
rw :
  ContinuousWithinAt f s x ∧
      ContDiffWithinAtProp I I' n
        ((↑(chartAt H' (f x)) : 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 f s x ∧
      ContDiffWithinAtProp 𝓘(𝕜, E) I' n
        ((↑(chartAt H' ((f ∘ (↑(extChartAt I x).symm : E → M)) ((↑(extChartAt I x) : M → E) x))) : M' → H') ∘
          (f ∘ (↑(extChartAt I x).symm : E → M)) ∘
            (↑(OpenPartialHomeomorph.symm (chartAt E ((↑(extChartAt I x) : M → E) x))) : E → E))
        ((↑(OpenPartialHomeomorph.symm (chartAt E ((↑(extChartAt I x) : M → E) x))) : E → E) ⁻¹'
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)))
        ((↑(chartAt E ((↑(extChartAt I x) : M → E) x)) : E → E) ((↑(extChartAt I x) : M → E) x))
⊢ ContinuousWithinAt f s x ∧
      ContDiffWithinAtProp I I' n
        ((↑(chartAt H' (f x)) : 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 (f ∘ (↑(extChartAt I x).symm : E → M))
        ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x) ∧
      ContDiffWithinAtProp 𝓘(𝕜, E) I' n
        ((↑(chartAt H' ((f ∘ (↑(extChartAt I x).symm : E → M)) ((↑(extChartAt I x) : M → E) x))) : M' → H') ∘
          (f ∘ (↑(extChartAt I x).symm : E → M)) ∘
            (↑(OpenPartialHomeomorph.symm (chartAt E ((↑(extChartAt I x) : M → E) x))) : E → E))
        ((↑(OpenPartialHomeomorph.symm (chartAt E ((↑(extChartAt I x) : M → E) x))) : E → E) ⁻¹'
          ((↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)))
        ((↑(chartAt E ((↑(extChartAt I x) : M → E) x)) : E → E) ((↑(extChartAt I x) : M → E) x))

Tactic:
rw [← this]