awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
x : E
n : ℕ∞ω
𝕜' : Type u_3
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
f : E → 𝕜'
g : E → F
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g x
hf₁ : ContDiffWithinAt 𝕜 n f univ x
⊢ ContDiffWithinAt 𝕜 n g univ x

Tactic:
rw [← contDiffWithinAt_univ] at *

Premises used: contDiffWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
x : E
n : ℕ∞ω
𝕜' : Type u_3
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
f : E → 𝕜'
g : E → F
hf : ContDiffWithinAt 𝕜 n f univ x
hg : ContDiffWithinAt 𝕜 n g univ x
⊢ ContDiffWithinAt 𝕜 n (f • g) univ x

Tactic:
hf.smul hg

Premises used: ContDiffWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
x : E
n : ℕ∞ω
𝕜' : Type u_3
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
f : E → 𝕜'
g : E → F
hf : ContDiffWithinAt 𝕜 n f univ x
hg : ContDiffWithinAt 𝕜 n g univ x
⊢ ContDiffWithinAt 𝕜 n (f • g) univ x

Tactic:
exact hf.smul hg

Premises used: ContDiffWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
n : ℕ∞ω
𝕜' : Type u_3
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
f : E → 𝕜'
g : E → F
hf : ContDiff 𝕜 n f
hg : ContDiff 𝕜 n g
⊢ ContDiff 𝕜 n (f • g)

Tactic:
contDiff_smul.comp (hf.prodMk hg)

Premises used: ContDiff.prodMk, ContDiff.comp, contDiff_smul
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
n : ℕ∞ω
𝕜' : Type u_3
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
s : Set E
f : E → 𝕜'
g : E → F
hf : ContDiffOn 𝕜 n f s
hg : ContDiffOn 𝕜 n g s
⊢ ContDiffOn 𝕜 n (f • g) s

Tactic:
fun x hx =>
  (hf x hx).smul (hg x hx)

Premises used: ContDiffOn, ContDiffWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
R : Type u_3
inst_3 : DistribSMul R F
inst_4 : SMulCommClass 𝕜 R F
inst_5 : ContinuousConstSMul R F
c : R
⊢ ContDiff 𝕜 (F := F) n fun (p : F) ↦ c • p

Tactic:
(c • ContinuousLinearMap.id 𝕜 F).contDiff

Premises used: ContinuousLinearMap.id, HSMul.hSMul, ContinuousLinearMap.contDiff
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type uF
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ∞ω
A : Type u_4
inst_3 : NormedRing A
inst_4 : NormedAlgebra 𝕜 A
inst_5 : Module A F
inst_6 : IsScalarTower 𝕜 A F
inst_7 : IsBoundedSMul A F
v : F
⊢ ContDiff.{u_1, u_4, uF} 𝕜 (F := F) n fun (a : A) ↦ a • v

Tactic:
((ContinuousLinearMap.id 𝕜 A).smulRight v).contDiff

Premises used: ContinuousLinearMap.smulRight, ContinuousLinearMap.id, ContinuousLinearMap.contDiff
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
n : ℕ∞ω
R : Type u_3
inst_5 : DistribSMul R F
inst_6 : SMulCommClass 𝕜 R F
inst_7 : ContinuousConstSMul R F
s : Set E
f : E → F
x : E
c : R
hf : ContDiffWithinAt 𝕜 n f s x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (y : E) ↦ c • f y) s x

Tactic:
(contDiff_const_smul c).contDiffAt.comp_contDiffWithinAt x hf

Premises used: contDiff_const_smul, ContDiffAt.comp_contDiffWithinAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
n : ℕ∞ω
A : Type u_4
inst_5 : NormedRing A
inst_6 : NormedAlgebra 𝕜 A
inst_7 : Module A F
inst_8 : IsScalarTower 𝕜 A F
inst_9 : IsBoundedSMul A F
s : Set E
f : E → A
x : E
hf : ContDiffWithinAt 𝕜 n f s x
v : F
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (y : E) ↦ f y • v) s x

Tactic:
(contDiff_smul_const v).contDiffAt.comp_contDiffWithinAt x hf

Premises used: contDiff_smul_const, ContDiffAt.comp_contDiffWithinAt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
n : ℕ∞ω
R : Type u_3
inst_5 : DistribSMul R F
inst_6 : SMulCommClass 𝕜 R F
inst_7 : ContinuousConstSMul R F
f : E → F
x : E
c : R
hf : ContDiffAt 𝕜 n f x
⊢ ContDiffWithinAt 𝕜 n f univ x

