awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
F : Type uF
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
G : Type uG
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
s : Set D
x : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D
Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E
Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F
Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G
isoD : Du ≃ₗᵢ[𝕜] D
isoE : Eu ≃ₗᵢ[𝕜] E
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : Du → Eu := (⇑isoE.symm : (a : E) → Eu) ∘ f ∘ (⇑isoD : (a : Du) → D)
gu : Du → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ g ∘ (⇑isoD : (a : Du) → D)
Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G :=
  flip
    (comp (σ₂₃ := RingHom.id 𝕜) (B ∘SL (↑(↑isoE : Eu ≃L[𝕜] E) : Eu →L[𝕜] E)).flip (↑(↑isoF : Fu ≃L[𝕜] F) : Fu →L[𝕜] F))
Bu : Eu →L[𝕜] Fu →L[𝕜] Gu :=
  (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
            (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
          ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
            (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
        (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
      (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
    Bu₀
hBu :
  Bu =
    (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
              (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
            ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
              (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
          (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
        (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
      Bu₀
Bu_eq :
  Eq (α := (y : Du) → Gu) (fun (y : Du) ↦ (((Bu : (a : Eu) → Fu →L[𝕜] Gu) (fu y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (gu y))
    (Function.comp (β := G) (⇑isoG.symm : (a : G) → Gu)
      ((fun (y : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) ∘ (⇑isoD : (a : Du) → D)))
Bu_le : ‖Bu‖ ≤ ‖B‖
su : Set Du := (⇑isoD : (a : Du) → D) ⁻¹' s
hsu : UniqueDiffOn 𝕜 su
xu : Du := (isoD.symm : (a : D) → Du) x
hxu : xu ∈ su
xu_x : (isoD : (a : Du) → D) xu = x
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu su
hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu su
i : ℕ
hx₁ hx₂ hx₃ hx₄ :
  ∀ (hx : Membership.mem (α := D) s ((isoD : (a : Du) → D) xu : D)) (hxu : xu ∈ su)
    (xu_x : (isoD : (a : Du) → D) xu = x) (hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu su) (hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu su)
    (i : ℕ), Membership.mem (α := D) s ((isoD : (a : Du) → D) xu : D)
⊢ Membership.mem (α := D) s ((isoD : (a : Du) → D) xu : D)

Tactic:
rwa [← xu_x] at hx
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
F : Type uF
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
G : Type uG
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
s : Set D
x : D
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
Du : Type (max uD uE uF uG) := ULift.{max uE uF uG, uD} D
Eu : Type (max uD uE uF uG) := ULift.{max uD uF uG, uE} E
Fu : Type (max uD uE uF uG) := ULift.{max uD uE uG, uF} F
Gu : Type (max uD uE uF uG) := ULift.{max uD uE uF, uG} G
isoD : Du ≃ₗᵢ[𝕜] D
isoE : Eu ≃ₗᵢ[𝕜] E
isoF : Fu ≃ₗᵢ[𝕜] F
isoG : Gu ≃ₗᵢ[𝕜] G
fu : Du → Eu := (⇑isoE.symm : (a : E) → Eu) ∘ f ∘ (⇑isoD : (a : Du) → D)
gu : Du → Fu := (⇑isoF.symm : (a : F) → Fu) ∘ g ∘ (⇑isoD : (a : Du) → D)
Bu₀ : Eu →L[𝕜] Fu →L[𝕜] G :=
  flip
    (comp (σ₂₃ := RingHom.id 𝕜) (B ∘SL (↑(↑isoE : Eu ≃L[𝕜] E) : Eu →L[𝕜] E)).flip (↑(↑isoF : Fu ≃L[𝕜] F) : Fu →L[𝕜] F))
Bu : Eu →L[𝕜] Fu →L[𝕜] Gu :=
  (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
            (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
          ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
            (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
        (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
      (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
    Bu₀
hBu :
  Bu =
    (((compL 𝕜 Eu (Fu →L[𝕜] G) (Fu →L[𝕜] Gu) :
              (a : (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu) → (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu)
            ((compL 𝕜 Fu G Gu : (a : G →L[𝕜] Gu) → (Fu →L[𝕜] G) →L[𝕜] Fu →L[𝕜] Gu)
              (↑(↑isoG.symm : G ≃L[𝕜] Gu) : G →L[𝕜] Gu)) :
          (Eu →L[𝕜] Fu →L[𝕜] G) →L[𝕜] Eu →L[𝕜] Fu →L[𝕜] Gu) :
        (a : Eu →L[𝕜] Fu →L[𝕜] G) → Eu →L[𝕜] Fu →L[𝕜] Gu)
      Bu₀
Bu_eq :
  Eq (α := (y : Du) → Gu) (fun (y : Du) ↦ (((Bu : (a : Eu) → Fu →L[𝕜] Gu) (fu y) : Fu →L[𝕜] Gu) : (a : Fu) → Gu) (gu y))
    (Function.comp (β := G) (⇑isoG.symm : (a : G) → Gu)
      ((fun (y : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) ∘ (⇑isoD : (a : Du) → D)))
Bu_le : ‖Bu‖ ≤ ‖B‖
su : Set Du := (⇑isoD : (a : Du) → D) ⁻¹' s
hsu : UniqueDiffOn 𝕜 su
xu : Du := (isoD.symm : (a : D) → Du) x
hxu : xu ∈ su
xu_x : (isoD : (a : Du) → D) xu = x
hfu : ContDiffOn 𝕜 (↑n : ℕ∞ω) fu su
hgu : ContDiffOn 𝕜 (↑n : ℕ∞ω) gu su
⊢ ∀ (i : ℕ),
    norm (E := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ Du) Eu) (iteratedFDerivWithin 𝕜 i fu su xu) =
      norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uE} 𝕜 (fun (i : Fin i) ↦ D) E) (iteratedFDerivWithin 𝕜 i f s x)

Tactic:
have Nfu : ∀ i, ‖iteratedFDerivWithin 𝕜 i fu su xu‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖ := by
    intro i
    rw [LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left _ _ hsu hxu]
    rw [LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_right _ _ hs, xu_x]
    rwa [← xu_x] at hx
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
D : Type uD
inst_1 : NormedAddCommGroup D
inst_2 : NormedSpace 𝕜 D
E : Type uE
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
F : Type uF
inst_5 : NormedAddCommGroup F
inst_6 : NormedSpace 𝕜 F
G : Type uG
inst_7 : NormedAddCommGroup G
inst_8 : NormedSpace 𝕜 G
B : E →L[𝕜] F →L[𝕜] G
f : D → E
g : D → F
N : ℕ∞ω
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : D
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
simp_rw :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uG} 𝕜 (fun (i : Fin n) ↦ D) G)
      (iteratedFDerivWithin 𝕜 n (fun (y : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) univ
        x) ≤
    ‖B‖ *
      ∑ x_1 ∈ Finset.range (n + 1),
        (↑(n.choose x_1) : ℝ) *
            norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uE} 𝕜 (fun (i : Fin x_1) ↦ D) E)
              (iteratedFDerivWithin 𝕜 x_1 f univ x) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uF} 𝕜 (fun (i : Fin (n - x_1)) ↦ D) F)
            (iteratedFDerivWithin 𝕜 (n - x_1) g univ x)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uG} 𝕜 (fun (i : Fin n) ↦ D) G)
      (iteratedFDeriv 𝕜 n (fun (y : D) ↦ (((B : (a : E) → F →L[𝕜] G) (f y) : F →L[𝕜] G) : (a : F) → G) (g y)) x) ≤
    ‖B‖ *
      ∑ i ∈ Finset.range (n + 1),
        (↑(n.choose i) : ℝ) *
            norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uE} 𝕜 (fun (i : Fin i) ↦ D) E) (iteratedFDeriv 𝕜 i f x) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uD, uF} 𝕜 (fun (i : Fin (n - i)) ↦ D) F)
            (iteratedFDeriv 𝕜 (n - i) g x)

Tactic:
simp_rw [← iteratedFDerivWithin_univ]

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

Tactic:
B.norm_iteratedFDerivWithin_le_of_bilinear hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ
    (mem_univ x) hn

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

Tactic:
exact B.norm_iteratedFDerivWithin_le_of_bilinear hf.contDiffOn hg.contDiffOn uniqueDiffOn_univ
    (mem_univ x) hn

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

Tactic:
apply (B.norm_iteratedFDerivWithin_le_of_bilinear hf hg hs hx hn).trans

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

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

Tactic:
exact mul_le_of_le_one_left (by positivity) hB

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

Tactic:
simp_rw [← iteratedFDerivWithin_univ]

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

Tactic:
B.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one hf.contDiffOn hg.contDiffOn
    uniqueDiffOn_univ (mem_univ x) hn hB

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

Tactic:
exact B.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one hf.contDiffOn hg.contDiffOn
    uniqueDiffOn_univ (mem_univ x) hn hB

Premises used: ContDiff.contDiffOn, uniqueDiffOn_univ, Set.mem_univ, 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
s : Set E
𝕜' : Type u_2
inst_5 : NormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' F
inst_8 : IsScalarTower 𝕜 𝕜' F
f : E → 𝕜'
g : E → F
N : ℕ∞ω
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ f y • g y) s x) ≤
    ∑ i ∈ Finset.range (n + 1),
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_2} 𝕜 (fun (i : Fin i) ↦ E) 𝕜')
            (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:
(ContinuousLinearMap.lsmul 𝕜 𝕜' :
    𝕜' →L[𝕜] F →L[𝕜] F).norm_iteratedFDerivWithin_le_of_bilinear_of_le_one
      hf hg hs hx hn ContinuousLinearMap.opNorm_lsmul_le

Premises used: ContinuousLinearMap.opNorm_lsmul_le, ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_of_le_one, ContinuousLinearMap.lsmul
-- 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
𝕜' : Type u_2
inst_5 : NormedField 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : NormedSpace 𝕜' F
inst_8 : IsScalarTower 𝕜 𝕜' F
f : E → 𝕜'
g : E → F
N : ℕ∞ω
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : E
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin n) ↦ E) F)
      (iteratedFDeriv 𝕜 n (fun (y : E) ↦ f y • g y) x) ≤
    ∑ i ∈ Finset.range (n + 1),
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_2} 𝕜 (fun (i : Fin i) ↦ E) 𝕜') (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:
(ContinuousLinearMap.lsmul 𝕜 𝕜' : 𝕜' →L[𝕜] F →L[𝕜] F).norm_iteratedFDeriv_le_of_bilinear_of_le_one
    hf hg x hn ContinuousLinearMap.opNorm_lsmul_le

Premises used: ContinuousLinearMap.norm_iteratedFDeriv_le_of_bilinear_of_le_one, ContinuousLinearMap.opNorm_lsmul_le, ContinuousLinearMap.lsmul
-- Module: Mathlib.Analysis.Calculus.ContDiff.Bounds
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type uE
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
A : Type u_3
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f g : E → A
N : ℕ∞ω
hf : ContDiffOn 𝕜 N f s
hg : ContDiffOn 𝕜 N g s
hs : UniqueDiffOn 𝕜 s
x : E
hx : x ∈ s
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_3} 𝕜 (fun (i : Fin n) ↦ E) A)
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ f y * g y) s x) ≤
    ∑ i ∈ Finset.range (n + 1),
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_3} 𝕜 (fun (i : Fin i) ↦ E) A)
            (iteratedFDerivWithin 𝕜 i f s x) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_3} 𝕜 (fun (i : Fin (n - i)) ↦ E) A)
          (iteratedFDerivWithin 𝕜 (n - i) g s x)

