-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem contDiffWithinAt_pi :
    ContDiffWithinAt 𝕜 n Φ s x ↔ ∀ i, ContDiffWithinAt 𝕜 n (fun x => Φ x i) s x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
x : E
n : WithTop ℕ∞
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
h : ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => Φ x i) s x
⊢ ContDiffWithinAt 𝕜 n Φ s x

Tactic:
match n with
| ω =>
  choose u hux p hp h'p using h
  refine ⟨⋂ i, u i, Filter.iInter_mem.2 hux, _,
    hasFTaylorSeriesUpToOn_pi.2 fun i => (hp i).mono <| iInter_subset _ _, fun m ↦ ?_⟩
  set L : (∀ i, E[×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E[×m]→L[𝕜] ∀ i, F' i :=
    ContinuousMultilinearMap.piₗᵢ _ _
  change AnalyticOn 𝕜 (fun x ↦ L (fun i ↦ p i x m)) (⋂ i, u i)
  apply (L.analyticOnNhd univ).comp_analyticOn ?_ (mapsTo_univ _ _)
  exact AnalyticOn.pi (fun i ↦ (h'p i m).mono (iInter_subset _ _))
| (n : ℕ∞) =>
  intro m hm
  choose u hux p hp using fun i => h i m hm
  exact ⟨⋂ i, u i, Filter.iInter_mem.2 hux, _,
    hasFTaylorSeriesUpToOn_pi.2 fun i => (hp i).mono <| iInter_subset _ _⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
x : E
n : WithTop ℕ∞
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
u : ι → Set E
hux : ∀ (i : ι), u i ∈ 𝓝[insert x s] x
p : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
hp : ∀ (i : ι), HasFTaylorSeriesUpToOn ω (fun x => Φ x i) (p i) (u i)
h'p : ∀ (i : ι) (i_1 : ℕ), AnalyticOn 𝕜 (fun x => p i x i_1) (u i)
m : ℕ
L : ((i : ι) → ContinuousMultilinearMap 𝕜 (fun i => E) (F' i)) ≃ₗᵢ[𝕜]
  ContinuousMultilinearMap 𝕜 (fun i => E) ((i : ι) → F' i) :=
  ContinuousMultilinearMap.piₗᵢ 𝕜 fun i => E
⊢ AnalyticOn 𝕜 (fun x i => p i x m) (⋂ i, u i)

Tactic:
exact AnalyticOn.pi (fun i ↦ (h'p i m).mono (iInter_subset _ _))

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
x : E
n : WithTop ℕ∞
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
u : ι → Set E
hux : ∀ (i : ι), u i ∈ 𝓝[insert x s] x
p : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
hp : ∀ (i : ι), HasFTaylorSeriesUpToOn ω (fun x => Φ x i) (p i) (u i)
h'p : ∀ (i : ι) (i_1 : ℕ), AnalyticOn 𝕜 (fun x => p i x i_1) (u i)
m : ℕ
L : ((i : ι) → ContinuousMultilinearMap 𝕜 (fun i => E) (F' i)) ≃ₗᵢ[𝕜]
  ContinuousMultilinearMap 𝕜 (fun i => E) ((i : ι) → F' i) :=
  ContinuousMultilinearMap.piₗᵢ 𝕜 fun i => E
⊢ AnalyticOn 𝕜 (fun x => ContinuousMultilinearMap.pi fun i => p i x m) (⋂ i, u i)

Tactic:
change AnalyticOn 𝕜 (fun x ↦ L (fun i ↦ p i x m)) (⋂ i, u i)

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
x : E
n : WithTop ℕ∞
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
u : ι → Set E
hux : ∀ (i : ι), u i ∈ 𝓝[insert x s] x
p : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
hp : ∀ (i : ι), HasFTaylorSeriesUpToOn ω (fun x => Φ x i) (p i) (u i)
h'p : ∀ (i : ι) (i_1 : ℕ), AnalyticOn 𝕜 (fun x => p i x i_1) (u i)
m : ℕ
L : ((i : ι) → ContinuousMultilinearMap 𝕜 (fun i => E) (F' i)) ≃ₗᵢ[𝕜]
  ContinuousMultilinearMap 𝕜 (fun i => E) ((i : ι) → F' i) :=
  ContinuousMultilinearMap.piₗᵢ 𝕜 fun i => E
⊢ AnalyticOn 𝕜 (fun x => L fun i => p i x m) (⋂ i, u i)

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
x : E
n✝ : WithTop ℕ∞
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
n : ℕ∞
h : ∀ (i : ι), ContDiffWithinAt 𝕜 (↑n) (fun x => Φ x i) s x
⊢ ContDiffWithinAt 𝕜 (↑n) Φ s x

Tactic:
intro m hm

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
x : E
n✝ : WithTop ℕ∞
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
n : ℕ∞
h : ∀ (i : ι), ContDiffWithinAt 𝕜 (↑n) (fun x => Φ x i) s x
m : ℕ
hm : ↑m ≤ n
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) Φ p u

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
x : E
n : WithTop ℕ∞
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
u : ι → Set E
hux : ∀ (i : ι), u i ∈ 𝓝[insert x s] x
p : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
hp : ∀ (i : ι), HasFTaylorSeriesUpToOn ω (fun x => Φ x i) (p i) (u i)
h'p : ∀ (i : ι) (i_1 : ℕ), AnalyticOn 𝕜 (fun x => p i x i_1) (u i)
m : ℕ
⊢ AnalyticOn 𝕜 (fun x => ContinuousMultilinearMap.pi fun i => p i x m) (⋂ i, u i)

Tactic:
set L : (∀ i, E[×m]→L[𝕜] F' i) ≃ₗᵢ[𝕜] E[×m]→L[𝕜] ∀ i, F' i :=
  ContinuousMultilinearMap.piₗᵢ _ _

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
x : E
n : WithTop ℕ∞
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
u : ι → Set E
hux : ∀ (i : ι), u i ∈ 𝓝[insert x s] x
p : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
hp : ∀ (i : ι), HasFTaylorSeriesUpToOn ω (fun x => Φ x i) (p i) (u i)
h'p : ∀ (i : ι) (i_1 : ℕ), AnalyticOn 𝕜 (fun x => p i x i_1) (u i)
m : ℕ
L : ((i : ι) → ContinuousMultilinearMap 𝕜 (fun i => E) (F' i)) ≃ₗᵢ[𝕜]
  ContinuousMultilinearMap 𝕜 (fun i => E) ((i : ι) → F' i) :=
  ContinuousMultilinearMap.piₗᵢ 𝕜 fun i => E
⊢ AnalyticOn 𝕜 (fun x => ContinuousMultilinearMap.pi fun i => p i x m) (⋂ i, u i)

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
x : E
n✝ : WithTop ℕ∞
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
Φ : E → (i : ι) → F' i
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
n : ℕ∞
h : ∀ (i : ι), ContDiffWithinAt 𝕜 (↑n) (fun x => Φ x i) s x
m : ℕ
hm : ↑m ≤ n
u : ι → Set E
hux : ∀ (i : ι), u i ∈ 𝓝[insert x s] x
p : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
hp : ∀ (i : ι), HasFTaylorSeriesUpToOn (↑m) (fun x => Φ x i) (p i) (u i)
⊢ ∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) Φ p u

Tactic:
exact ⟨⋂ i, u i, Filter.iInter_mem.2 hux, _,
  hasFTaylorSeriesUpToOn_pi.2 fun i => (hp i).mono <| iInter_subset _ _⟩

Result:
no goals