-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
theorem analyticOn_taylorComp
    (hq : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x ↦ q x n) t)
    (hp : ∀ n, AnalyticOn 𝕜 (fun x ↦ p x n) s) {f : E → F}
    (hf : AnalyticOn 𝕜 f s) (h : MapsTo f s t) (n : ℕ) :
    AnalyticOn 𝕜 (fun x ↦ (q (f x)).taylorComp (p x) n) s

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
hq : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x => q x n) t
hp : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x => p x n) s
f : E → F
hf : AnalyticOn 𝕜 f s
h : MapsTo f s t
n : ℕ
c : OrderedFinpartition n
x✝ : c ∈ Finset.univ
B : ContinuousMultilinearMap 𝕜 (fun i => F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜 (fun i => ContinuousMultilinearMap 𝕜 (fun i => E) F)
    (ContinuousMultilinearMap 𝕜 (fun i => E) G) :=
  OrderedFinpartition.compAlongOrderedFinpartitionL 𝕜 E F G c
⊢ AnalyticOn 𝕜 (fun x => (q (f x) c.length, fun m => p x (c.partSize m))) s

Tactic:
apply AnalyticOn.prod

Result:
case hf
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
hq : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x => q x n) t
hp : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x => p x n) s
f : E → F
hf : AnalyticOn 𝕜 f s
h : MapsTo f s t
n : ℕ
c : OrderedFinpartition n
x✝ : c ∈ Finset.univ
B : ContinuousMultilinearMap 𝕜 (fun i => F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜 (fun i => ContinuousMultilinearMap 𝕜 (fun i => E) F)
    (ContinuousMultilinearMap 𝕜 (fun i => E) G) :=
  OrderedFinpartition.compAlongOrderedFinpartitionL 𝕜 E F G c
⊢ AnalyticOn 𝕜 (fun x => q (f x) c.length) s

case hg
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
hq : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x => q x n) t
hp : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x => p x n) s
f : E → F
hf : AnalyticOn 𝕜 f s
h : MapsTo f s t
n : ℕ
c : OrderedFinpartition n
x✝ : c ∈ Finset.univ
B : ContinuousMultilinearMap 𝕜 (fun i => F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜 (fun i => ContinuousMultilinearMap 𝕜 (fun i => E) F)
    (ContinuousMultilinearMap 𝕜 (fun i => E) G) :=
  OrderedFinpartition.compAlongOrderedFinpartitionL 𝕜 E F G c
⊢ AnalyticOn 𝕜 (fun x m => p x (c.partSize m)) s

Proof state:
case hf
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
hq : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x => q x n) t
hp : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x => p x n) s
f : E → F
hf : AnalyticOn 𝕜 f s
h : MapsTo f s t
n : ℕ
c : OrderedFinpartition n
x✝ : c ∈ Finset.univ
B : ContinuousMultilinearMap 𝕜 (fun i => F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜 (fun i => ContinuousMultilinearMap 𝕜 (fun i => E) F)
    (ContinuousMultilinearMap 𝕜 (fun i => E) G) :=
  OrderedFinpartition.compAlongOrderedFinpartitionL 𝕜 E F G c
⊢ AnalyticOn 𝕜 (fun x => q (f x) c.length) s

Tactic:
exact (hq c.length).comp hf h

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
hq : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x => q x n) t
hp : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x => p x n) s
f : E → F
hf : AnalyticOn 𝕜 f s
h : MapsTo f s t
n : ℕ
c : OrderedFinpartition n
x✝ : c ∈ Finset.univ
⊢ AnalyticOn 𝕜 (fun z => (q (f z)).compAlongOrderedFinpartition (p z) c) s

Tactic:
let B := c.compAlongOrderedFinpartitionL 𝕜 E F G

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
hq : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x => q x n) t
hp : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x => p x n) s
f : E → F
hf : AnalyticOn 𝕜 f s
h : MapsTo f s t
n : ℕ
c : OrderedFinpartition n
x✝ : c ∈ Finset.univ
B : ContinuousMultilinearMap 𝕜 (fun i => F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜 (fun i => ContinuousMultilinearMap 𝕜 (fun i => E) F)
    (ContinuousMultilinearMap 𝕜 (fun i => E) G) :=
  OrderedFinpartition.compAlongOrderedFinpartitionL 𝕜 E F G c
⊢ AnalyticOn 𝕜 (fun z => (q (f z)).compAlongOrderedFinpartition (p z) c) s

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
hq : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x => q x n) t
hp : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x => p x n) s
f : E → F
hf : AnalyticOn 𝕜 f s
h : MapsTo f s t
n : ℕ
c : OrderedFinpartition n
x✝ : c ∈ Finset.univ
B : ContinuousMultilinearMap 𝕜 (fun i => F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜 (fun i => ContinuousMultilinearMap 𝕜 (fun i => E) F)
    (ContinuousMultilinearMap 𝕜 (fun i => E) G) :=
  OrderedFinpartition.compAlongOrderedFinpartitionL 𝕜 E F G c
⊢ AnalyticOn 𝕜 ((fun p => (B p.1) p.2) ∘ fun x => (q (f x) c.length, fun m => p x (c.partSize m))) s

Tactic:
apply B.analyticOnNhd_uncurry_of_multilinear.comp_analyticOn ?_ (mapsTo_univ _ _)

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
t : Set F
q : F → FormalMultilinearSeries 𝕜 F G
p : E → FormalMultilinearSeries 𝕜 E F
hq : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x => q x n) t
hp : ∀ (n : ℕ), AnalyticOn 𝕜 (fun x => p x n) s
f : E → F
hf : AnalyticOn 𝕜 f s
h : MapsTo f s t
n : ℕ
c : OrderedFinpartition n
x✝ : c ∈ Finset.univ
B : ContinuousMultilinearMap 𝕜 (fun i => F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜 (fun i => ContinuousMultilinearMap 𝕜 (fun i => E) F)
    (ContinuousMultilinearMap 𝕜 (fun i => E) G) :=
  OrderedFinpartition.compAlongOrderedFinpartitionL 𝕜 E F G c
⊢ AnalyticOn 𝕜 (fun x => (q (f x) c.length, fun m => p x (c.partSize m))) s