awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
X : Type u_5
inst_7 : NormedAddCommGroup X
inst_8 : NormedSpace 𝕜 X
n : ℕ∞ω
g : X → F →L[𝕜] G
f : X → E →L[𝕜] F
x : X
hg : ContDiffAt 𝕜 n g x
hf : ContDiffAt 𝕜 n f x
⊢ ContDiffAt 𝕜 (F := E →L[𝕜] G) n (fun (x : X) ↦ g x ∘SL f x) x

Tactic:
(isBoundedBilinearMap_comp (E := E) (G := G)).contDiff.comp₂_contDiffAt hg hf

Premises used: IsBoundedBilinearMap.contDiff, ContDiff.comp₂_contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
X : Type u_5
inst_7 : NormedAddCommGroup X
inst_8 : NormedSpace 𝕜 X
n : ℕ∞ω
g : X → F →L[𝕜] G
f : X → E →L[𝕜] F
s : Set X
x : X
hg : ContDiffWithinAt 𝕜 n g s x
hf : ContDiffWithinAt 𝕜 n f s x
⊢ ContDiffWithinAt 𝕜 (F := E →L[𝕜] G) n (fun (x : X) ↦ g x ∘SL f x) s x

Tactic:
(isBoundedBilinearMap_comp (E := E) (G := G)).contDiff.comp₂_contDiffWithinAt hg hf

Premises used: ContDiff.comp₂_contDiffWithinAt, IsBoundedBilinearMap.contDiff
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
f : E → F →L[𝕜] G
g : E → F
hf : ContDiff 𝕜 n f
hg : ContDiff 𝕜 n g
⊢ ContDiff.{u_1, u_2, u_4} 𝕜 (F := G) n fun (x : E) ↦ (f x : (a : F) → G) (g x)

Tactic:
isBoundedBilinearMap_apply.contDiff.comp₂ hf hg

Premises used: IsBoundedBilinearMap.contDiff, ContDiff.comp₂
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
n : ℕ∞ω
f : E → F →L[𝕜] G
g : E → F
hf : ContDiffOn 𝕜 n f s
hg : ContDiffOn 𝕜 n g s
⊢ ContDiffOn.{u_1, u_2, u_4} 𝕜 (F := G) n (fun (x : E) ↦ (f x : (a : F) → G) (g x)) s

Tactic:
isBoundedBilinearMap_apply.contDiff.comp₂_contDiffOn hf hg

Premises used: IsBoundedBilinearMap.contDiff, ContDiff.comp₂_contDiffOn
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
n : ℕ∞ω
f : E → F →L[𝕜] G
g : E → F
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g x
⊢ ContDiffAt.{u_1, u_2, u_4} 𝕜 (F := G) n (fun (x : E) ↦ (f x : (a : F) → G) (g x)) x

Tactic:
isBoundedBilinearMap_apply.contDiff.comp₂_contDiffAt hf hg

Premises used: IsBoundedBilinearMap.contDiff, ContDiff.comp₂_contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x : E
n : ℕ∞ω
f : E → F →L[𝕜] G
g : E → F
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
⊢ ContDiffWithinAt.{u_1, u_2, u_4} 𝕜 (F := G) n (fun (x : E) ↦ (f x : (a : F) → G) (g x)) s x

Tactic:
isBoundedBilinearMap_apply.contDiff.comp₂_contDiffWithinAt hf hg

Premises used: ContDiff.comp₂_contDiffWithinAt, IsBoundedBilinearMap.contDiff
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
f : E → StrongDual 𝕜 F
g : E → G
hf : ContDiff 𝕜 n f
hg : ContDiff 𝕜 n g
⊢ ContDiff 𝕜 (F := F →L[𝕜] G) n fun (x : E) ↦ ContinuousLinearMap.smulRight (f x) (g x)

Tactic:
isBoundedBilinearMap_smulRight.contDiff.comp₂ (g := fun p => p.1.smulRight p.2) hf hg

Premises used: IsBoundedBilinearMap.contDiff, ContDiff.comp₂
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
n : ℕ∞ω
f : E → StrongDual 𝕜 F
g : E → G
hf : ContDiffOn 𝕜 n f s
hg : ContDiffOn 𝕜 n g s
⊢ ContDiffOn 𝕜 (F := F →L[𝕜] G) n (fun (x : E) ↦ ContinuousLinearMap.smulRight (f x) (g x)) s

Tactic:
(isBoundedBilinearMap_smulRight (E := F)).contDiff.comp₂_contDiffOn hf hg

Premises used: IsBoundedBilinearMap.contDiff, ContDiff.comp₂_contDiffOn
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
n : ℕ∞ω
f : E → StrongDual 𝕜 F
g : E → G
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g x
⊢ ContDiffAt 𝕜 (F := F →L[𝕜] G) n (fun (x : E) ↦ ContinuousLinearMap.smulRight (f x) (g x)) x

