-- 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:
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

Tactic:
change (p (g x) 0 fun _ : Fin 0 => g 0) = p (g x) 0 0

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) fun x => g 0) = (p (g x) 0) 0

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) fun x => g 0) = (p (g x) 0) 0

Tactic:
rw [ContinuousLinearMap.map_zero]

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) fun x => 0) = (p (g x) 0) 0

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 ⁻¹' s, ((p (g x) 0).compContinuousLinearMap fun x => g).curry0 = (f ∘ ⇑g) x

Tactic:
intro x hx

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 = (f ∘ ⇑g) x

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
hA : ∀ (m : ℕ), IsBoundedLinearMap 𝕜 (A m)
⊢ HasFTaylorSeriesUpToOn n (f ∘ ⇑g) (fun x k => (p (g x) k).compContinuousLinearMap fun x => g) (⇑g ⁻¹' s)

Tactic:
constructor

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 ⁻¹' s, ((p (g x) 0).compContinuousLinearMap fun x => g).curry0 = (f ∘ ⇑g) x

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

case cont
𝕜 : 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 → ContinuousOn (fun x => (p (g x) m).compContinuousLinearMap fun x => g) (⇑g ⁻¹' s)