𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type ?u.456792
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g✝ : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
x : G
g : G →L[𝕜] E
hf : ContDiffWithinAt 𝕜 n f s (↑g x)
m : ℕ
hm : ↑m ≤ n
⊢ ∃ u, u ∈ 𝓝[insert x (↑g ⁻¹' s)] x ∧ ∃ p, HasFTaylorSeriesUpToOn (↑m) (f ∘ ↑g) p u
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type ?u.456792
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g✝ : F → G
x✝ x₀ : E
c : F
b : E × F → G
m n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
x : G
g : G →L[𝕜] E
hf : ContDiffWithinAt 𝕜 n f s (↑g x)
⊢ ContDiffWithinAt 𝕜 n (f ∘ ↑g) (↑g ⁻¹' s) x
intro m hm
case intro.intro.intro
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type ?u.456792
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g✝ : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
x : G
g : G →L[𝕜] E
hf : ContDiffWithinAt 𝕜 n f s (↑g x)
m : ℕ
hm : ↑m ≤ n
u : Set E
hu : u ∈ 𝓝[insert (↑g x) s] ↑g x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m) f p u
⊢ ∃ u, u ∈ 𝓝[insert x (↑g ⁻¹' s)] x ∧ ∃ p, HasFTaylorSeriesUpToOn (↑m) (f ∘ ↑g) p u
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type ?u.456792
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u : Set E
f f₁ : E → F
g✝ : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n : ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
x : G
g : G →L[𝕜] E
hf : ContDiffWithinAt 𝕜 n f s (↑g x)
m : ℕ
hm : ↑m ≤ n
⊢ ∃ u, u ∈ 𝓝[insert x (↑g ⁻¹' s)] x ∧ ∃ p, HasFTaylorSeriesUpToOn (↑m) (f ∘ ↑g) p u
rcases hf m hm with ⟨u, hu, p, hp⟩
case intro.intro.intro
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type ?u.456792
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g✝ : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
x : G
g : G →L[𝕜] E
hf : ContDiffWithinAt 𝕜 n f s (↑g x)
m : ℕ
hm : ↑m ≤ n
u : Set E
hu : u ∈ 𝓝[insert (↑g x) s] ↑g x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m) f p u
⊢ ↑g ⁻¹' u ∈ 𝓝[insert x (↑g ⁻¹' s)] x
case intro.intro.intro
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type ?u.456792
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g✝ : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
x : G
g : G →L[𝕜] E
hf : ContDiffWithinAt 𝕜 n f s (↑g x)
m : ℕ
hm : ↑m ≤ n
u : Set E
hu : u ∈ 𝓝[insert (↑g x) s] ↑g x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m) f p u
⊢ ∃ u, u ∈ 𝓝[insert x (↑g ⁻¹' s)] x ∧ ∃ p, HasFTaylorSeriesUpToOn (↑m) (f ∘ ↑g) p u
refine ⟨g ⁻¹' u, ?_, _, hp.compContinuousLinearMap g⟩
case intro.intro.intro
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type ?u.456792
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g✝ : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
x : G
g : G →L[𝕜] E
hf : ContDiffWithinAt 𝕜 n f s (↑g x)
m : ℕ
hm : ↑m ≤ n
u : Set E
hu : u ∈ 𝓝[insert (↑g x) s] ↑g x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m) f p u
⊢ MapsTo (↑g) (insert x (↑g ⁻¹' s)) (insert (↑g x) s)
case intro.intro.intro
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type ?u.456792
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g✝ : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
x : G
g : G →L[𝕜] E
hf : ContDiffWithinAt 𝕜 n f s (↑g x)
m : ℕ
hm : ↑m ≤ n
u : Set E
hu : u ∈ 𝓝[insert (↑g x) s] ↑g x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m) f p u
⊢ ↑g ⁻¹' u ∈ 𝓝[insert x (↑g ⁻¹' s)] x
refine g.continuous.continuousWithinAt.tendsto_nhdsWithin ?_ hu
no goals
case intro.intro.intro
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
D : Type uD
inst✝⁹ : NormedAddCommGroup D
inst✝⁸ : NormedSpace 𝕜 D
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type uG
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
X : Type ?u.456792
inst✝¹ : NormedAddCommGroup X
inst✝ : NormedSpace 𝕜 X
s s₁ t u✝ : Set E
f f₁ : E → F
g✝ : F → G
x✝ x₀ : E
c : F
b : E × F → G
m✝ n : ℕ∞
p✝ : E → FormalMultilinearSeries 𝕜 E F
x : G
g : G →L[𝕜] E
hf : ContDiffWithinAt 𝕜 n f s (↑g x)
m : ℕ
hm : ↑m ≤ n
u : Set E
hu : u ∈ 𝓝[insert (↑g x) s] ↑g x
p : E → FormalMultilinearSeries 𝕜 E F
hp : HasFTaylorSeriesUpToOn (↑m) f p u
⊢ MapsTo (↑g) (insert x (↑g ⁻¹' s)) (insert (↑g x) s)
exact (mapsTo_singleton.2 <| mem_singleton _).union_union (mapsTo_preimage _ _)