Tactic:
rw [← contDiffWithinAt_univ] at *

Premises used: contDiffWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
n : ℕ∞ω
R : Type u_3
inst_5 : DistribSMul R F
inst_6 : SMulCommClass 𝕜 R F
inst_7 : ContinuousConstSMul R F
f : E → F
x : E
c : R
hf : ContDiffWithinAt 𝕜 n f univ x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (y : E) ↦ c • f y) univ x

Tactic:
hf.const_smul c

Premises used: ContDiffWithinAt.const_smul
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
n : ℕ∞ω
R : Type u_3
inst_5 : DistribSMul R F
inst_6 : SMulCommClass 𝕜 R F
inst_7 : ContinuousConstSMul R F
f : E → F
x : E
c : R
hf : ContDiffWithinAt 𝕜 n f univ x
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (y : E) ↦ c • f y) univ x

Tactic:
exact hf.const_smul c

Premises used: ContDiffWithinAt.const_smul
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
n : ℕ∞ω
A : Type u_4
inst_5 : NormedRing A
inst_6 : NormedAlgebra 𝕜 A
inst_7 : Module A F
inst_8 : IsScalarTower 𝕜 A F
inst_9 : IsBoundedSMul A F
f : E → A
x : E
hf : ContDiffAt 𝕜 n f x
v : F
rw :
  ∀ (hf : ContDiffWithinAt 𝕜 n f univ x) (v : F),
    ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (y : E) ↦ f y • v) univ x
⊢ ContDiffAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (y : E) ↦ f y • v) x

Tactic:
rw [← contDiffWithinAt_univ] at *

Premises used: contDiffWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
n : ℕ∞ω
A : Type u_4
inst_5 : NormedRing A
inst_6 : NormedAlgebra 𝕜 A
inst_7 : Module A F
inst_8 : IsScalarTower 𝕜 A F
inst_9 : IsBoundedSMul A F
f : E → A
x : E
hf : ContDiffWithinAt 𝕜 n f univ x
v : F
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (y : E) ↦ f y • v) univ x

Tactic:
hf.smul_const v

Premises used: ContDiffWithinAt.smul_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
n : ℕ∞ω
A : Type u_4
inst_5 : NormedRing A
inst_6 : NormedAlgebra 𝕜 A
inst_7 : Module A F
inst_8 : IsScalarTower 𝕜 A F
inst_9 : IsBoundedSMul A F
f : E → A
x : E
hf : ContDiffWithinAt 𝕜 n f univ x
v : F
⊢ ContDiffWithinAt.{u_1, uE, uF} 𝕜 (F := F) n (fun (y : E) ↦ f y • v) univ x

Tactic:
exact hf.smul_const v

Premises used: ContDiffWithinAt.smul_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
n : ℕ∞ω
R : Type u_3
inst_5 : DistribSMul R F
inst_6 : SMulCommClass 𝕜 R F
inst_7 : ContinuousConstSMul R F
f : E → F
c : R
hf : ContDiff 𝕜 n f
⊢ ContDiff.{u_1, uE, uF} 𝕜 (F := F) n fun (y : E) ↦ c • f y

Tactic:
(contDiff_const_smul c).comp hf

Premises used: contDiff_const_smul, ContDiff.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
n : ℕ∞ω
A : Type u_4
inst_5 : NormedRing A
inst_6 : NormedAlgebra 𝕜 A
inst_7 : Module A F
inst_8 : IsScalarTower 𝕜 A F
inst_9 : IsBoundedSMul A F
f : E → A
hf : ContDiff 𝕜 n f
v : F
⊢ ContDiff.{u_1, uE, uF} 𝕜 (F := F) n fun (y : E) ↦ f y • v

Tactic:
(contDiff_smul_const v).comp hf

Premises used: contDiff_smul_const, ContDiff.comp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
n : ℕ∞ω
R : Type u_3
inst_5 : DistribSMul R F
inst_6 : SMulCommClass 𝕜 R F
inst_7 : ContinuousConstSMul R F
s : Set E
f : E → F
c : R
hf : ContDiffOn 𝕜 n f s
⊢ ContDiffOn.{u_1, uE, uF} 𝕜 (F := F) n (fun (y : E) ↦ c • f y) s

Tactic:
fun x hx => (hf x hx).const_smul c

