awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
g : E → F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
B : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G := ContinuousLinearMap.flip (ContinuousLinearMap.apply 𝕜 G)
hB : ‖B‖ ≤ 1
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ (f y : (a : F) → G) (g y)) s x) ≤
    ∑ i ∈ Finset.range (n + 1),
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 i f s x) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (n - i)) ↦ E) F)
          (iteratedFDerivWithin 𝕜 (n - i) g s x)

Tactic:
B.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one hf hg hs hx hn hB

Premises used: ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
g : E → F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
B : (F →L[𝕜] G) →L[𝕜] F →L[𝕜] G := ContinuousLinearMap.flip (ContinuousLinearMap.apply 𝕜 G)
hB : ‖B‖ ≤ 1
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ (f y : (a : F) → G) (g y)) s x) ≤
    ∑ i ∈ Finset.range (n + 1),
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 i f s x) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (n - i)) ↦ E) F)
          (iteratedFDerivWithin 𝕜 (n - i) g s x)

Tactic:
exact B.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one hf hg hs hx hn hB

Premises used: ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
g : E → F
N : ℕ∞ω
n : ℕ
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : E
hn : (↑n : ℕ∞ω) ≤ N
simp :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ (f y : (a : F) → G) (g y)) univ x) ≤
    ∑ x_1 ∈ Finset.range (n + 1),
      (↑(n.choose x_1) : ℝ) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin x_1) ↦ E) (F →L[𝕜] G))
            (iteratedFDerivWithin 𝕜 x_1 f univ x) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (n - x_1)) ↦ E) F)
          (iteratedFDerivWithin 𝕜 (n - x_1) g univ x)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDeriv 𝕜 n (fun (y : E) ↦ (f y : (a : F) → G) (g y)) x) ≤
    ∑ i ∈ Finset.range (n + 1),
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) (iteratedFDeriv 𝕜 i f x) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (n - i)) ↦ E) F)
          (iteratedFDeriv 𝕜 (n - i) g x)

Tactic:
simp only [← iteratedFDerivWithin_univ]

Premises used: iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
g : E → F
N : ℕ∞ω
n : ℕ
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : E
hn : (↑n : ℕ∞ω) ≤ N
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ (f y : (a : F) → G) (g y)) univ x) ≤
    ∑ x_1 ∈ Finset.range (n + 1),
      (↑(n.choose x_1) : ℝ) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin x_1) ↦ E) (F →L[𝕜] G))
            (iteratedFDerivWithin 𝕜 x_1 f univ x) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (n - x_1)) ↦ E) F)
          (iteratedFDerivWithin 𝕜 (n - x_1) g univ x)

Tactic:
norm_iteratedFDerivWithin_clm_apply hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ
    (Set.mem_univ x) hn

Premises used: norm_iteratedFDerivWithin_clm_apply, ContDiff.contDiffOn, uniqueDiffOn_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
g : E → F
N : ℕ∞ω
n : ℕ
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : E
hn : (↑n : ℕ∞ω) ≤ N
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ (f y : (a : F) → G) (g y)) univ x) ≤
    ∑ x_1 ∈ Finset.range (n + 1),
      (↑(n.choose x_1) : ℝ) *
          norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin x_1) ↦ E) (F →L[𝕜] G))
            (iteratedFDerivWithin 𝕜 x_1 f univ x) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (n - x_1)) ↦ E) F)
          (iteratedFDerivWithin 𝕜 (n - x_1) g univ x)

Tactic:
exact norm_iteratedFDerivWithin_clm_apply hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ
    (Set.mem_univ x) hn

Premises used: norm_iteratedFDerivWithin_clm_apply, ContDiff.contDiffOn, uniqueDiffOn_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
L : F →L[𝕜] G
f : E → F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (L.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E) (iteratedFDerivWithin 𝕜 n f s x)) ≤
    ‖L‖ *
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)