Tactic:
(isBoundedBilinearMap_smulRight (E := F)).contDiff.comp₂_contDiffAt hf hg

Premises used: IsBoundedBilinearMap.contDiff, ContDiff.comp₂_contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
s : Set E
x : E
n : ℕ∞ω
f : E → StrongDual 𝕜 F
g : E → G
hf : ContDiffWithinAt 𝕜 n f s x
hg : ContDiffWithinAt 𝕜 n g s x
⊢ ContDiffWithinAt 𝕜 (F := F →L[𝕜] G) n (fun (x : E) ↦ ContinuousLinearMap.smulRight (f x) (g x)) s x

Tactic:
(isBoundedBilinearMap_smulRight (E := F)).contDiff.comp₂_contDiffWithinAt hf hg

Premises used: ContDiff.comp₂_contDiffWithinAt, IsBoundedBilinearMap.contDiff
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
hi : (↑0 : ℕ∞ω) ≤ n
x : E
hx : x ∈ s
m : Fin 0 → E
⊢ Eq.{u_4 + 1} (α := G)
    ((iteratedFDerivWithin 𝕜 0 (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin 0) → E) → G) m : G)
    ((((iteratedFDerivWithin 𝕜 0 c s x : (a : (i : Fin 0) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ∀ (hi : (↑i : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin i → E},
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin i) → E) → G) m : G)
      ((((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
hi : (↑(i + 1) : ℕ∞ω) ≤ n
x : E
hx : x ∈ s
m : Fin (i + 1) → E
norm_cast : i < i + 1
⊢ LT.lt (α := ℕ∞ω) (↑i : ℕ∞ω) (↑(i + 1) : ℕ∞ω)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ∀ (hi : (↑i : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin i → E},
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin i) → E) → G) m : G)
      ((((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
hi : (↑(i + 1) : ℕ∞ω) ≤ n
x : E
hx : x ∈ s
m : Fin (i + 1) → E
⊢ i < i + 1

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ∀ (hi : (↑i : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin i → E},
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin i) → E) → G) m : G)
      ((((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
hi : (↑(i + 1) : ℕ∞ω) ≤ n
x : E
hx : x ∈ s
m : Fin (i + 1) → E
⊢ (↑i : ℕ∞ω) < n

Tactic:
replace hi : (i : ℕ∞ω) < n := lt_of_lt_of_le (by norm_cast; simp) hi
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ∀ (hi : (↑i : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin i → E},
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin i) → E) → G) m : G)
      ((((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : (↑i : ℕ∞ω) < n
⊢ DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s) s

Tactic:
have h_deriv_apply : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i (fun y ↦ (c y) u) s) s :=
      (hc.clm_apply contDiffOn_const).differentiableOn_iteratedFDerivWithin hi hs
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ∀ (hi : (↑i : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin i → E},
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin i) → E) → G) m : G)
      ((((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : (↑i : ℕ∞ω) < n
h_deriv_apply :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s) s
⊢ DifferentiableOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 i c s)
    s

Tactic:
have h_deriv : DifferentiableOn 𝕜 (iteratedFDerivWithin 𝕜 i c s) s :=
      hc.differentiableOn_iteratedFDerivWithin hi hs
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ∀ (hi : (↑i : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin i → E},
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin i) → E) → G) m : G)
      ((((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : (↑i : ℕ∞ω) < n
h_deriv_apply :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s) s
h_deriv :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 i c s)
    s
succ :
  Eq.{u_4 + 1} (α := G)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) G)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) :
          (a : (i : Fin i) → E) → G)
        (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
      G)
    ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x :
                      (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G))
                    (m 0) :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) :
                (a : (i : Fin i) → E) → F →L[𝕜] G)
              (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
            F →L[𝕜] G) :
          (a : F) → G)
        u :
      G)
⊢ Eq.{u_4 + 1} (α := G)
    ((iteratedFDerivWithin 𝕜 (i + 1) (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin (i + 1)) → E) → G) m : G)
    ((((iteratedFDerivWithin 𝕜 (i + 1) c s x : (a : (i : Fin (i + 1)) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G)
        u :
      G)

Tactic:
simp only [iteratedFDerivWithin_succ_apply_left]

Premises used: iteratedFDerivWithin_succ_apply_left
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ∀ (hi : (↑i : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin i → E},
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin i) → E) → G) m : G)
      ((((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : (↑i : ℕ∞ω) < n
h_deriv_apply :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s) s
h_deriv :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 i c s)
    s
succ :
  Eq.{u_4 + 1} (α := G)
    ((fderivWithin 𝕜
            (fun (y : E) ↦
              (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s y : (a : (i : Fin i) → E) → G)
                (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m))
            s x :
          (a : E) → G)
        (m 0) :
      G)
    ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x :
                      (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G))
                    (m 0) :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) :
                (a : (i : Fin i) → E) → F →L[𝕜] G)
              (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
            F →L[𝕜] G) :
          (a : F) → G)
        u :
      G)
