awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
d : 𝔸'
⊢ HasFDerivWithinAt (fun (y : E) ↦ c y * d) (c' <• d) s x

Tactic:
hc.mul_const' d

Premises used: HasFDerivWithinAt.mul_const'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
d : 𝔸'
h : Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul d) (HSMul.hSMul (MulOpposite.op d))
⊢ HasFDerivWithinAt (fun (y : E) ↦ c y * d) (d •> c') s x

Tactic:
convert! hc.mul_const' d

Premises used: HasFDerivWithinAt.mul_const'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
d : 𝔸'
h : ∀ (z : E →L[𝕜] 𝔸') (x : E), Eq.{u_6 + 1} (α := 𝔸') ((d •> z : (a : E) → 𝔸') x : 𝔸') ((z <• d : (a : E) → 𝔸') x : 𝔸')
⊢ Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul d) (HSMul.hSMul (MulOpposite.op d))

Tactic:
ext z
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
d : 𝔸'
z : E →L[𝕜] 𝔸'
x_1 : E
⊢ Eq.{u_6 + 1} (α := 𝔸') ((d •> z : (a : E) → 𝔸') x_1 : 𝔸') ((z <• d : (a : E) → 𝔸') x_1 : 𝔸')

Tactic:
apply mul_comm

Premises used: mul_comm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
a : E → 𝔸
a' : E →L[𝕜] 𝔸
ha : HasFDerivAt a a' x
b : 𝔸
⊢ HasFDerivAt (fun (y : E) ↦ a y * b) (a' <• b) x

Tactic:
((ContinuousLinearMap.mul 𝕜 𝔸).flip b).hasFDerivAt.comp x ha

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.hasFDerivAt, ContinuousLinearMap.mul, ContinuousLinearMap.flip, MulOpposite.unop, DFunLike.coe, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
d : 𝔸'
⊢ HasFDerivAt (fun (y : E) ↦ c y * d) (c' <• d) x

Tactic:
hc.mul_const' d

Premises used: HasFDerivAt.mul_const'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
d : 𝔸'
h : Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul d) (HSMul.hSMul (MulOpposite.op d))
⊢ HasFDerivAt (fun (y : E) ↦ c y * d) (d •> c') x

Tactic:
convert! hc.mul_const' d

Premises used: HasFDerivAt.mul_const'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
d : 𝔸'
h : ∀ (z : E →L[𝕜] 𝔸') (x : E), Eq.{u_6 + 1} (α := 𝔸') ((d •> z : (a : E) → 𝔸') x : 𝔸') ((z <• d : (a : E) → 𝔸') x : 𝔸')
⊢ Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul d) (HSMul.hSMul (MulOpposite.op d))

Tactic:
ext z
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
d : 𝔸'
z : E →L[𝕜] 𝔸'
x_1 : E
⊢ Eq.{u_6 + 1} (α := 𝔸') ((d •> z : (a : E) → 𝔸') x_1 : 𝔸') ((z <• d : (a : E) → 𝔸') x_1 : 𝔸')

Tactic:
apply mul_comm

Premises used: mul_comm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
a : E → 𝔸
ha : DifferentiableWithinAt 𝕜 a s x
b : 𝔸
⊢ DifferentiableWithinAt.{u_1, u_2, u_5} 𝕜 (F := 𝔸) (fun (y : E) ↦ a y * b) s x

Tactic:
(ha.hasFDerivWithinAt.mul_const' b).differentiableWithinAt

Premises used: HasFDerivWithinAt.mul_const', HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
a : E → 𝔸
ha : DifferentiableAt 𝕜 a x
b : 𝔸
⊢ DifferentiableAt.{u_1, u_2, u_5} 𝕜 (F := 𝔸) (fun (y : E) ↦ a y * b) x

Tactic:
(ha.hasFDerivAt.mul_const' b).differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt, HasFDerivAt.mul_const'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
a : E → 𝔸
ha : DifferentiableOn 𝕜 a s
b : 𝔸
⊢ DifferentiableOn.{u_1, u_2, u_5} 𝕜 (F := 𝔸) (fun (y : E) ↦ a y * b) s

Tactic:
fun x hx => (ha x hx).mul_const b

Premises used: DifferentiableOn, DifferentiableWithinAt.mul_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
a : E → 𝔸
ha : Differentiable 𝕜 a
b : 𝔸
⊢ Differentiable.{u_1, u_2, u_5} 𝕜 (F := 𝔸) fun (y : E) ↦ a y * b

Tactic:
fun x => (ha x).mul_const b

Premises used: Differentiable, DifferentiableAt.mul_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
a : E → 𝔸
hxs : UniqueDiffWithinAt 𝕜 s x
ha : DifferentiableWithinAt 𝕜 a s x
b : 𝔸
⊢ fderivWithin 𝕜 (fun (y : E) ↦ a y * b) s x = fderivWithin 𝕜 a s x <• b

Tactic:
(ha.hasFDerivWithinAt.mul_const' b).fderivWithin hxs

Premises used: HasFDerivWithinAt.mul_const', HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
hxs : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 c s x
d : 𝔸'
⊢ fderivWithin 𝕜 (fun (y : E) ↦ c y * d) s x = d •> fderivWithin 𝕜 c s x

Tactic:
(hc.hasFDerivWithinAt.mul_const d).fderivWithin hxs

Premises used: HasFDerivWithinAt.mul_const, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
a : E → 𝔸
ha : DifferentiableAt 𝕜 a x
b : 𝔸
⊢ fderiv 𝕜 (fun (y : E) ↦ a y * b) x = fderiv 𝕜 a x <• b

Tactic:
(ha.hasFDerivAt.mul_const' b).fderiv

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv, HasFDerivAt.mul_const'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
hc : DifferentiableAt 𝕜 c x
d : 𝔸'
⊢ fderiv 𝕜 (fun (y : E) ↦ c y * d) x = d •> fderiv 𝕜 c x

Tactic:
(hc.hasFDerivAt.mul_const d).fderiv

Premises used: HasFDerivAt.mul_const, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
a : E → 𝔸
a' : E →L[𝕜] 𝔸
ha : HasStrictFDerivAt a a' x
b : 𝔸
⊢ HasStrictFDerivAt (fun (y : E) ↦ b * a y) (b •> a') x

Tactic:
((ContinuousLinearMap.mul 𝕜 𝔸) b).hasStrictFDerivAt.comp x ha

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.hasStrictFDerivAt, ContinuousLinearMap.mul, HasStrictFDerivAt.comp, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
a : E → 𝔸
a' : E →L[𝕜] 𝔸
ha : HasFDerivWithinAt a a' s x
b : 𝔸
⊢ HasFDerivWithinAt (fun (y : E) ↦ b * a y) (b •> a') s x

Tactic:
((ContinuousLinearMap.mul 𝕜 𝔸) b).hasFDerivAt.comp_hasFDerivWithinAt x ha

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.hasFDerivAt, HasFDerivAt.comp_hasFDerivWithinAt, ContinuousLinearMap.mul, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
a : E → 𝔸
a' : E →L[𝕜] 𝔸
ha : HasFDerivAt a a' x
b : 𝔸
⊢ HasFDerivAt (fun (y : E) ↦ b * a y) (b •> a') x

Tactic:
((ContinuousLinearMap.mul 𝕜 𝔸) b).hasFDerivAt.comp x ha

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.hasFDerivAt, ContinuousLinearMap.mul, DFunLike.coe, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
a : E → 𝔸
ha : DifferentiableWithinAt 𝕜 a s x
b : 𝔸
⊢ DifferentiableWithinAt.{u_1, u_2, u_5} 𝕜 (F := 𝔸) (fun (y : E) ↦ b * a y) s x

Tactic:
(ha.hasFDerivWithinAt.const_mul b).differentiableWithinAt

Premises used: HasFDerivWithinAt.const_mul, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
a : E → 𝔸
ha : DifferentiableAt 𝕜 a x
b : 𝔸
⊢ DifferentiableAt.{u_1, u_2, u_5} 𝕜 (F := 𝔸) (fun (y : E) ↦ b * a y) x

Tactic:
(ha.hasFDerivAt.const_mul b).differentiableAt

Premises used: HasFDerivAt.const_mul, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set E
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
a : E → 𝔸
ha : DifferentiableOn 𝕜 a s
b : 𝔸
⊢ DifferentiableOn.{u_1, u_2, u_5} 𝕜 (F := 𝔸) (fun (y : E) ↦ b * a y) s

Tactic:
fun x hx => (ha x hx).const_mul b

Premises used: DifferentiableWithinAt.const_mul, DifferentiableOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
a : E → 𝔸
ha : Differentiable 𝕜 a
b : 𝔸
⊢ Differentiable.{u_1, u_2, u_5} 𝕜 (F := 𝔸) fun (y : E) ↦ b * a y

Tactic:
fun x => (ha x).const_mul b

Premises used: Differentiable, DifferentiableAt.const_mul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
a : E → 𝔸
hxs : UniqueDiffWithinAt 𝕜 s x
ha : DifferentiableWithinAt 𝕜 a s x
b : 𝔸
⊢ fderivWithin 𝕜 (fun (y : E) ↦ b * a y) s x = b •> fderivWithin 𝕜 a s x

Tactic:
(ha.hasFDerivWithinAt.const_mul b).fderivWithin hxs

Premises used: HasFDerivWithinAt.const_mul, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
a : E → 𝔸
ha : DifferentiableAt 𝕜 a x
b : 𝔸
⊢ fderiv 𝕜 (fun (y : E) ↦ b * a y) x = b •> fderiv 𝕜 a x

Tactic:
(ha.hasFDerivAt.const_mul b).fderiv

Premises used: HasFDerivAt.const_mul, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
inst_3 : Finite ι
l : List ι
x : ι → 𝔸
have :
  ∀ (this : Fintype ι),
    HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x l).prod)
      (∑ i : Fin l.length,
        (List.map x (List.take (↑i : ℕ) l)).prod •>
          (proj (φ := fun (a : ι) ↦ 𝔸)
              (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
            (List.map x (List.drop (↑i : ℕ).succ l)).prod))
      x
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x l).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l)).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l)).prod))
    x

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
inst_3 : Finite ι
x : ι → 𝔸
this : Fintype ι
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x []).prod)
    (∑ i : Fin [].length,
      (List.map x (List.take (↑i : ℕ) [])).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin (List.length.{u_5} (α := ι) [])) ↦ (↑i : ℕ) < xs.length) [] i
              ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ [])).prod))
    x