Tactic:
have h := L.norm_compContinuousMultilinearMap_le (iteratedFDerivWithin 𝕜 n f s x)
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
L : F →L[𝕜] G
f : E → F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
h :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (L.compContinuousMultilinearMap (M₁ := fun (i : Fin n) ↦ E) (iteratedFDerivWithin 𝕜 n f s x)) ≤
    ‖L‖ *
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (h :
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
          (iteratedFDerivWithin 𝕜 n ((⇑L : (a : F) → G) ∘ f) s x) ≤
        ‖L‖ *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
            (iteratedFDerivWithin 𝕜 n f s x)),
    norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
        (iteratedFDerivWithin 𝕜 n ((⇑L : (a : F) → G) ∘ f) s x) ≤
      ‖L‖ *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n ((⇑L : (a : F) → G) ∘ f) s x) ≤
    ‖L‖ *
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDerivWithin 𝕜 n f s x)

Tactic:
rwa [← L.iteratedFDerivWithin_comp_left hf hs hx hn] at h

Premises used: ContinuousLinearMap.iteratedFDerivWithin_comp_left
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
L : F →L[𝕜] G
f : E → F
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffAt 𝕜 N f x
hn : (↑n : ℕ∞ω) ≤ N
simp :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n ((⇑L : (a : F) → G) ∘ f) univ x) ≤
    ‖L‖ *
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
        (iteratedFDerivWithin 𝕜 n f univ x)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDeriv 𝕜 n ((⇑L : (a : F) → G) ∘ f) x) ≤
    ‖L‖ * norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F) (iteratedFDeriv 𝕜 n f x)

Tactic:
simp only [← iteratedFDerivWithin_univ]

Premises used: iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
L : F →L[𝕜] G
f : E → F
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffAt 𝕜 N f x
hn : (↑n : ℕ∞ω) ≤ N
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n ((⇑L : (a : F) → G) ∘ f) univ x) ≤
    ‖L‖ *
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
        (iteratedFDerivWithin 𝕜 n f univ x)

Tactic:
L.norm_iteratedFDerivWithin_comp_left hf.contDiffWithinAt uniqueDiffOn_univ (Set.mem_univ x)
    hn

Premises used: ContinuousLinearMap.norm_iteratedFDerivWithin_comp_left, uniqueDiffOn_univ, Set.mem_univ, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
L : F →L[𝕜] G
f : E → F
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffAt 𝕜 N f x
hn : (↑n : ℕ∞ω) ≤ N
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n ((⇑L : (a : F) → G) ∘ f) univ x) ≤
    ‖L‖ *
      norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
        (iteratedFDerivWithin 𝕜 n f univ x)

Tactic:
exact L.norm_iteratedFDerivWithin_comp_left hf.contDiffWithinAt uniqueDiffOn_univ (Set.mem_univ x)
    hn

Premises used: ContinuousLinearMap.norm_iteratedFDerivWithin_comp_left, uniqueDiffOn_univ, Set.mem_univ, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
apply :
  norm (E := (F →L[𝕜] G) →L[𝕜] G)
        ((ContinuousLinearMap.apply 𝕜 G : (a : F) → (F →L[𝕜] G) →L[𝕜] G) c : (F →L[𝕜] G) →L[𝕜] G) *
      norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 n f s x) ≤
    ‖c‖ * norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 n f s x)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ (f y : (a : F) → G) c) s x) ≤
    ‖c‖ * norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 n f s x)

Tactic:
apply ((ContinuousLinearMap.apply 𝕜 G c).norm_iteratedFDerivWithin_comp_left hf hs hx hn).trans

Premises used: ContinuousLinearMap.norm_iteratedFDerivWithin_comp_left, ContinuousLinearMap.apply, LE.le.trans, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
hbc :
  norm (E := (F →L[𝕜] G) →L[𝕜] G)
      ((ContinuousLinearMap.apply 𝕜 G : (a : F) → (F →L[𝕜] G) →L[𝕜] G) c : (F →L[𝕜] G) →L[𝕜] G) ≤
    ‖c‖
⊢ norm (E := (F →L[𝕜] G) →L[𝕜] G)
        ((ContinuousLinearMap.apply 𝕜 G : (a : F) → (F →L[𝕜] G) →L[𝕜] G) c : (F →L[𝕜] G) →L[𝕜] G) *
      norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 n f s x) ≤
    ‖c‖ * norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 n f s x)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