Premises used: ContDiffOn, ContDiffWithinAt.const_smul
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
n : ℕ∞ω
A : Type u_4
inst_5 : NormedRing A
inst_6 : NormedAlgebra 𝕜 A
inst_7 : Module A F
inst_8 : IsScalarTower 𝕜 A F
inst_9 : IsBoundedSMul A F
s : Set E
f : E → A
hf : ContDiffOn 𝕜 n f s
v : F
⊢ ContDiffOn.{u_1, uE, uF} 𝕜 (F := F) n (fun (y : E) ↦ f y • v) s

Tactic:
fun x hx => (hf x hx).smul_const v

Premises used: ContDiffOn, ContDiffWithinAt.smul_const
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
f : E → F
x : E
R : Type u_3
inst_5 : DistribSMul R F
inst_6 : SMulCommClass 𝕜 R F
inst_7 : ContinuousConstSMul R F
i : ℕ
a : R
hf : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ iteratedFDerivWithin 𝕜 i (a • f) s x =
    HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) a
      (iteratedFDerivWithin 𝕜 i f s x)

Tactic:
(a • (1 : F →L[𝕜] F)).iteratedFDerivWithin_comp_left hf hu hx le_rfl

Premises used: le_rfl, ContinuousLinearMap.compContinuousMultilinearMap, ContinuousLinearMap.iteratedFDerivWithin_comp_left, HSMul.hSMul, OfNat.ofNat, LinearMap.compMultilinearMap
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
x : E
A : Type u_4
inst_5 : NormedRing A
inst_6 : NormedAlgebra 𝕜 A
inst_7 : Module A F
inst_8 : IsScalarTower 𝕜 A F
inst_9 : IsBoundedSMul A F
i : ℕ
v : F
f : E → A
hf : ContDiffWithinAt 𝕜 (↑i : ℕ∞ω) f s x
hu : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDerivWithin 𝕜 i (fun (y : E) ↦ f y • v) s x)
    (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E)
      (ContinuousLinearMap.smulRight (ContinuousLinearMap.id 𝕜 A) v) (iteratedFDerivWithin 𝕜 i f s x))

Tactic:
(ContinuousLinearMap.id 𝕜 A).smulRight v |>.iteratedFDerivWithin_comp_left hf hu hx le_rfl

Premises used: le_rfl, ContinuousLinearMap.smulRight, ContinuousLinearMap.iteratedFDerivWithin_comp_left, ContinuousLinearMap.id
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
f : E → F
x : E
R : Type u_3
inst_5 : DistribSMul R F
inst_6 : SMulCommClass 𝕜 R F
inst_7 : ContinuousConstSMul R F
i : ℕ
a : R
hf : ContDiffAt 𝕜 (↑i : ℕ∞ω) f x
⊢ iteratedFDeriv 𝕜 i (a • f) x =
    HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) a (iteratedFDeriv 𝕜 i f x)

Tactic:
(a • (1 : F →L[𝕜] F)).iteratedFDeriv_comp_left hf le_rfl

Premises used: le_rfl, ContinuousLinearMap.compContinuousMultilinearMap, HSMul.hSMul, OfNat.ofNat, ContinuousLinearMap.iteratedFDeriv_comp_left, LinearMap.compMultilinearMap
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
f : E → F
x : E
R : Type u_3
inst_5 : DistribSMul R F
inst_6 : SMulCommClass 𝕜 R F
inst_7 : ContinuousConstSMul R F
i : ℕ
a : R
hf : ContDiffAt 𝕜 (↑i : ℕ∞ω) f x
⊢ iteratedFDeriv 𝕜 i (fun (x : E) ↦ a • f x) x =
    HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) a (iteratedFDeriv 𝕜 i f x)

Tactic:
iteratedFDeriv_const_smul_apply hf

Premises used: iteratedFDeriv_const_smul_apply
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
x : E
A : Type u_4
inst_5 : NormedRing A
inst_6 : NormedAlgebra 𝕜 A
inst_7 : Module A F
inst_8 : IsScalarTower 𝕜 A F
inst_9 : IsBoundedSMul A F
i : ℕ
v : F
f : E → A
hf : ContDiffAt 𝕜 (↑i : ℕ∞ω) f x
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDeriv 𝕜 i (fun (y : E) ↦ f y • v) x)
    (ContinuousLinearMap.compContinuousMultilinearMap (M₁ := fun (i : Fin i) ↦ E)
      (ContinuousLinearMap.smulRight (ContinuousLinearMap.id 𝕜 A) v) (iteratedFDeriv 𝕜 i f x))

