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 : ℕ∞ω
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)
⊢ 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))

Tactic:
simp only [ContDiffWithinAtProp, mfld_simps, preimage_comp, comp_assoc]

Premises used: Set.preimage_comp, ContDiffWithinAtProp, Function.comp_assoc
-- 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'
x : M
n : ℕ∞ω
rw :
  ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' univ ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x) ↔
    ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)
⊢ ContMDiffAt I I' n f x ↔
    ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x)

Tactic:
rw [← contMDiffWithinAt_univ, contMDiffWithinAt_iff_source]

Premises used: contMDiffWithinAt_iff_source, contMDiffWithinAt_univ
-- 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'
x : M
n : ℕ∞ω
⊢ ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' univ ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x) ↔
    ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(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'
e : OpenPartialHomeomorph M H
f : M → M'
s : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
hx : x ∈ e.source
⊢ x ∈ e.source

Tactic:
have h2x := hx
-- 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'
e : OpenPartialHomeomorph M H
f : M → M'
s : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
hx h2x : x ∈ e.source
⊢ x ∈ (e.extend I).source

Tactic:
rw [← e.extend_source (I := I)] at h2x

Premises used: OpenPartialHomeomorph.extend_source
-- 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'
e : OpenPartialHomeomorph M H
f : M → M'
s : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
hx : x ∈ e.source
h2x : x ∈ (e.extend I).source
simp_rw :
  ContinuousWithinAt (f ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x) ∧
      ContDiffWithinAt 𝕜 n
        ((↑I' : H' → E') ∘ ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑e.symm : H → M)) ∘ (↑I.symm : E → H))
        ((↑I.symm : E → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : M → H) x)) ↔
    ContinuousWithinAt (f ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x) ∧
      ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(e.extend I).symm : E → M))
        ((↑(e.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(e.extend I) : M → E) x)
⊢ ContMDiffWithinAt I I' n f s x ↔
    ContMDiffWithinAt 𝓘(𝕜, E) I' n (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:
simp_rw [ContMDiffWithinAt,
    (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_indep_chart_source he hx,
    StructureGroupoid.liftPropWithinAt_self_source,
    e.extend_symm_continuousWithinAt_comp_right_iff, contDiffWithinAtProp_self_source,
    ContDiffWithinAtProp, Function.comp, e.left_inv hx, (e.extend I).left_inv h2x]

Premises used: ContMDiffWithinAt, Function.comp, contDiffWithinAtProp_self_source, OpenPartialHomeomorph.left_inv, contDiffWithinAt_localInvariantProp, OpenPartialHomeomorph.extend_symm_continuousWithinAt_comp_right_iff, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_source, PartialEquiv.left_inv, StructureGroupoid.liftPropWithinAt_self_source, ContDiffWithinAtProp, OpenPartialHomeomorph.extend
-- 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'
e : OpenPartialHomeomorph M H
f : M → M'
s : Set M
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
hx : x ∈ e.source
h2x : x ∈ (e.extend I).source
⊢ ContinuousWithinAt (f ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x) ∧
      ContDiffWithinAt 𝕜 n
        ((↑I' : H' → E') ∘ ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑e.symm : H → M)) ∘ (↑I.symm : E → H))
        ((↑I.symm : E → H) ⁻¹' (↑e.symm : H → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑I : H → E) ((↑e : M → H) x)) ↔
    ContinuousWithinAt (f ∘ (↑e.symm : H → M)) ((↑e.symm : H → M) ⁻¹' s) ((↑e : M → H) x) ∧
      ContDiffWithinAt 𝕜 n ((↑I' : H' → E') ∘ (↑(chartAt H' (f x)) : M' → H') ∘ 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:
rfl
-- 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 : ℕ∞ω
inst_11 : IsManifold I n M
x' : M
hx' : x' ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ ContMDiffWithinAt I I' n f s x' ↔
    ContMDiffWithinAt 𝓘(𝕜, E) I' n (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:
contMDiffWithinAt_iff_source_of_mem_maximalAtlas (chart_mem_maximalAtlas x) hx'

Premises used: extChartAt, contMDiffWithinAt_iff_source_of_mem_maximalAtlas, IsManifold.chart_mem_maximalAtlas
-- 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'
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
x' : M
hx' : x' ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
simp_rw :
  ContMDiffWithinAt I I' n f univ x' ↔
    ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x')
simp_rw₁ :
  ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x).symm : E → M) ⁻¹' univ ∩ range (↑I : H → E)) ((↑(extChartAt I x) : M → E) x') ↔
    ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x')
simp_rw₂ :
  ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (↑(extChartAt I x).symm : E → M)) (univ ∩ range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x') ↔
    ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x')
⊢ ContMDiffAt I I' n f x' ↔
    ContMDiffWithinAt 𝓘(𝕜, E) I' n (f ∘ (↑(extChartAt I x).symm : E → M)) (range (↑I : H → E))
      ((↑(extChartAt I x) : M → E) x')

Tactic:
simp_rw [ContMDiffAt, contMDiffWithinAt_iff_source_of_mem_source hx', preimage_univ, univ_inter]

Premises used: Set.univ_inter, contMDiffWithinAt_iff_source_of_mem_source, ContMDiffAt, Set.preimage_univ
-- 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
n : ℕ∞ω
inst_11 : IsManifold I' n M'
x : M
y : M'
hy : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
rw :
  ContinuousWithinAt f s x →
    (LiftPropWithinAt (ContDiffWithinAtProp I I' n) ((↑(chartAt H' y) : M' → H') ∘ f) s x ↔
      LiftPropWithinAt (ContDiffWithinAtProp I 𝓘(𝕜, E') n) ((↑(extChartAt I' y) : M' → E') ∘ f) s x)
⊢ LiftPropWithinAt (ContDiffWithinAtProp I I' n) f s x ↔
    ContinuousWithinAt f s x ∧
      LiftPropWithinAt (ContDiffWithinAtProp I 𝓘(𝕜, E') n) ((↑(extChartAt I' y) : M' → E') ∘ f) s x

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

Premises used: contDiffWithinAt_localInvariantProp, IsManifold.chart_mem_maximalAtlas, and_congr_right, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_indep_chart_target
-- 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
n : ℕ∞ω
inst_11 : IsManifold I' n 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 ∧
      ContDiffWithinAtProp I I' n
        (((↑(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 ∧
      ContDiffWithinAtProp I 𝓘(𝕜, E') n
        (((↑(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 (ContDiffWithinAtProp I I' n) ((↑(chartAt H' y) : M' → H') ∘ f) s x ↔
    LiftPropWithinAt (ContDiffWithinAtProp I 𝓘(𝕜, E') n) ((↑(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.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
n : ℕ∞ω
inst_11 : IsManifold I' n M'
x : M
y : M'
hy : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
hf : ContinuousWithinAt f s x
simp_rw :
  True ∧
      ContDiffWithinAtProp I I' n
        (((↑(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 ∧
      ContDiffWithinAtProp I 𝓘(𝕜, E') n
        (((↑(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 ∧
      ContDiffWithinAtProp I I' n
        (((↑(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 ∧
      ContDiffWithinAtProp I 𝓘(𝕜, E') n
        (((↑(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.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
n : ℕ∞ω
inst_11 : IsManifold I' n 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 := I')] at hy

Premises used: extChartAt_source
-- 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
n : ℕ∞ω
inst_11 : IsManifold I' n 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 := I')] at hy

Premises used: extChartAt_source
-- 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
n : ℕ∞ω
inst_11 : IsManifold I' n M'
x : M
y : M'
hy : f x ∈ (extChartAt I' y).source
hf : ContinuousWithinAt f s x
simp_rw :
  True ∧
      ContDiffWithinAtProp I I' n
        (((↑(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 ∧
      ContDiffWithinAtProp I 𝓘(𝕜, E') n
        (((↑(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 ∧
      ContDiffWithinAtProp I I' n
        (((↑(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 ∧
      ContDiffWithinAtProp I 𝓘(𝕜, E') n
        (((↑(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.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
n : ℕ∞ω
inst_11 : IsManifold I' n M'
x : M
y : M'
hy : f x ∈ (extChartAt I' y).source
hf : ContinuousWithinAt f s x
⊢ True ∧
      ContDiffWithinAtProp I I' n
        (((↑(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 ∧
      ContDiffWithinAtProp I 𝓘(𝕜, E') n
        (((↑(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.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'
n : ℕ∞ω
inst_11 : IsManifold I' n M'
x : M
y : M'
hy : f x ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
rw :
  ContMDiffWithinAt I I' n f univ x ↔ ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n ((↑(extChartAt I' y) : M' → E') ∘ f) x
rw₁ :
  ContinuousWithinAt f univ x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n ((↑(extChartAt I' y) : M' → E') ∘ f) univ x ↔
    ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n ((↑(extChartAt I' y) : M' → E') ∘ f) x
rw₂ :
  ContinuousAt f x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n ((↑(extChartAt I' y) : M' → E') ∘ f) univ x ↔
    ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n ((↑(extChartAt I' y) : M' → E') ∘ f) x
rw₃ rw₄ :
  ContinuousAt f x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n ((↑(extChartAt I' y) : M' → E') ∘ f) univ x ↔
    ContinuousAt f x ∧ ContMDiffWithinAt I 𝓘(𝕜, E') n ((↑(extChartAt I' y) : M' → E') ∘ f) univ x
⊢ ContMDiffAt I I' n f x ↔ ContinuousAt f x ∧ ContMDiffAt I 𝓘(𝕜, E') n ((↑(extChartAt I' y) : M' → E') ∘ f) x

Tactic:
rw [ContMDiffAt, contMDiffWithinAt_iff_target_of_mem_source hy, continuousWithinAt_univ,
    ContMDiffAt]

Premises used: continuousWithinAt_univ, contMDiffWithinAt_iff_target_of_mem_source, ContMDiffAt