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'
x : M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n 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' ∧
      ContDiffWithinAt 𝕜 n ((↑(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' ∧
      ContDiffWithinAt 𝕜 n ((↑(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' ∧
      ContDiffWithinAt 𝕜 n ((↑(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' ∧
      ContDiffWithinAt 𝕜 n ((↑(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' ∧
      ContDiffWithinAt 𝕜 n ((↑(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' ∧
      ContDiffWithinAt 𝕜 n ((↑(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' ∧
      ContDiffWithinAt 𝕜 n ((↑(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' ∧
      ContDiffWithinAt 𝕜 n ((↑(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.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
e' : OpenPartialHomeomorph M' H'
f : M → M'
s : Set M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas I' n M') e'
hs : s ⊆ e.source
h2s : MapsTo f s e'.source
simp_rw :
  (∀ x ∈ s, ContMDiffWithinAt I I' n f s x) ↔
    ∀ (x : M) (x_1 : x ∈ s),
      ContinuousWithinAt f s x ∧
        ContDiffWithinAt 𝕜 n ((↑(e'.extend I') : M' → E') ∘ f ∘ (↑(e.extend I).symm : E → M))
          ((↑(e.extend I) : M → E) '' s) ((↑(e.extend I) : M → E) x)
⊢ ContMDiffOn I I' n f s ↔
    ContinuousOn f s ∧
      ContDiffOn 𝕜 n ((↑(e'.extend I') : M' → E') ∘ f ∘ (↑(e.extend I).symm : E → M)) ((↑(e.extend I) : M → E) '' s)

Tactic:
simp_rw [ContinuousOn, ContDiffOn, Set.forall_mem_image, ← forall_and, ContMDiffOn]

Premises used: ContDiffOn, ContinuousOn, Set.forall_mem_image, forall_and, ContMDiffOn
-- 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
e' : OpenPartialHomeomorph M' H'
f : M → M'
s : Set M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas I' n M') e'
hs : s ⊆ e.source
h2s : MapsTo f s e'.source
⊢ (∀ x ∈ s, ContMDiffWithinAt I I' n f s x) ↔
    ∀ (x : M) (x_1 : x ∈ s),
      ContinuousWithinAt f s x ∧
        ContDiffWithinAt 𝕜 n ((↑(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 => contMDiffWithinAt_iff_image he he' hs (hs hx) (h2s hx)

Premises used: contMDiffWithinAt_iff_image, forall₂_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'
e : OpenPartialHomeomorph M H
e' : OpenPartialHomeomorph M' H'
f : M → M'
s : Set M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas I' n M') e'
hs : s ⊆ e.source
h2s : MapsTo f s e'.source
⊢ (∀ x ∈ s, ContMDiffWithinAt I I' n f s x) ↔
    ∀ (x : M) (x_1 : x ∈ s),
      ContinuousWithinAt f s x ∧
        ContDiffWithinAt 𝕜 n ((↑(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 => contMDiffWithinAt_iff_image he he' hs (hs hx) (h2s hx)

Premises used: contMDiffWithinAt_iff_image, forall₂_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'
e : OpenPartialHomeomorph M H
e' : OpenPartialHomeomorph M' H'
f : M → M'
s : Set M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
he : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) e
he' : Membership.mem (γ := Set (OpenPartialHomeomorph M' H')) (maximalAtlas I' n M') e'
hs : s ⊆ e.source
h2s : MapsTo f s e'.source
⊢ ContMDiffOn I I' n f s ↔
    ContDiffOn 𝕜 n ((↑(e'.extend I') : M' → E') ∘ f ∘ (↑(e.extend I).symm : E → M)) ((↑(e.extend I) : M → E) '' s)

Tactic:
(contMDiffOn_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: OpenPartialHomeomorph.continuousOn_writtenInExtend_iff, contMDiffOn_iff_of_mem_maximalAtlas, ContDiffOn.continuousOn, Iff.mp, Iff.trans, and_iff_right_of_imp
-- 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'
hs : s ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
h2s : MapsTo f s (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
⊢ ContMDiffOn I I' n f s ↔
    ContinuousOn f s ∧
      ContDiffOn 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
        ((↑(extChartAt I x) : M → E) '' s)

Tactic:
contMDiffOn_iff_of_mem_maximalAtlas (chart_mem_maximalAtlas x) (chart_mem_maximalAtlas y) hs
    h2s

Premises used: IsManifold.chart_mem_maximalAtlas, contMDiffOn_iff_of_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'
s : Set M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n 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
-- 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'
hs : s ⊆ (extChartAt I x).source
h2s : MapsTo f s (extChartAt I' y).source
hs₁ : s ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
⊢ MapsTo f s (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source

Tactic:
rw [extChartAt_source] at hs h2s

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
inst_12 : IsManifold I' n M'
x : M
y : M'
hs : s ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
h2s : MapsTo f s (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
⊢ ContMDiffOn I I' n f s ↔
    ContDiffOn 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x) : M → E) '' s)

Tactic:
contMDiffOn_iff_of_mem_maximalAtlas' (chart_mem_maximalAtlas x)
    (chart_mem_maximalAtlas y) hs h2s

Premises used: contMDiffOn_iff_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'
s : Set M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
x : M
y : M'
hs : s ⊆ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source
h2s : MapsTo f s (OpenPartialHomeomorph.toPartialEquiv (chartAt H' y)).source
⊢ ContMDiffOn I I' n f s ↔
    ContDiffOn 𝕜 n ((↑(extChartAt I' y) : M' → E') ∘ f ∘ (↑(extChartAt I x).symm : E → M))
      ((↑(extChartAt I x) : M → E) '' s)

Tactic:
exact contMDiffOn_iff_of_mem_maximalAtlas' (chart_mem_maximalAtlas x)
    (chart_mem_maximalAtlas y) hs h2s

Premises used: contMDiffOn_iff_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'
s : Set M
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold I' n M'
mp :
  ContMDiffOn I I' n f s →
    ContinuousOn f s ∧
      ∀ (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))
mpr :
  (ContinuousOn f s ∧
      ∀ (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))) →
    ContMDiffOn I I' n f s
⊢ ContMDiffOn I I' n f s ↔
    ContinuousOn f s ∧
      ∀ (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))

Tactic:
constructor
-- 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'
h : ContMDiffOn I I' n f s
⊢ ContinuousOn f s ∧
    ∀ (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))

Tactic:
⟨fun x hx => (h x hx).1, fun x y z hz => ?_⟩

Premises used: ChartedSpace.LiftPropWithinAt.continuousWithinAt, 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'
h : ContMDiffOn I I' n f s
mp :
  ∀ (x : M) (y : M') (z : E)
    (hz : z ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' 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)) z
⊢ ContinuousOn f s ∧
    ∀ (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))

Tactic:
refine ⟨fun x hx => (h x hx).1, fun x y z hz => ?_⟩
-- 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'
h : ContMDiffOn I I' n f s
x : M
y : M'
z : E
hz : z ∈ (extChartAt I x).target ∩ (↑(extChartAt I x).symm : E → M) ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source)
⊢ (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

Tactic:
simp only [mfld_simps] at hz
-- 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'
h : ContMDiffOn I I' n f s
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
⊢ w ∈ s

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'
h : ContMDiffOn I I' n f s
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
⊢ w ∈ s

Tactic:
have : w ∈ s := 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'
h : ContMDiffOn I I' n f s
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
⊢ ContMDiffWithinAt I I' n f s w

Tactic:
specialize h w 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
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
⊢ w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).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
⊢ w ∈ (OpenPartialHomeomorph.toPartialEquiv (chartAt H x)).source

Tactic:
have w1 : w ∈ (chartAt H x).source := by simp only [w, hz, mfld_simps]