awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I : ModelWithCorners 𝕜 E H_1
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H_1 M
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H_1 M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h₁ : ContMDiffOn I I n (↑f : M → M') f.source
h₂ : ContMDiffOn I I n (↑f.symm : M' → M) f.target
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H_1 := chartAt H_1 x
c' : OpenPartialHomeomorph M' H_1 := chartAt H_1 ((↑f : M → M') x)
hx' : (↑c : M → H_1) x ∈ (↑c.symm : H_1 → M) ⁻¹' f.source
y : E
hy :
  ((↑I.symm : E → H_1) y ∈ c'.target ∧
      (↑c'.symm : H_1 → M') ((↑I.symm : E → H_1) y) ∈ f.target ∧
        (↑f.symm : M' → M) ((↑c'.symm : H_1 → M') ((↑I.symm : E → H_1) y)) ∈ c.source) ∧
    y ∈ range (↑I : H_1 → E)
H :
  ContinuousWithinAt (↑f.symm : M' → M) (f.symm ≫ₕ c).source ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y) ∧
    ContDiffWithinAt 𝕜 n
      ((↑(extChartAt I x) : M → E) ∘ (↑f.symm : M' → M) ∘ (↑(extChartAt I ((↑f : M → M') x)).symm : E → M'))
      ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') ⁻¹' (f.symm ≫ₕ c).source ∩ range (↑I : H_1 → E))
      ((↑(extChartAt I ((↑f : M → M') x)) : M' → E) ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y))
hy' : (↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y ∈ c'.source
hy'' : (↑f.symm : M' → M) ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y) ∈ c.source
⊢ ContDiffWithinAt 𝕜 n
    ((↑(extChartAt I x) : M → E) ∘ (↑f.symm : M' → M) ∘ (↑(extChartAt I ((↑f : M → M') x)).symm : E → M'))
    ((↑I.symm : E → H_1) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').target ∩ range (↑I : H_1 → E))
    ((↑(extChartAt I ((↑f : M → M') x)) : M' → E) ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y))

Tactic:
H.2.mono _

Premises used: And.right, ContDiffWithinAt.mono
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I : ModelWithCorners 𝕜 E H_1
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H_1 M
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H_1 M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h₁ : ContMDiffOn I I n (↑f : M → M') f.source
h₂ : ContMDiffOn I I n (↑f.symm : M' → M) f.target
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H_1 := chartAt H_1 x
c' : OpenPartialHomeomorph M' H_1 := chartAt H_1 ((↑f : M → M') x)
hx' : (↑c : M → H_1) x ∈ (↑c.symm : H_1 → M) ⁻¹' f.source
y : E
hy :
  ((↑I.symm : E → H_1) y ∈ c'.target ∧
      (↑c'.symm : H_1 → M') ((↑I.symm : E → H_1) y) ∈ f.target ∧
        (↑f.symm : M' → M) ((↑c'.symm : H_1 → M') ((↑I.symm : E → H_1) y)) ∈ c.source) ∧
    y ∈ range (↑I : H_1 → E)
H :
  ContinuousWithinAt (↑f.symm : M' → M) (f.symm ≫ₕ c).source ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y) ∧
    ContDiffWithinAt 𝕜 n
      ((↑(extChartAt I x) : M → E) ∘ (↑f.symm : M' → M) ∘ (↑(extChartAt I ((↑f : M → M') x)).symm : E → M'))
      ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') ⁻¹' (f.symm ≫ₕ c).source ∩ range (↑I : H_1 → E))
      ((↑(extChartAt I ((↑f : M → M') x)) : M' → E) ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y))
hy' : (↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y ∈ c'.source
hy'' : (↑f.symm : M' → M) ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y) ∈ c.source
h : y = (↑(extChartAt I ((↑f : M → M') x)) : M' → E) ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y)
mpr :
  (↑I.symm : E → H_1) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').target ∩ range (↑I : H_1 → E) ⊆
    (↑(extChartAt I ((↑f : M → M') x)).symm : E → M') ⁻¹' (f.symm ≫ₕ c).source ∩ range (↑I : H_1 → E)
⊢ ContDiffWithinAt 𝕜 n ((↑I : H_1 → E) ∘ (↑((c.symm ≫ₕ f) ≫ₕ c').symm : H_1 → H_1) ∘ (↑I.symm : E → H_1))
    ((↑I.symm : E → H_1) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').target ∩ range (↑I : H_1 → E)) y

Tactic:
convert! H.2.mono _

Premises used: And.right, ContDiffWithinAt.mono
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I : ModelWithCorners 𝕜 E H_1
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H_1 M
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H_1 M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h₁ : ContMDiffOn I I n (↑f : M → M') f.source
h₂ : ContMDiffOn I I n (↑f.symm : M' → M) f.target
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H_1 := chartAt H_1 x
c' : OpenPartialHomeomorph M' H_1 := chartAt H_1 ((↑f : M → M') x)
hx' : (↑c : M → H_1) x ∈ (↑c.symm : H_1 → M) ⁻¹' f.source
y : E
hy :
  ((↑I.symm : E → H_1) y ∈ c'.target ∧
      (↑c'.symm : H_1 → M') ((↑I.symm : E → H_1) y) ∈ f.target ∧
        (↑f.symm : M' → M) ((↑c'.symm : H_1 → M') ((↑I.symm : E → H_1) y)) ∈ c.source) ∧
    y ∈ range (↑I : H_1 → E)
H :
  ContinuousWithinAt (↑f.symm : M' → M) (f.symm ≫ₕ c).source ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y) ∧
    ContDiffWithinAt 𝕜 n
      ((↑(extChartAt I x) : M → E) ∘ (↑f.symm : M' → M) ∘ (↑(extChartAt I ((↑f : M → M') x)).symm : E → M'))
      ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') ⁻¹' (f.symm ≫ₕ c).source ∩ range (↑I : H_1 → E))
      ((↑(extChartAt I ((↑f : M → M') x)) : M' → E) ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y))
hy' : (↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y ∈ c'.source
hy'' : (↑f.symm : M' → M) ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y) ∈ c.source
⊢ y = (↑(extChartAt I ((↑f : M → M') x)) : M' → E) ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y)

Tactic:
simp only [c', hy, mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
H_1 : Type u_3
inst_3 : TopologicalSpace H_1
I : ModelWithCorners 𝕜 E H_1
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : ChartedSpace H_1 M
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H_1 M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h₁ : ContMDiffOn I I n (↑f : M → M') f.source
h₂ : ContMDiffOn I I n (↑f.symm : M' → M) f.target
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H_1 := chartAt H_1 x
c' : OpenPartialHomeomorph M' H_1 := chartAt H_1 ((↑f : M → M') x)
hx' : (↑c : M → H_1) x ∈ (↑c.symm : H_1 → M) ⁻¹' f.source
y : E
hy :
  ((↑I.symm : E → H_1) y ∈ c'.target ∧
      (↑c'.symm : H_1 → M') ((↑I.symm : E → H_1) y) ∈ f.target ∧
        (↑f.symm : M' → M) ((↑c'.symm : H_1 → M') ((↑I.symm : E → H_1) y)) ∈ c.source) ∧
    y ∈ range (↑I : H_1 → E)
H :
  ContinuousWithinAt (↑f.symm : M' → M) (f.symm ≫ₕ c).source ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y) ∧
    ContDiffWithinAt 𝕜 n
      ((↑(extChartAt I x) : M → E) ∘ (↑f.symm : M' → M) ∘ (↑(extChartAt I ((↑f : M → M') x)).symm : E → M'))
      ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') ⁻¹' (f.symm ≫ₕ c).source ∩ range (↑I : H_1 → E))
      ((↑(extChartAt I ((↑f : M → M') x)) : M' → E) ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y))
hy' : (↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y ∈ c'.source
hy'' : (↑f.symm : M' → M) ((↑(extChartAt I ((↑f : M → M') x)).symm : E → M') y) ∈ c.source
mpr :
  (↑I.symm : E → H_1) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H_1 ((↑f : M → M') x))).target ∩
        ((↑I.symm : E → H_1) ⁻¹'
            (↑(OpenPartialHomeomorph.symm (chartAt H_1 ((↑f : M → M') x))) : H_1 → M') ⁻¹' f.target ∩
          (↑I.symm : E → H_1) ⁻¹'
            (↑(OpenPartialHomeomorph.symm (chartAt H_1 ((↑f : M → M') x))) : H_1 → M') ⁻¹'
              (↑f.symm : M' → M) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H_1 x)).source) ∩
      range (↑I : H_1 → E) ⊆
    (↑(OpenPartialHomeomorph.symm (chartAt H_1 ((↑f : M → M') x))) : H_1 → M') ∘ (↑I.symm : E → H_1) ⁻¹' f.target ∩
        (↑(OpenPartialHomeomorph.symm (chartAt H_1 ((↑f : M → M') x))) : H_1 → M') ∘ (↑I.symm : E → H_1) ⁻¹'
          (↑f.symm : M' → M) ⁻¹' (OpenPartialHomeomorph.toPartialEquiv (chartAt H_1 x)).source ∩
      range (↑I : H_1 → E)
⊢ (↑I.symm : E → H_1) ⁻¹' ((c.symm ≫ₕ f) ≫ₕ c').target ∩ range (↑I : H_1 → E) ⊆
    (↑(extChartAt I ((↑f : M → M') x)).symm : E → M') ⁻¹' (f.symm ≫ₕ c).source ∩ range (↑I : H_1 → E)

Tactic:
dsimp [c, c']
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h₁ : ContMDiffOn I I n (↑f : M → M') f.source
h₂ : ContMDiffOn I I n (↑f.symm : M' → M) f.target
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hx' : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source
mpr :
  EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source ∩
      (c.target ∩ (↑c.symm : H → M) ⁻¹' f.source ∩ (↑f : M → M') ∘ (↑c.symm : H → M) ⁻¹' c'.source))
⊢ EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) (↑((c.symm ≫ₕ f) ≫ₕ c').toPartialEquiv : H → H)
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source ∩ ((c.symm ≫ₕ f) ≫ₕ c').source)

Tactic:
simp only [mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h₁ : ContMDiffOn I I n (↑f : M → M') f.source
h₂ : ContMDiffOn I I n (↑f.symm : M' → M) f.target
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hx' : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source
⊢ EqOn ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M)) ((↑c' : M' → H) ∘ (↑f : M → M') ∘ (↑c.symm : H → M))
    ((↑(OpenPartialHomeomorph.symm (chartAt H x)) : H → M) ⁻¹' f.source ∩
      (c.target ∩ (↑c.symm : H → M) ⁻¹' f.source ∩ (↑f : M → M') ∘ (↑c.symm : H → M) ⁻¹' c'.source))

Tactic:
apply eqOn_refl

Premises used: Set.eqOn_refl
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
n : ℕ∞ω
inst_6 : IsManifold I n M
M' : Type u_5
inst_7 : TopologicalSpace M'
inst_8 : ChartedSpace H M'
IsM' : IsManifold I n M'
f : OpenPartialHomeomorph M M'
h₁ : ContMDiffOn I I n (↑f : M → M') f.source
h₂ : ContMDiffOn I I n (↑f.symm : M' → M) f.target
x : M
hx : x ∈ f.source
c : OpenPartialHomeomorph M H := chartAt H x
c' : OpenPartialHomeomorph M' H := chartAt H ((↑f : M → M') x)
hx' : (↑c : M → H) x ∈ (↑c.symm : H → M) ⁻¹' f.source
⊢ (↑(chartAt H x) : M → H) x ∈ ((c.symm ≫ₕ f) ≫ₕ c').source

Tactic:
simp only [c, c', hx', mfld_simps]
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
F : Type u_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_7
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold J n N
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
y : M
hφ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) φ
hψ : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (maximalAtlas J n N) ψ
hy : y ∈ φ.source
hgy : f y ∈ ψ.source
hmaps : MapsTo f s ψ.source
rw :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
      ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y) ↔
    ContinuousWithinAt f s y ∧
      ContDiffWithinAt 𝕜 n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
        ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
      ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y) ↔
    ContMDiffWithinAt I J n f s y

Tactic:
rw [contMDiffWithinAt_iff_of_mem_maximalAtlas hφ hψ hy hgy]

Premises used: contMDiffWithinAt_iff_of_mem_maximalAtlas
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
F : Type u_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_7
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold J n N
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
y : M
hφ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) φ
hψ : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (maximalAtlas J n N) ψ
hy : y ∈ φ.source
hgy : f y ∈ ψ.source
hmaps : MapsTo f s ψ.source
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
      ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y) ↔
    ContinuousWithinAt f s y ∧
      ContDiffWithinAt 𝕜 n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
        ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)

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

Premises used: And.intro, Iff.intro
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
F : Type u_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_7
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold J n N
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
y : M
hφ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) φ
hψ : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (maximalAtlas J n N) ψ
hy : y ∈ φ.source
hgy : f y ∈ ψ.source
hmaps : MapsTo f s ψ.source
refine_1 :
  ∀
    (h :
      ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
        ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)),
    ContinuousWithinAt f s y
refine_2 :
  ∀
    (h :
      ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
        ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)),
    ContDiffWithinAt 𝕜 n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
      ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)
refine_3 :
  ∀
    (h :
      ContinuousWithinAt f s y ∧
        ContDiffWithinAt 𝕜 n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
          ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)),
    ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
      ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
      ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y) ↔
    ContinuousWithinAt f s y ∧
      ContDiffWithinAt 𝕜 n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
        ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ ?_⟩
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
F : Type u_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_7
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold J n N
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
y : M
hφ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) φ
hψ : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (maximalAtlas J n N) ψ
hy : y ∈ φ.source
hgy : f y ∈ ψ.source
hmaps : MapsTo f s ψ.source
h :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
    ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)
refine_1 :
  ContinuousWithinAt ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
    ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)
⊢ ContinuousWithinAt f s y

Tactic:
rw [← φ.continuousWithinAt_writtenInExtend_iff (I := I) (I' := J) hy hgy hmaps]

Premises used: OpenPartialHomeomorph.continuousWithinAt_writtenInExtend_iff
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
F : Type u_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_7
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold J n N
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
y : M
hφ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) φ
hψ : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (maximalAtlas J n N) ψ
hy : y ∈ φ.source
hgy : f y ∈ ψ.source
hmaps : MapsTo f s ψ.source
h :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
    ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)
⊢ ContinuousWithinAt ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
    ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)

Tactic:
h.continuousWithinAt

Premises used: ContMDiffWithinAt.continuousWithinAt
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
F : Type u_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_7
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold J n N
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
y : M
hφ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) φ
hψ : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (maximalAtlas J n N) ψ
hy : y ∈ φ.source
hgy : f y ∈ ψ.source
hmaps : MapsTo f s ψ.source
h :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
    ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)
⊢ ContinuousWithinAt ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
    ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)

Tactic:
exact h.continuousWithinAt

Premises used: ContMDiffWithinAt.continuousWithinAt
-- Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas
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
F : Type u_6
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
G : Type u_7
inst_8 : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst_9 : TopologicalSpace N
inst_10 : ChartedSpace G N
n : ℕ∞ω
inst_11 : IsManifold I n M
inst_12 : IsManifold J n N
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
y : M
hφ : Membership.mem (γ := Set (OpenPartialHomeomorph M H)) (maximalAtlas I n M) φ
hψ : Membership.mem (γ := Set (OpenPartialHomeomorph N G)) (maximalAtlas J n N) ψ
hy : y ∈ φ.source
hgy : f y ∈ ψ.source
hmaps : MapsTo f s ψ.source
h refine_2 refine_2₁ refine_2₂ refine_2₃ :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
    ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)
⊢ ContDiffWithinAt 𝕜 n ((↑(ψ.extend J) : N → F) ∘ f ∘ (↑(φ.extend I).symm : E → M))
    ((↑(φ.extend I).symm : E → M) ⁻¹' s ∩ range (↑I : H → E)) ((↑(φ.extend I) : M → E) y)

Tactic:
rwa [← contMDiffWithinAt_iff_contDiffWithinAt]

Premises used: contMDiffWithinAt_iff_contDiffWithinAt