Tactic:
simp [hasStrictFDerivAt_const]

Premises used: hasStrictFDerivAt_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
inst_3 : Finite ι
x : ι → 𝔸
this : Fintype ι
a : ι
l : List ι
IH :
  HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x l).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l)).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l)).prod))
    x
cons :
  HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸)
    (fun (x : ι → 𝔸) ↦
      HMul.hMul (α := 𝔸) ((proj (φ := fun (x : ι) ↦ 𝔸) a : (a : (i : ι) → 𝔸) → 𝔸) x : 𝔸) (List.map x l).prod)
    (∑ i : Fin (a :: l).length,
      (List.map x (List.take (↑i : ℕ) (a :: l))).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin (a :: l).length) ↦ (↑i : ℕ) < xs.length) (a :: l) i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ (a :: l))).prod))
    x
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x (a :: l)).prod)
    (∑ i : Fin (a :: l).length,
      (List.map x (List.take (↑i : ℕ) (a :: l))).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin (a :: l).length) ↦ (↑i : ℕ) < xs.length) (a :: l) i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ (a :: l))).prod))
    x

Tactic:
simp only [List.map_cons, List.prod_cons, ← proj_apply (R := 𝕜) (φ := fun _ : ι ↦ 𝔸) a]

Premises used: List.map_cons, ContinuousLinearMap.proj_apply, List.prod_cons
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
inst_3 : Finite ι
x : ι → 𝔸
this : Fintype ι
a : ι
l : List ι
IH :
  HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x l).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l)).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l)).prod))
    x