Tactic:
(ContinuousLinearMap.mul 𝕜 A :
    A →L[𝕜] A →L[𝕜] A).norm_iteratedFDerivWithin_le_of_bilinear_of_le_one
      hf hg hs hx hn (ContinuousLinearMap.opNorm_mul_le _ _)

Premises used: ContinuousLinearMap.opNorm_mul_le, ContinuousLinearMap.mul, 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
A : Type u_3
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
f g : E → A
N : ℕ∞ω
hf : ContDiff 𝕜 N f
hg : ContDiff 𝕜 N g
x : E
n : ℕ
hn : (↑n : ℕ∞ω) ≤ N
simp_rw :
  norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_3} 𝕜 (fun (i : Fin n) ↦ E) A)
      (iteratedFDerivWithin 𝕜 n (fun (y : E) ↦ f y * g y) univ x) ≤
    ∑ x_1 ∈ Finset.range (n + 1),
      (↑(n.choose x_1) : ℝ) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_3} 𝕜 (fun (i : Fin x_1) ↦ E) A)
            (iteratedFDerivWithin 𝕜 x_1 f univ x) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_3} 𝕜 (fun (i : Fin (n - x_1)) ↦ E) A)
          (iteratedFDerivWithin 𝕜 (n - x_1) g univ x)
⊢ norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_3} 𝕜 (fun (i : Fin n) ↦ E) A)
      (iteratedFDeriv 𝕜 n (fun (y : E) ↦ f y * g y) x) ≤
    ∑ i ∈ Finset.range (n + 1),
      (↑(n.choose i) : ℝ) *
          norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_3} 𝕜 (fun (i : Fin i) ↦ E) A) (iteratedFDeriv 𝕜 i f x) *
        norm (E := ContinuousMultilinearMap.{u_1, 0, uE, u_3} 𝕜 (fun (i : Fin (n - i)) ↦ E) A)
          (iteratedFDeriv 𝕜 (n - i) g x)

Tactic:
simp_rw [← iteratedFDerivWithin_univ]

Premises used: iteratedFDerivWithin_univ