Tactic:
(ContinuousLinearMap.id 𝕜 A).smulRight v |>.iteratedFDeriv_comp_left hf le_rfl

Premises used: le_rfl, ContinuousLinearMap.smulRight, ContinuousLinearMap.id, ContinuousLinearMap.iteratedFDeriv_comp_left
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
f : E → F
i : ℕ
a : 𝕜
hf : ContDiff 𝕜 (↑0 : ℕ∞ω) f
zero :
  ∀ (x : E) (x_1 : (i : Fin 0) → E),
    Eq.{uF + 1} (α := F) ((iteratedFDeriv 𝕜 0 (fun (z : E) ↦ f (a • z)) x : (a : (i : Fin 0) → E) → F) x_1 : F)
      ((HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (HPow.hPow (β := ℕ) a 0)
              (iteratedFDeriv 𝕜 0 f (a • x)) :
            (a : (i : Fin 0) → E) → F)
          x_1 :
        F)
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
    (iteratedFDeriv 𝕜 0 fun (z : E) ↦ f (a • z)) fun (x : E) ↦
    HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (HPow.hPow (β := ℕ) a 0)
      (iteratedFDeriv 𝕜 0 f (a • x))

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
f : E → F
i : ℕ
a : 𝕜
hf : ContDiff 𝕜 (↑0 : ℕ∞ω) f
x : E
x_1 : (i : Fin 0) → E
⊢ Eq.{uF + 1} (α := F) ((iteratedFDeriv 𝕜 0 (fun (z : E) ↦ f (a • z)) x : (a : (i : Fin 0) → E) → F) x_1 : F)
    ((HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (HPow.hPow (β := ℕ) a 0)
            (iteratedFDeriv 𝕜 0 f (a • x)) :
          (a : (i : Fin 0) → E) → F)
        x_1 :
      F)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
f : E → F
i_1 : ℕ
a : 𝕜
i : ℕ
hi :
  ∀ (hf : ContDiff 𝕜 (↑i : ℕ∞ω) f),
    Eq (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDeriv 𝕜 i fun (z : E) ↦ f (a • z)) fun (x : E) ↦
      HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (a ^ i)
        (iteratedFDeriv 𝕜 i f (a • x))
hf : ContDiff 𝕜 (↑(i + 1) : ℕ∞ω) f
succ :
  ∀ (v : E) (x : (i : Fin (i + 1)) → E),
    Eq.{uF + 1} (α := F)
      ((iteratedFDeriv 𝕜 (i + 1) (fun (z : E) ↦ f (a • z)) v : (a : (i : Fin (i + 1)) → E) → F) x : F)
      ((HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F) (a ^ (i + 1))
              (iteratedFDeriv 𝕜 (i + 1) f (a • v)) :
            (a : (i : Fin (i + 1)) → E) → F)
          x :
        F)
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F)
    (iteratedFDeriv 𝕜 (i + 1) fun (z : E) ↦ f (a • z)) fun (x : E) ↦
    HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F) (a ^ (i + 1))
      (iteratedFDeriv 𝕜 (i + 1) f (a • x))

Tactic:
ext v
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
f : E → F
i_1 : ℕ
a : 𝕜
i : ℕ
hi :
  ∀ (hf : ContDiff 𝕜 (↑i : ℕ∞ω) f),
    Eq (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
      (iteratedFDeriv 𝕜 i fun (z : E) ↦ f (a • z)) fun (x : E) ↦
      HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (a ^ i)
        (iteratedFDeriv 𝕜 i f (a • x))
hf : ContDiff 𝕜 (↑(i + 1) : ℕ∞ω) f
v : E
x : (i : Fin (i + 1)) → E
succ :
  Eq.{uF + 1} (α := F)
    ((comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
            (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (i + 1)) ↦ E) F) :
                  (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) ≃ₗᵢ[𝕜]
                    ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (x : Fin (i + 1)) ↦ E) F) :
              (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F) →
                ContinuousMultilinearMap 𝕜 (fun (x : Fin (i + 1)) ↦ E) F)
            (fderiv 𝕜 (iteratedFDeriv 𝕜 i fun (z : E) ↦ f (a • z))) v :
          (a : (i : Fin (i + 1)) → E) → F)
        x :
      F)
    ((HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F) (a ^ (i + 1))
            (comp (β := E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
              (⇑(LinearIsometryEquiv.symm (continuousMultilinearCurryLeftEquiv 𝕜 (fun (x : Fin (i + 1)) ↦ E) F) :
                    (E →L[𝕜] ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) ≃ₗᵢ[𝕜]
                      ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (x : Fin (i + 1)) ↦ E) F) :
                (a : E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun (i : Fin i) ↦ E) F) →
                  ContinuousMultilinearMap 𝕜 (fun (x : Fin (i + 1)) ↦ E) F)
              (fderiv 𝕜 (iteratedFDeriv 𝕜 i f)) (a • v)) :
          (a : (i : Fin (i + 1)) → E) → F)
        x :
      F)