h :
  ∀ (x_1 : ι → 𝔸),
    Eq.{u_6 + 1} (α := 𝔸)
      ((((proj (φ := fun (x : ι) ↦ 𝔸) a : (a : (i : ι) → 𝔸) → 𝔸) x : 𝔸) •>
                ∑ i : Fin l.length,
                  (List.map x (List.take (↑i : ℕ) l)).prod •>
                    (proj (φ := fun (a : ι) ↦ 𝔸)
                        (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
                      (List.map x (List.drop (↑i : ℕ).succ l)).prod) +
              proj (φ := fun (x : ι) ↦ 𝔸) a <• (List.map x l).prod :
            (a : ι → 𝔸) → 𝔸)
          x_1 :
        𝔸)
      ((∑ i : Fin (a :: l).length,
              (List.map x (List.take (↑i : ℕ) (a :: l))).prod •>
                (proj (φ := fun (a : ι) ↦ 𝔸)
                    (getElem (valid := fun (xs : List ι) (i : Fin (a :: l).length) ↦ (↑i : ℕ) < xs.length) (a :: l) i
                      ⋯) <•
                  (List.map x (List.drop (↑i : ℕ).succ (a :: l))).prod) :
            (a : ι → 𝔸) → 𝔸)
          x_1 :
        𝔸)
⊢ ((proj (φ := fun (x : ι) ↦ 𝔸) a : (a : (i : ι) → 𝔸) → 𝔸) x : 𝔸) •>
        ∑ i : Fin l.length,
          (List.map x (List.take (↑i : ℕ) l)).prod •>
            (proj (φ := fun (a : ι) ↦ 𝔸)
                (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
              (List.map x (List.drop (↑i : ℕ).succ l)).prod) +
      proj (φ := fun (x : ι) ↦ 𝔸) a <• (List.map x l).prod =
    ∑ i : Fin (a :: l).length,
      (List.map x (List.take (↑i : ℕ) (a :: l))).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin (a :: l).length) ↦ (↑i : ℕ) < xs.length) (a :: l) i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ (a :: l))).prod)

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
inst_3 : Finite ι
x : ι → 𝔸
this : Fintype ι
a : ι
l : List ι
IH :
  HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x l).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l)).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l)).prod))
    x
