-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem HasFTaylorSeriesUpToOn.compContinuousLinearMap
    (hf : HasFTaylorSeriesUpToOn n f p s) (g : G →L[𝕜] E) :
    HasFTaylorSeriesUpToOn n (f ∘ g) (fun x k => (p (g x) k).compContinuousLinearMap fun _ => g)
      (g ⁻¹' s)

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
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
s : Set E
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →L[𝕜] E
A : (m : ℕ) → ContinuousMultilinearMap 𝕜 (fun i => E) F → ContinuousMultilinearMap 𝕜 (fun i => G) F :=
  fun m h => h.compContinuousLinearMap fun x => g
⊢ HasFTaylorSeriesUpToOn n (f ∘ ⇑g) (fun x k => (p (g x) k).compContinuousLinearMap fun x => g) (⇑g ⁻¹' s)

Tactic:
have hA : ∀ m, IsBoundedLinearMap 𝕜 (A m) := fun m =>
  isBoundedLinearMap_continuousMultilinearMap_comp_linear g

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
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
s : Set E
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →L[𝕜] E
A : (m : ℕ) → ContinuousMultilinearMap 𝕜 (fun i => E) F → ContinuousMultilinearMap 𝕜 (fun i => G) F :=
  fun m h => h.compContinuousLinearMap fun x => g
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
⊢ HasFTaylorSeriesUpToOn n (f ∘ ⇑g) (fun x k => (p (g x) k).compContinuousLinearMap fun x => g) (⇑g ⁻¹' s)

Proof state:
case fderivWithin
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
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
s : Set E
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →L[𝕜] E
A : (m : ℕ) → ContinuousMultilinearMap 𝕜 (fun i => E) F → ContinuousMultilinearMap 𝕜 (fun i => G) F :=
  fun m h => h.compContinuousLinearMap fun x => g
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
⊢ ∀ (m : ℕ),
    ↑m < n →
      ∀ x ∈ ⇑g ⁻¹' s,
        HasFDerivWithinAt (fun x => (p (g x) m).compContinuousLinearMap fun x => g)
          ((p (g x) m.succ).compContinuousLinearMap fun x => g).curryLeft (⇑g ⁻¹' s) x

Tactic:
intro m hm x hx

Result:
case fderivWithin
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
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
s : Set E
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →L[𝕜] E
A : (m : ℕ) → ContinuousMultilinearMap 𝕜 (fun i => E) F → ContinuousMultilinearMap 𝕜 (fun i => G) F :=
  fun m h => h.compContinuousLinearMap fun x => g
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
m : ℕ
hm : ↑m < n
x : G
hx : x ∈ ⇑g ⁻¹' s
⊢ HasFDerivWithinAt (fun x => (p (g x) m).compContinuousLinearMap fun x => g)
    ((p (g x) m.succ).compContinuousLinearMap fun x => g).curryLeft (⇑g ⁻¹' s) x

Proof state:
case zero_eq
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
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
s : Set E
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →L[𝕜] E
A : (m : ℕ) → ContinuousMultilinearMap 𝕜 (fun i => E) F → ContinuousMultilinearMap 𝕜 (fun i => G) F :=
  fun m h => h.compContinuousLinearMap fun x => g
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
x : G
hx : x ∈ ⇑g ⁻¹' s
⊢ ((p (g x) 0).compContinuousLinearMap fun x => g).curry0 = (f ∘ ⇑g) x

Tactic:
simp only [(hf.zero_eq (g x) hx).symm, Function.comp_apply]

Result:
case zero_eq
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
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
s : Set E
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →L[𝕜] E
A : (m : ℕ) → ContinuousMultilinearMap 𝕜 (fun i => E) F → ContinuousMultilinearMap 𝕜 (fun i => G) F :=
  fun m h => h.compContinuousLinearMap fun x => g
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
x : G
hx : x ∈ ⇑g ⁻¹' s
⊢ ((p (g x) 0).compContinuousLinearMap fun x => g).curry0 = (p (g x) 0).curry0

Proof state:
case h.e'_12.h.h.h.H
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
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
s : Set E
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →L[𝕜] E
A : (m : ℕ) → ContinuousMultilinearMap 𝕜 (fun i => E) F → ContinuousMultilinearMap 𝕜 (fun i => G) F :=
  fun m h => h.compContinuousLinearMap fun x => g
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
m : ℕ
hm : ↑m < n
x : G
hx : x ∈ ⇑g ⁻¹' s
e_8✝ : ContinuousMultilinearMap.instAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝ : ContinuousMultilinearMap.instModule = NormedSpace.toModule
e_10✝ : ContinuousMultilinearMap.instTopologicalSpace = UniformSpace.toTopologicalSpace
y : G
v : Fin m → G
⊢ (((p (g x) m.succ).compContinuousLinearMap fun x => g).curryLeft y) v =
    ((⋯.toContinuousLinearMap.comp ((p (g x) m.succ).curryLeft.comp g)) y) v

Tactic:
change p (g x) (Nat.succ m) (g ∘ cons y v) = p (g x) m.succ (cons (g y) (g ∘ v))

Result:
case h.e'_12.h.h.h.H
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
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
s : Set E
f : E → F
n : WithTop ℕ∞
p : E → FormalMultilinearSeries 𝕜 E F
hf : HasFTaylorSeriesUpToOn n f p s
g : G →L[𝕜] E
A : (m : ℕ) → ContinuousMultilinearMap 𝕜 (fun i => E) F → ContinuousMultilinearMap 𝕜 (fun i => G) F :=
  fun m h => h.compContinuousLinearMap fun x => g
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
m : ℕ
hm : ↑m < n
x : G
hx : x ∈ ⇑g ⁻¹' s
e_8✝ : ContinuousMultilinearMap.instAddCommGroup = SeminormedAddCommGroup.toAddCommGroup
he✝ : ContinuousMultilinearMap.instModule = NormedSpace.toModule
e_10✝ : ContinuousMultilinearMap.instTopologicalSpace = UniformSpace.toTopologicalSpace
y : G
v : Fin m → G
⊢ (p (g x) m.succ) (⇑g ∘ cons y v) = (p (g x) m.succ) (cons (g y) (⇑g ∘ v))