Module: Mathlib.Geometry.Manifold.ContMDiff.Atlas

Goal state before:
pp: case refine_1
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_7
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
y : M
hφ : φ ∈ maximalAtlas I n M
hψ : ψ ∈ maximalAtlas J n N
hy : y ∈ φ.source
hgy : f y ∈ ψ.source
hmaps : MapsTo f s ψ.source
h :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (↑(φ.extend I).symm ⁻¹' s ∩ range ↑I)
    (↑(φ.extend I) y)
⊢ ContinuousWithinAt f s y

pp: case refine_2
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_7
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
y : M
hφ : φ ∈ maximalAtlas I n M
hψ : ψ ∈ maximalAtlas J n N
hy : y ∈ φ.source
hgy : f y ∈ ψ.source
hmaps : MapsTo f s ψ.source
h :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (↑(φ.extend I).symm ⁻¹' s ∩ range ↑I)
    (↑(φ.extend I) y)
⊢ ContDiffWithinAt 𝕜 n (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (↑(φ.extend I).symm ⁻¹' s ∩ range ↑I) (↑(φ.extend I) y)

pp: case refine_3
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_7
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
y : M
hφ : φ ∈ maximalAtlas I n M
hψ : ψ ∈ maximalAtlas J n N
hy : y ∈ φ.source
hgy : f y ∈ ψ.source
hmaps : MapsTo f s ψ.source
h :
  ContinuousWithinAt f s y ∧
    ContDiffWithinAt 𝕜 n (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (↑(φ.extend I).symm ⁻¹' s ∩ range ↑I)
      (↑(φ.extend I) y)
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (↑(φ.extend I).symm ⁻¹' s ∩ range ↑I)
    (↑(φ.extend I) y)

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

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_7
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
y : M
hφ : φ ∈ maximalAtlas I n M
hψ : ψ ∈ maximalAtlas J n N
hy : y ∈ φ.source
hgy : f y ∈ ψ.source
hmaps : MapsTo f s ψ.source
h :
  ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (↑(φ.extend I).symm ⁻¹' s ∩ range ↑I)
    (↑(φ.extend I) y)
⊢ ContDiffWithinAt 𝕜 n (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (↑(φ.extend I).symm ⁻¹' s ∩ range ↑I) (↑(φ.extend I) y)

case refine_3
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
F : Type u_6
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
G : Type u_7
inst✝² : TopologicalSpace G
J : ModelWithCorners 𝕜 F G
N : Type u_8
inst✝¹ : TopologicalSpace N
inst✝ : ChartedSpace G N
n : ℕ∞ω
f : M → N
s : Set M
φ : OpenPartialHomeomorph M H
ψ : OpenPartialHomeomorph N G
y : M
hφ : φ ∈ maximalAtlas I n M
hψ : ψ ∈ maximalAtlas J n N
hy : y ∈ φ.source
hgy : f y ∈ ψ.source
hmaps : MapsTo f s ψ.source
h :
  ContinuousWithinAt f s y ∧
    ContDiffWithinAt 𝕜 n (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (↑(φ.extend I).symm ⁻¹' s ∩ range ↑I)
      (↑(φ.extend I) y)
⊢ ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, F) n (↑(ψ.extend J) ∘ f ∘ ↑(φ.extend I).symm) (↑(φ.extend I).symm ⁻¹' s ∩ range ↑I)
    (↑(φ.extend I) y)