x_1 : ι → 𝔸
⊢ Eq.{u_6 + 1} (α := 𝔸)
    ((((proj (φ := fun (x : ι) ↦ 𝔸) a : (a : (i : ι) → 𝔸) → 𝔸) x : 𝔸) •>
              ∑ i : Fin l.length,
                (List.map x (List.take (↑i : ℕ) l)).prod •>
                  (proj (φ := fun (a : ι) ↦ 𝔸)
                      (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
                    (List.map x (List.drop (↑i : ℕ).succ l)).prod) +
            proj (φ := fun (x : ι) ↦ 𝔸) a <• (List.map x l).prod :
          (a : ι → 𝔸) → 𝔸)
        x_1 :
      𝔸)
    ((∑ i : Fin (a :: l).length,
            (List.map x (List.take (↑i : ℕ) (a :: l))).prod •>
              (proj (φ := fun (a : ι) ↦ 𝔸)
                  (getElem (valid := fun (xs : List ι) (i : Fin (a :: l).length) ↦ (↑i : ℕ) < xs.length) (a :: l) i
                    ⋯) <•
                (List.map x (List.drop (↑i : ℕ).succ (a :: l))).prod) :
          (a : ι → 𝔸) → 𝔸)
        x_1 :
      𝔸)

Tactic:
simp [Fin.sum_univ_succ, Finset.mul_sum, mul_assoc, add_comm]

Premises used: Finset.mul_sum, mul_assoc, add_comm, Fin.sum_univ_succ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
inst_3 : Finite ι
x : ι → 𝔸
this : Fintype ι
a : ι
l : List ι
IH :
  HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x l).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l)).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l)).prod))
    x
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸)
    (fun (x : ι → 𝔸) ↦
      HMul.hMul (α := 𝔸) ((proj (φ := fun (x : ι) ↦ 𝔸) a : (a : (i : ι) → 𝔸) → 𝔸) x : 𝔸) (List.map x l).prod)
    (∑ i : Fin (a :: l).length,
      (List.map x (List.take (↑i : ℕ) (a :: l))).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin (a :: l).length) ↦ (↑i : ℕ) < xs.length) (a :: l) i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ (a :: l))).prod))
    x

Tactic:
exact .congr_fderiv (.mul' (ContinuousLinearMap.hasStrictFDerivAt _) IH)
      (by ext; simp [Fin.sum_univ_succ, Finset.mul_sum, mul_assoc, add_comm])
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
inst_3 : Finite ι
l : List ι
x : ι → 𝔸
this : Fintype ι
nil :
  HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x []).prod)
    (∑ i : Fin [].length,
      (List.map x (List.take (↑i : ℕ) [])).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin (List.length.{u_5} (α := ι) [])) ↦ (↑i : ℕ) < xs.length) [] i
              ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ [])).prod))
    x
cons :
  ∀ (a : ι) (l : List ι)
    (IH :
      HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x l).prod)
        (∑ i : Fin l.length,
          (List.map x (List.take (↑i : ℕ) l)).prod •>
            (proj (φ := fun (a : ι) ↦ 𝔸)
                (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
              (List.map x (List.drop (↑i : ℕ).succ l)).prod))
        x),
    HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x (a :: l)).prod)
      (∑ i : Fin (a :: l).length,
        (List.map x (List.take (↑i : ℕ) (a :: l))).prod •>
          (proj (φ := fun (a : ι) ↦ 𝔸)
              (getElem (valid := fun (xs : List ι) (i : Fin (a :: l).length) ↦ (↑i : ℕ) < xs.length) (a :: l) i ⋯) <•
            (List.map x (List.drop (↑i : ℕ).succ (a :: l))).prod))
      x
⊢ HasStrictFDerivAt (𝕜 := 𝕜) (F := 𝔸) (fun (x : ι → 𝔸) ↦ (List.map x l).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i : ℕ) l)).prod •>
        (proj (φ := fun (a : ι) ↦ 𝔸)
            (getElem (valid := fun (xs : List ι) (i : Fin l.length) ↦ (↑i : ℕ) < xs.length) l i ⋯) <•
          (List.map x (List.drop (↑i : ℕ).succ l)).prod))
    x

Tactic:
induction l with
  | nil => simp [hasStrictFDerivAt_const]
  | cons a l IH =>
    simp only [List.map_cons, List.prod_cons, ← proj_apply (R := 𝕜) (φ := fun _ : ι ↦ 𝔸) a]
    exact .congr_fderiv (.mul' (ContinuousLinearMap.hasStrictFDerivAt _) IH)
      (by ext; simp [Fin.sum_univ_succ, Finset.mul_sum, mul_assoc, add_comm])

Premises used: List.map_cons, hasStrictFDerivAt_const, List.prod_cons