-- Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
theorem norm_iteratedFDerivWithin_clm_apply_const {f : E → F →L[𝕜] G} {c : F} {s : Set E} {x : E}
    {N : WithTop ℕ∞} {n : ℕ} (hf : ContDiffWithinAt 𝕜 N f s x) (hs : UniqueDiffOn 𝕜 s)
    (hx : x ∈ s) (hn : n ≤ N) :
    ‖iteratedFDerivWithin 𝕜 n (fun y : E => (f y) c) s x‖ ≤
      ‖c‖ * ‖iteratedFDerivWithin 𝕜 n f s 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
f✝ : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : WithTop ℕ∞
n : ℕ
hf : ContDiffWithinAt 𝕜 N f✝ s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : ↑n ≤ N
g : (F →L[𝕜] G) →L[𝕜] G := (ContinuousLinearMap.apply 𝕜 G) c
h : ‖iteratedFDerivWithin 𝕜 n (⇑g ∘ f✝) s x‖ ≤ ‖g‖ * ‖iteratedFDerivWithin 𝕜 n f✝ s x‖
f : F →L[𝕜] G
⊢ ‖f c‖ ≤ ‖f‖ * ‖c‖

Tactic:
exact f.le_opNorm c

Result:
no goals

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
f : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : WithTop ℕ∞
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : ↑n ≤ N
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y => (f y) c) s x‖ ≤ ‖c‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖

Tactic:
let g : (F →L[𝕜] G) →L[𝕜] G := ContinuousLinearMap.apply 𝕜 G c

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
f : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : WithTop ℕ∞
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : ↑n ≤ N
g : (F →L[𝕜] G) →L[𝕜] G := (ContinuousLinearMap.apply 𝕜 G) c
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y => (f y) c) s x‖ ≤ ‖c‖ * ‖iteratedFDerivWithin 𝕜 n f s 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
f : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : WithTop ℕ∞
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : ↑n ≤ N
g : (F →L[𝕜] G) →L[𝕜] G := (ContinuousLinearMap.apply 𝕜 G) c
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y => (f y) c) s x‖ ≤ ‖c‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖

Tactic:
have h := g.norm_compContinuousMultilinearMap_le (iteratedFDerivWithin 𝕜 n f s x)

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
f : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : WithTop ℕ∞
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : ↑n ≤ N
g : (F →L[𝕜] G) →L[𝕜] G := (ContinuousLinearMap.apply 𝕜 G) c
h : ‖g.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 n f s x)‖ ≤ ‖g‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y => (f y) c) s x‖ ≤ ‖c‖ * ‖iteratedFDerivWithin 𝕜 n f s 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
f : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : WithTop ℕ∞
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : ↑n ≤ N
g : (F →L[𝕜] G) →L[𝕜] G := (ContinuousLinearMap.apply 𝕜 G) c
h : ‖g.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 n f s x)‖ ≤ ‖g‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y => (f y) c) s x‖ ≤ ‖c‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖

Tactic:
rw [← g.iteratedFDerivWithin_comp_left hf hs hx hn] at h

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
f : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : WithTop ℕ∞
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : ↑n ≤ N
g : (F →L[𝕜] G) →L[𝕜] G := (ContinuousLinearMap.apply 𝕜 G) c
h : ‖iteratedFDerivWithin 𝕜 n (⇑g ∘ f) s x‖ ≤ ‖g‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y => (f y) c) s x‖ ≤ ‖c‖ * ‖iteratedFDerivWithin 𝕜 n f s 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
f : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : WithTop ℕ∞
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : ↑n ≤ N
g : (F →L[𝕜] G) →L[𝕜] G := (ContinuousLinearMap.apply 𝕜 G) c
h : ‖iteratedFDerivWithin 𝕜 n (⇑g ∘ f) s x‖ ≤ ‖g‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖
⊢ ‖g‖ ≤ ‖c‖

Tactic:
refine g.opNorm_le_bound (norm_nonneg _) fun f => ?_

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
f✝ : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : WithTop ℕ∞
n : ℕ
hf : ContDiffWithinAt 𝕜 N f✝ s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : ↑n ≤ N
g : (F →L[𝕜] G) →L[𝕜] G := (ContinuousLinearMap.apply 𝕜 G) c
h : ‖iteratedFDerivWithin 𝕜 n (⇑g ∘ f✝) s x‖ ≤ ‖g‖ * ‖iteratedFDerivWithin 𝕜 n f✝ s x‖
f : F →L[𝕜] G
⊢ ‖g f‖ ≤ ‖c‖ * ‖f‖

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
f✝ : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : WithTop ℕ∞
n : ℕ
hf : ContDiffWithinAt 𝕜 N f✝ s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : ↑n ≤ N
g : (F →L[𝕜] G) →L[𝕜] G := (ContinuousLinearMap.apply 𝕜 G) c
h : ‖iteratedFDerivWithin 𝕜 n (⇑g ∘ f✝) s x‖ ≤ ‖g‖ * ‖iteratedFDerivWithin 𝕜 n f✝ s x‖
f : F →L[𝕜] G
⊢ ‖g f‖ ≤ ‖c‖ * ‖f‖

Tactic:
rw [ContinuousLinearMap.apply_apply, mul_comm]

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
f✝ : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : WithTop ℕ∞
n : ℕ
hf : ContDiffWithinAt 𝕜 N f✝ s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : ↑n ≤ N
g : (F →L[𝕜] G) →L[𝕜] G := (ContinuousLinearMap.apply 𝕜 G) c
h : ‖iteratedFDerivWithin 𝕜 n (⇑g ∘ f✝) s x‖ ≤ ‖g‖ * ‖iteratedFDerivWithin 𝕜 n f✝ s x‖
f : F →L[𝕜] G
⊢ ‖f c‖ ≤ ‖f‖ * ‖c‖