⊢ norm (E := (F →L[𝕜] G) →L[𝕜] G)
      ((ContinuousLinearMap.apply 𝕜 G : (a : F) → (F →L[𝕜] G) →L[𝕜] G) c : (F →L[𝕜] G) →L[𝕜] G) ≤
    ‖c‖

Tactic:
(ContinuousLinearMap.apply 𝕜 G c).opNorm_le_bound (norm_nonneg _) fun f => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound, ContinuousLinearMap.apply, DFunLike.coe, norm_nonneg
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
hbc :
  ∀ (f : F →L[𝕜] G),
    norm.{uG} (E := G)
        ((((ContinuousLinearMap.apply 𝕜 G : (a : F) → (F →L[𝕜] G) →L[𝕜] G) c : (F →L[𝕜] G) →L[𝕜] G) :
              (a : F →L[𝕜] G) → G)
            f :
          G) ≤
      ‖c‖ * ‖f‖
⊢ norm (E := (F →L[𝕜] G) →L[𝕜] G)
      ((ContinuousLinearMap.apply 𝕜 G : (a : F) → (F →L[𝕜] G) →L[𝕜] G) c : (F →L[𝕜] G) →L[𝕜] G) ≤
    ‖c‖

Tactic:
refine (ContinuousLinearMap.apply 𝕜 G c).opNorm_le_bound (norm_nonneg _) fun f => ?_

Premises used: ContinuousLinearMap.opNorm_le_bound, ContinuousLinearMap.apply, DFunLike.coe, norm_nonneg
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f_1 : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffWithinAt 𝕜 N f_1 s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
f : F →L[𝕜] G
hbc : norm.{uG} (E := G) ((f : (a : F) → G) c : G) ≤ ‖f‖ * ‖c‖
⊢ norm.{uG} (E := G)
      ((((ContinuousLinearMap.apply 𝕜 G : (a : F) → (F →L[𝕜] G) →L[𝕜] G) c : (F →L[𝕜] G) →L[𝕜] G) : (a : F →L[𝕜] G) → G)
          f :
        G) ≤
    ‖c‖ * ‖f‖

Tactic:
rw [ContinuousLinearMap.apply_apply, mul_comm]

Premises used: mul_comm, ContinuousLinearMap.apply_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f_1 : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffWithinAt 𝕜 N f_1 s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
f : F →L[𝕜] G
⊢ norm.{uG} (E := G) ((f : (a : F) → G) c : G) ≤ ‖f‖ * ‖c‖

Tactic:
f.le_opNorm c

Premises used: ContinuousLinearMap.le_opNorm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f_1 : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffWithinAt 𝕜 N f_1 s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : (↑n : ℕ∞ω) ≤ N
f : F →L[𝕜] G
⊢ norm.{uG} (E := G) ((f : (a : F) → G) c : G) ≤ ‖f‖ * ‖c‖

Tactic:
exact f.le_opNorm c

Premises used: ContinuousLinearMap.le_opNorm
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
c : F
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffAt 𝕜 N f x
hn : (↑n : ℕ∞ω) ≤ N
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ (f y : (a : F) → G) c) univ x) ≤
    ‖c‖ * norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 n f univ x)

Tactic:
norm_iteratedFDerivWithin_clm_apply_const hf.contDiffWithinAt uniqueDiffOn_univ
    (Set.mem_univ x) hn

Premises used: norm_iteratedFDerivWithin_clm_apply_const, uniqueDiffOn_univ, Set.mem_univ, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type uF
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type uG
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
c : F
x : E
N : ℕ∞ω
n : ℕ
hf : ContDiffAt 𝕜 N f x
hn : (↑n : ℕ∞ω) ≤ N
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uG} 𝕜 (fun (i : Fin n) ↦ E) G)
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ (f y : (a : F) → G) c) univ x) ≤
    ‖c‖ * norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin n) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 n f univ x)

Tactic:
exact norm_iteratedFDerivWithin_clm_apply_const hf.contDiffWithinAt uniqueDiffOn_univ
    (Set.mem_univ x) hn

