-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem ContDiffWithinAt.restrict_scalars (h : ContDiffWithinAt 𝕜' n f s x) :
    ContDiffWithinAt 𝕜 n f s x

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
𝕜' : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
u : Set E
u_mem : u ∈ 𝓝[insert x s] x
p' : E → FormalMultilinearSeries 𝕜' E F
hp' : HasFTaylorSeriesUpToOn ω f p' u
Hp' : ∀ (i : ℕ), AnalyticOn 𝕜' (fun x => p' x i) u
⊢ ContDiffWithinAt 𝕜 ω f s x

Tactic:
refine ⟨u, u_mem, _, hp'.restrictScalars _, fun i ↦ ?_⟩

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n : WithTop ℕ∞
𝕜' : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
u : Set E
u_mem : u ∈ 𝓝[insert x s] x
p' : E → FormalMultilinearSeries 𝕜' E F
hp' : HasFTaylorSeriesUpToOn ω f p' u
Hp' : ∀ (i : ℕ), AnalyticOn 𝕜' (fun x => p' x i) u
i : ℕ
⊢ AnalyticOn 𝕜 (fun x => FormalMultilinearSeries.restrictScalars 𝕜 (p' x) i) u

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n✝ : WithTop ℕ∞
𝕜' : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
n : ℕ∞
h : ContDiffWithinAt 𝕜' (↑n) f s x
m : ℕ
hm : ↑m ≤ n
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u

Tactic:
rcases h m hm with ⟨u, u_mem, p', hp'⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n✝ : WithTop ℕ∞
𝕜' : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
n : ℕ∞
h : ContDiffWithinAt 𝕜' (↑n) f s x
m : ℕ
hm : ↑m ≤ n
u : Set E
u_mem : u ∈ 𝓝[insert x s] x
p' : E → FormalMultilinearSeries 𝕜' E F
hp' : HasFTaylorSeriesUpToOn (↑m) f p' u
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u

Proof state:
case intro.intro.intro
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
F : Type uF
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
n✝ : WithTop ℕ∞
𝕜' : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
n : ℕ∞
h : ContDiffWithinAt 𝕜' (↑n) f s x
m : ℕ
hm : ↑m ≤ n
u : Set E
u_mem : u ∈ 𝓝[insert x s] x
p' : E → FormalMultilinearSeries 𝕜' E F
hp' : HasFTaylorSeriesUpToOn (↑m) f p' u
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u

Tactic:
exact ⟨u, u_mem, _, hp'.restrictScalars _⟩

Result:
no goals