-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
theorem HasFTaylorSeriesUpToOn.comp {n : WithTop ℕ∞} {g : F → G} {f : E → F}
    (hg : HasFTaylorSeriesUpToOn n g q t) (hf : HasFTaylorSeriesUpToOn n f p s) (h : MapsTo f s t) :
    HasFTaylorSeriesUpToOn n (g ∘ f) (fun x ↦ (q (f x)).taylorComp (p x)) s

Proof state:
case zero_eq
𝕜 : 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
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
⊢ ∀ x ∈ s, ((q (f x)).taylorComp (p x) 0).curry0 = (g ∘ f) x

Tactic:
intro x hx

Result:
case zero_eq
𝕜 : 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
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
x : E
hx : x ∈ s
⊢ ((q (f x)).taylorComp (p x) 0).curry0 = (g ∘ f) x

Proof state:
case cont
𝕜 : 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
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
⊢ ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => (q (f x)).taylorComp (p x) m) s

Tactic:
intro m hm

Result:
case cont
𝕜 : 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
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : ↑m ≤ n
⊢ ContinuousOn (fun x => (q (f x)).taylorComp (p x) m) 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
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : ↑m ≤ n
c : OrderedFinpartition m
x✝ : c ∈ Finset.univ
B : ContinuousMultilinearMap 𝕜 (fun i => F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜 (fun i => ContinuousMultilinearMap 𝕜 (fun i => E) F)
    (ContinuousMultilinearMap 𝕜 (fun i => E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
this : ↑c.length ≤ ↑m
⊢ ContinuousOn (fun x => q (f x) c.length) s

Tactic:
exact (hg.cont c.length (this.trans hm)).comp hf.continuousOn 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
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
c : OrderedFinpartition m
B : ContinuousMultilinearMap 𝕜 (fun i => F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜 (fun i => ContinuousMultilinearMap 𝕜 (fun i => E) F)
    (ContinuousMultilinearMap 𝕜 (fun i => E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
cm : ↑c.length ≤ ↑m
⊢ HasFDerivWithinAt (fun y => (B (q (f y) c.length)) fun i => p y (c.partSize i))
    (∑ i : Option (Fin c.length), ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x

Tactic:
have cp i : (c.partSize i : WithTop ℕ∞) ≤ m := by
  exact_mod_cast OrderedFinpartition.partSize_le c i

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
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
c : OrderedFinpartition m
B : ContinuousMultilinearMap 𝕜 (fun i => F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜 (fun i => ContinuousMultilinearMap 𝕜 (fun i => E) F)
    (ContinuousMultilinearMap 𝕜 (fun i => E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
cm : ↑c.length ≤ ↑m
cp : ∀ (i : Fin c.length), ↑(c.partSize i) ≤ ↑m
⊢ HasFDerivWithinAt (fun y => (B (q (f y) c.length)) fun i => p y (c.partSize i))
    (∑ i : Option (Fin c.length), ((q (f x)).compAlongOrderedFinpartition (p x) (c.extend i)).curryLeft) s x

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
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : ↑m ≤ n
c : OrderedFinpartition m
x✝ : c ∈ Finset.univ
B : ContinuousMultilinearMap 𝕜 (fun i => F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜 (fun i => ContinuousMultilinearMap 𝕜 (fun i => E) F)
    (ContinuousMultilinearMap 𝕜 (fun i => E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
⊢ ContinuousOn (fun a => (q (f a)).compAlongOrderedFinpartition (p a) c) s

Tactic:
change ContinuousOn
  ((fun p ↦ B p.1 p.2) ∘ (fun x ↦ (q (f x) c.length, fun i ↦ p x (c.partSize i)))) s

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
n : WithTop ℕ∞
g : F → G
f : E → F
hg : HasFTaylorSeriesUpToOn n g q t
hf : HasFTaylorSeriesUpToOn n f p s
h : MapsTo f s t
m : ℕ
hm : ↑m ≤ n
c : OrderedFinpartition m
x✝ : c ∈ Finset.univ
B : ContinuousMultilinearMap 𝕜 (fun i => F) G →L[𝕜]
  ContinuousMultilinearMap 𝕜 (fun i => ContinuousMultilinearMap 𝕜 (fun i => E) F)
    (ContinuousMultilinearMap 𝕜 (fun i => E) G) :=
  compAlongOrderedFinpartitionL 𝕜 E F G c
⊢ ContinuousOn ((fun p => (B p.1) p.2) ∘ fun x => (q (f x) c.length, fun i => p x (c.partSize i))) s