⊢ Eq.{u_4 + 1} (α := G)
    ((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s) s x :
                (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) G)
              (m 0) :
            ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G) :
          (a : (i : Fin i) → E) → G)
        (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
      G)
    ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x :
                      (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G))
                    (m 0) :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) :
                (a : (i : Fin i) → E) → F →L[𝕜] G)
              (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
            F →L[𝕜] G) :
          (a : F) → G)
        u :
      G)

Tactic:
rw [← fderivWithin_continuousMultilinear_apply_const_apply (hs x hx) (h_deriv_apply x hx)]

Premises used: fderivWithin_continuousMultilinear_apply_const_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ∀ (hi : (↑i : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin i → E},
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin i) → E) → G) m : G)
      ((((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : (↑i : ℕ∞ω) < n
h_deriv_apply :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s) s
h_deriv :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 i c s)
    s
succ :
  Eq.{u_4 + 1} (α := G)
    ((fderivWithin 𝕜
            (fun (x : E) ↦
              (((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G)
                      (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
                    F →L[𝕜] G) :
                  (a : F) → G)
                u)
            s x :
          (a : E) → G)
        (m 0) :
      G)
    ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x :
                      (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G))
                    (m 0) :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) :
                (a : (i : Fin i) → E) → F →L[𝕜] G)
              (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
            F →L[𝕜] G) :
          (a : F) → G)
        u :
      G)
⊢ Eq.{u_4 + 1} (α := G)
    ((fderivWithin 𝕜
            (fun (y : E) ↦
              (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s y : (a : (i : Fin i) → E) → G)
                (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m))
            s x :
          (a : E) → G)
        (m 0) :
      G)
    ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x :
                      (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G))
                    (m 0) :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) :
                (a : (i : Fin i) → E) → F →L[𝕜] G)
              (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
            F →L[𝕜] G) :
          (a : F) → G)
        u :
      G)

Tactic:
rw [fderivWithin_congr' (fun x hx ↦ ih hi.le hx) hx]

Premises used: fderivWithin_congr', LT.lt.le
-- Module: Mathlib.Analysis.Calculus.ContDiff.Comp
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
n : ℕ∞ω
s : Set E
hs : UniqueDiffOn 𝕜 s
c : E → F →L[𝕜] G
hc : ContDiffOn 𝕜 n c s
u : F
i : ℕ
ih :
  ∀ (hi : (↑i : ℕ∞ω) ≤ n) {x : E} (hx : x ∈ s) {m : Fin i → E},
    Eq.{u_4 + 1} (α := G)
      ((iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s x : (a : (i : Fin i) → E) → G) m : G)
      ((((iteratedFDerivWithin 𝕜 i c s x : (a : (i : Fin i) → E) → F →L[𝕜] G) m : F →L[𝕜] G) : (a : F) → G) u : G)
x : E
hx : x ∈ s
m : Fin (i + 1) → E
hi : (↑i : ℕ∞ω) < n
h_deriv_apply :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin i) ↦ E) G)
    (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ (c y : (a : F) → G) u) s) s
h_deriv :
  DifferentiableOn 𝕜 (F := ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) (iteratedFDerivWithin 𝕜 i c s)
    s
succ succ₁ :
  Eq.{u_4 + 1} (α := G)
    ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x :
                      (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G))
                    (m 0) :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) :
                (a : (i : Fin i) → E) → F →L[𝕜] G)
              (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
            F →L[𝕜] G) :
          (a : F) → G)
        u :
      G)
    ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x :
                      (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G))
                    (m 0) :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) :
                (a : (i : Fin i) → E) → F →L[𝕜] G)
              (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
            F →L[𝕜] G) :
          (a : F) → G)
        u :
      G)
⊢ Eq.{u_4 + 1} (α := G)
    ((((fderivWithin 𝕜
                  (fun (y : E) ↦
                    (iteratedFDerivWithin 𝕜 i c s y : (a : (i : Fin i) → E) → F →L[𝕜] G)
                      (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m))
                  s x :
                (a : E) → F →L[𝕜] G)
              (m 0) :
            F →L[𝕜] G) :
          (a : F) → G)
        u :
      G)
    ((((((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i c s) s x :
                      (a : E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G))
                    (m 0) :
                  ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) (F →L[𝕜] G)) :
                (a : (i : Fin i) → E) → F →L[𝕜] G)
              (Fin.tail (α := fun (i : Fin (i + 1)) ↦ E) m) :
            F →L[𝕜] G) :
          (a : F) → G)
        u :
      G)

Tactic:
rw [fderivWithin_continuousMultilinear_apply_const_apply (hs x hx) (h_deriv x hx)]

Premises used: fderivWithin_continuousMultilinear_apply_const_apply