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
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
x : M
y : M'
z : E
hz :
  (z ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
w : M := (↑(extChartAt I x).symm : E → M) z
this : w ∈ s
h : ContMDiffWithinAt I I' n f s w
w1 : w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ f w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source

Tactic:
simp only [w, hz, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.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
inst_12 : IsManifold I' n M'
x : M
y : M'
z : E
hz :
  (z ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
w : M := (↑(extChartAt I x).symm : E → M) z
this : w ∈ s
h : ContMDiffWithinAt I I' n f s w
w1 : w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ f w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source

Tactic:
have w2 : f w ∈ (chartAt H' y).source := by simp only [w, hz, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.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
inst_12 : IsManifold I' n M'
x : M
y : M'
z : E
hz :
  (z ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
w : M := (↑(extChartAt I x).symm : E → M) z
this : w ∈ s
h : ContMDiffWithinAt I I' n f s w
w1 : w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
w2 : f w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
⊢ ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
    ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
    ((↑(extChartAt I x) : M → E) w)

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

Premises used: And.right, Iff.mp, contMDiffWithinAt_iff_of_mem_source, ContDiffWithinAt.mono
-- 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
inst_12 : IsManifold I' n M'
x : M
y : M'
z : E
hz :
  (z ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
w : M := (↑(extChartAt I x).symm : E → M) z
this : w ∈ s
h : ContMDiffWithinAt I I' n f s w
w1 : w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
w2 : f w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
h₁ : z = (↑(extChartAt I x) : M → E) w
mp :
  (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source) ⊆
    (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
⊢ ContDiffWithinAt 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
    ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)) z

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

Premises used: And.right, Iff.mp, contMDiffWithinAt_iff_of_mem_source, ContDiffWithinAt.mono
-- 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
inst_12 : IsManifold I' n M'
x : M
y : M'
z : E
hz :
  (z ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
w : M := (↑(extChartAt I x).symm : E → M) z
this : w ∈ s
h : ContMDiffWithinAt I I' n f s w
w1 : w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
w2 : f w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
⊢ z = (↑(extChartAt I x) : M → E) w

Tactic:
simp only [w, hz, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.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
inst_12 : IsManifold I' n M'
x : M
y : M'
z : E
hz :
  (z ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) z ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
    (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z) ∈ s ∧
      f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) z)) ∈
        (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
w : M := (↑(extChartAt I x).symm : E → M) z
this : w ∈ s
h : ContMDiffWithinAt I I' n f s w
w1 : w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
w2 : f w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
mp mp₁ mp₂ :
  ∀ ⦃my_y : E⦄,
    my_y ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source) →
      my_y ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
mp₃ mp₄ :
  ∀ ⦃my_y : E⦄,
    (my_y ∈ range (↑I : H → E) ∧ (↑I.symm : E → H) my_y ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target) ∧
        (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) my_y) ∈ s ∧
          f ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ((↑I.symm : E → H) my_y)) ∈
            (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source →
      my_y ∈ (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)
⊢ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source) ⊆
    (↑(extChartAt I x).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)

Tactic:
mfld_set_tac
-- Module: Mathlib.Geometry.Manifold.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
inst_12 : IsManifold I' n M'
hcont : ContinuousOn f s
hdiff :
  ∀ (x : M) (y : M'),
    ContDiffOn 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
x : M
hx : x ∈ s
⊢ ContMDiffWithinAt I I' n f s x

Tactic:
(contDiffWithinAt_localInvariantProp n).liftPropWithinAt_iff.mpr ?_

Premises used: Iff.mpr, ContMDiffWithinAt, contDiffWithinAt_localInvariantProp, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_iff
-- 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
inst_12 : IsManifold I' n M'
hcont : ContinuousOn f s
hdiff :
  ∀ (x : M) (y : M'),
    ContDiffOn 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
x : M
hx : x ∈ s
mpr :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAtProp I I' n
      ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
          (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source))
      ((↑(chartAt H x) : M → H) x)
⊢ ContMDiffWithinAt I I' n f s x

Tactic:
refine (contDiffWithinAt_localInvariantProp n).liftPropWithinAt_iff.mpr ?_

Premises used: Iff.mpr, contDiffWithinAt_localInvariantProp, StructureGroupoid.LocalInvariantProp.liftPropWithinAt_iff
-- 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
inst_12 : IsManifold I' n M'
hcont : ContinuousOn f s
hdiff :
  ∀ (x : M) (y : M'),
    ContDiffOn 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
x : M
hx : x ∈ s
⊢ ContinuousWithinAt f s x ∧
    ContDiffWithinAtProp I I' n
      ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
          (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source))
      ((↑(chartAt H x) : M → H) x)

Tactic:
⟨hcont x hx, ?_⟩

Premises used: And.intro
-- 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
inst_12 : IsManifold I' n M'
hcont : ContinuousOn f s
hdiff :
  ∀ (x : M) (y : M'),
    ContDiffOn 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
x : M
hx : x ∈ s
mpr :
  ContDiffWithinAtProp I I' n
    ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
      (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
        (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source))
    ((↑(chartAt H x) : M → H) x)
⊢ ContinuousWithinAt f s x ∧
    ContDiffWithinAtProp I I' n
      ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
      ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
          (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source))
      ((↑(chartAt H x) : M → H) x)

Tactic:
refine ⟨hcont x 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'
f : M → M'
s : Set M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
hcont : ContinuousOn f s
hdiff :
  ∀ (x : M) (y : M'),
    ContDiffOn 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
x : M
hx : x ∈ s
mpr :
  ContDiffWithinAt 𝕜 n
    ((↑I' : H' → E') ∘
      ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
        ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩
          (↑I.symm : E → H) ⁻¹'
            (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
              f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source) ∩
      range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x))
⊢ ContDiffWithinAtProp I I' n
    ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M))
    ((OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
      (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
        (s ∩ f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source))
    ((↑(chartAt H x) : M → H) x)

Tactic:
dsimp [ContDiffWithinAtProp]

Premises used: ContDiffWithinAtProp
-- 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
inst_12 : IsManifold I' n M'
hcont : ContinuousOn f s
hdiff :
  ∀ (x : M) (y : M'),
    ContDiffOn 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
x : M
hx : x ∈ s
⊢ (↑(extChartAt I x) : M → E) x ∈
    (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)

Tactic:
simp only [hx, mfld_simps]
-- 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
inst_12 : IsManifold I' n M'
hcont : ContinuousOn f s
hdiff :
  ∀ (x : M) (y : M'),
    ContDiffOn 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
x : M
hx : x ∈ s
h :
  (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
        ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩
          (↑I.symm : E → H) ⁻¹'
            (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
              f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source) ∩
      range (↑I : H → E) =
    (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)
⊢ ContDiffWithinAt 𝕜 n
    ((↑I' : H' → E') ∘
      ((↑(chartAt H' (f x)) : M' → H') ∘ f ∘ (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M)) ∘ (↑I.symm : E → H))
    ((↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
        ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩
          (↑I.symm : E → H) ⁻¹'
            (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
              f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source) ∩
      range (↑I : H → E))
    ((↑I : H → E) ((↑(chartAt H x) : M → H) x))

Tactic:
convert! hdiff x (f x) (extChartAt I x x) (by simp only [hx, mfld_simps]) using 1

Premises used: extChartAt, PartialEquiv.toFun
-- 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
inst_12 : IsManifold I' n M'
hcont : ContinuousOn f s
hdiff :
  ∀ (x : M) (y : M'),
    ContDiffOn 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
x : M
hx : x ∈ s
h h₁ h₂ h₃ :
  ∀ (my_y : E),
    my_y ∈
        (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
            ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩
              (↑I.symm : E → H) ⁻¹'
                (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
                  f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source) ∩
          range (↑I : H → E) ↔
      my_y ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)
⊢ (↑I.symm : E → H) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).target ∩
        ((↑I.symm : E → H) ⁻¹' (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' s ∩
          (↑I.symm : E → H) ⁻¹'
            (↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹'
              f ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H' (f x))).source) ∩
      range (↑I : H → E) =
    (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)

Tactic:
mfld_set_tac
-- 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
rw :
  (ContinuousOn f s ∧
      ∀ (x : M) (y : M'),
        ContDiffOn 𝕜 0 ((↑(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))) ↔
    ContinuousOn f s
⊢ ContMDiffOn I I' 0 f s ↔ ContinuousOn f s

Tactic:
rw [contMDiffOn_iff]

Premises used: contMDiffOn_iff
-- 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
⊢ (ContinuousOn f s ∧
      ∀ (x : M) (y : M'),
        ContDiffOn 𝕜 0 ((↑(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))) ↔
    ContinuousOn f s

Tactic:
⟨fun h ↦ h.1, fun h ↦ ⟨h, ?_⟩⟩

Premises used: And.left, And.intro, Iff.intro