Premises used: norm_iteratedFDerivWithin_clm_apply_const, uniqueDiffOn_univ, Set.mem_univ, ContDiffAt.contDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.CPolynomial
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ∞ω
t : Set E := {x : E | CPolynomialAt 𝕜 f x}
suffices : ContDiffOn 𝕜 n f t
⊢ ContDiffOn 𝕜 n f s

Tactic:
suffices ContDiffOn 𝕜 n f t from this.mono h
-- Module: Mathlib.Analysis.Calculus.ContDiff.CPolynomial
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ∞ω
t : Set E := {x : E | CPolynomialAt 𝕜 f x}
this : AnalyticOnNhd 𝕜 f t
⊢ IsOpen t

Tactic:
have t_open : IsOpen t := isOpen_cpolynomialAt 𝕜 f
-- Module: Mathlib.Analysis.Calculus.ContDiff.CPolynomial
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ∞ω
t : Set E := {x : E | CPolynomialAt 𝕜 f x}
this : AnalyticOnNhd 𝕜 f t
t_open : IsOpen t
⊢ ContDiffOn 𝕜 n f t

Tactic:
AnalyticOnNhd.contDiffOn this t_open.uniqueDiffOn

Premises used: AnalyticOnNhd.contDiffOn, IsOpen.uniqueDiffOn
-- Module: Mathlib.Analysis.Calculus.ContDiff.CPolynomial
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ∞ω
t : Set E := {x : E | CPolynomialAt 𝕜 f x}
this : AnalyticOnNhd 𝕜 f t
t_open : IsOpen t
⊢ ContDiffOn 𝕜 n f t

Tactic:
exact AnalyticOnNhd.contDiffOn this t_open.uniqueDiffOn

Premises used: AnalyticOnNhd.contDiffOn, IsOpen.uniqueDiffOn
-- Module: Mathlib.Analysis.Calculus.ContDiff.CPolynomial
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ∞ω
t : Set E := {x : E | CPolynomialAt 𝕜 f x}
suffices : AnalyticOnNhd 𝕜 f t
⊢ ContDiffOn 𝕜 n f t

Tactic:
suffices AnalyticOnNhd 𝕜 f t by
    have t_open : IsOpen t := isOpen_cpolynomialAt 𝕜 f
    exact AnalyticOnNhd.contDiffOn this t_open.uniqueDiffOn
-- Module: Mathlib.Analysis.Calculus.ContDiff.CPolynomial
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ∞ω
t : Set E := {x : E | CPolynomialAt 𝕜 f x}
⊢ CPolynomialOn 𝕜 f t

Tactic:
have H : CPolynomialOn 𝕜 f t := fun _x hx ↦ hx
-- Module: Mathlib.Analysis.Calculus.ContDiff.CPolynomial
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ∞ω
t : Set E := {x : E | CPolynomialAt 𝕜 f x}
H : CPolynomialOn 𝕜 f t
⊢ AnalyticOnNhd 𝕜 f t

Tactic:
H.analyticOnNhd

Premises used: CPolynomialOn.analyticOnNhd
-- Module: Mathlib.Analysis.Calculus.ContDiff.CPolynomial
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : CPolynomialOn 𝕜 f s
n : ℕ∞ω
t : Set E := {x : E | CPolynomialAt 𝕜 f x}
H : CPolynomialOn 𝕜 f t
⊢ AnalyticOnNhd 𝕜 f t

Tactic:
exact H.analyticOnNhd

Premises used: CPolynomialOn.analyticOnNhd
-- Module: Mathlib.Analysis.Calculus.ContDiff.CPolynomial
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
h : CPolynomialAt 𝕜 f x
n : ℕ∞ω
⊢ ContDiffAt 𝕜 n f x

Tactic:
let ⟨_, hs, hf⟩ := h.exists_mem_nhds_cpolynomialOn
  hf.contDiffOn.contDiffAt hs

Premises used: ContDiffAt, _private.0.CPolynomialAt.contDiffAt.match_1, CPolynomialOn.contDiffOn, CPolynomialAt.exists_mem_nhds_cpolynomialOn, ContDiffOn.contDiffAt