⊢ Eq.{uF + 1} (α := F) ((iteratedFDeriv 𝕜 (i + 1) (fun (z : E) ↦ f (a • z)) v : (a : (i : Fin (i + 1)) → E) → F) x : F)
    ((HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F) (a ^ (i + 1))
            (iteratedFDeriv 𝕜 (i + 1) f (a • v)) :
          (a : (i : Fin (i + 1)) → E) → F)
        x :
      F)

Tactic:
rw [iteratedFDeriv_succ_eq_comp_left, iteratedFDeriv_succ_eq_comp_left]

Premises used: iteratedFDeriv_succ_eq_comp_left
-- Module: Mathlib.Analysis.Calculus.ContDiff.Operations
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
f : E → F
i : ℕ
a : 𝕜
hf : ContDiff 𝕜 (↑i : ℕ∞ω) f
zero :
  ∀ (hf : ContDiff 𝕜 (↑0 : ℕ∞ω) f),
    Eq (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F)
      (iteratedFDeriv 𝕜 0 fun (z : E) ↦ f (a • z)) fun (x : E) ↦
      HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin 0) ↦ E) F) (HPow.hPow (β := ℕ) a 0)
        (iteratedFDeriv 𝕜 0 f (a • x))
succ :
  ∀ (i : ℕ)
    (hi :
      ∀ (hf : ContDiff 𝕜 (↑i : ℕ∞ω) f),
        Eq (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
          (iteratedFDeriv 𝕜 i fun (z : E) ↦ f (a • z)) fun (x : E) ↦
          HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (a ^ i)
            (iteratedFDeriv 𝕜 i f (a • x)))
    (hf : ContDiff 𝕜 (↑(i + 1) : ℕ∞ω) f),
    Eq (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F)
      (iteratedFDeriv 𝕜 (i + 1) fun (z : E) ↦ f (a • z)) fun (x : E) ↦
      HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin (i + 1)) ↦ E) F) (a ^ (i + 1))
        (iteratedFDeriv 𝕜 (i + 1) f (a • x))
⊢ Eq (α := E → ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F)
    (iteratedFDeriv 𝕜 i fun (z : E) ↦ f (a • z)) fun (x : E) ↦
    HSMul.hSMul (β := ContinuousMultilinearMap.{u_1, 0, uE, uF} 𝕜 (fun (i : Fin i) ↦ E) F) (a ^ i)
      (iteratedFDeriv 𝕜 i f (a • x))

Tactic:
induction i with
  | zero => ext; simp
  | succ i hi =>
    ext v
    rw [iteratedFDeriv_succ_eq_comp_left, iteratedFDeriv_succ_eq_comp_left]
    simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, self_le_add_right, hf.of_le, hi,
      comp_apply, continuousMultilinearCurryLeftEquiv_symm_apply,
      ContinuousMultilinearMap.smul_apply]
    rw [fderiv_fun_const_smul, fderiv_comp_smul, smul_smul, ← pow_succ]
    · simp
    rw [← Function.comp_def (g := (a • ·))]
    apply DifferentiableAt.comp
    · exact hf.contDiffAt.differentiableAt_iteratedFDeriv (Nat.cast_lt.2 i.lt_succ_self)
    · exact differentiableAt_id.const_smul _

Premises used: Iff.mpr, Nat.succ_eq_add_one, self_le_add_right, Fin.succ, pow_succ, DifferentiableAt.const_smul, smul_smul, Nat.cast_add, ContDiff.of_le, Function.comp_def, ContinuousMultilinearMap.smul_apply, fderiv_fun_const_smul, DifferentiableAt.comp, HSMul.hSMul, Function.comp_apply, continuousMultilinearCurryLeftEquiv_symm_apply, iteratedFDeriv_succ_eq_comp_left, ContDiffAt.differentiableAt_iteratedFDeriv, fderiv_comp_smul, Nat.cast_lt, Nat.cast_one, differentiableAt_id, ContDiff.contDiffAt