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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
s : Set E
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
c' : E →L[𝕜] 𝕜'
hc : HasFDerivWithinAt c c' s x
f : F
⊢ HasFDerivWithinAt (fun (y : E) ↦ c y • f) (c'.smulRight f) s x

Tactic:
simpa only [smul_zero, zero_add] using hc.smul (hasFDerivWithinAt_const f x s)

Premises used: hasFDerivWithinAt_const, smul_zero, zero_add, HasFDerivWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
c' : E →L[𝕜] 𝕜'
hc : HasFDerivAt c c' x
f : F
⊢ HasFDerivAt (fun (y : E) ↦ c y • f) (c'.smulRight f) x

Tactic:
simpa only [smul_zero, zero_add] using hc.smul (hasFDerivAt_const f x)

Premises used: smul_zero, zero_add, hasFDerivAt_const, HasFDerivAt.smul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Mul
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
s : Set E
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
f : F
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ c y • f) s x

Tactic:
(hc.hasFDerivWithinAt.smul_const f).differentiableWithinAt

Premises used: HasFDerivWithinAt.smul_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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
hc : DifferentiableAt 𝕜 c x
f : F
⊢ DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ c y • f) x

Tactic:
(hc.hasFDerivAt.smul_const f).differentiableAt

Premises used: HasFDerivAt.smul_const, 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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
hc : DifferentiableOn 𝕜 c s
f : F
⊢ DifferentiableOn.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ c y • f) s

Tactic:
fun x hx => (hc x hx).smul_const f

Premises used: DifferentiableWithinAt.smul_const, 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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
hc : Differentiable 𝕜 c
f : F
⊢ Differentiable.{u_1, u_2, u_3} 𝕜 (F := F) fun (y : E) ↦ c y • f

Tactic:
fun x => (hc x).smul_const f

Premises used: Differentiable, DifferentiableAt.smul_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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
s : Set E
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
hxs : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 c s x
f : F
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (y : E) ↦ c y • f) s x)
    (smulRight.{u_2, u_3, u_1, u_5} (S := 𝕜') (fderivWithin 𝕜 c s x) f)

Tactic:
(hc.hasFDerivWithinAt.smul_const f).fderivWithin hxs

Premises used: HasFDerivWithinAt.smul_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
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
𝕜' : Type u_5
inst_5 : NormedRing 𝕜'
inst_6 : NormedAlgebra 𝕜 𝕜'
inst_7 : Module 𝕜' F
inst_8 : IsBoundedSMul 𝕜' F
inst_9 : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
hc : DifferentiableAt 𝕜 c x
f : F
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (fun (y : E) ↦ c y • f) x) (smulRight.{u_2, u_3, u_1, u_5} (S := 𝕜') (fderiv 𝕜 c x) f)

Tactic:
(hc.hasFDerivAt.smul_const f).fderiv

Premises used: HasFDerivAt.smul_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
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
x : E
ha : HasStrictFDerivAt a a' x
hb : HasStrictFDerivAt b b' x
⊢ HasStrictFDerivAt (a * b) (a x •> b' + a' <• b x) x

Tactic:
((ContinuousLinearMap.mul 𝕜 𝔸).isBoundedBilinearMap.hasStrictFDerivAt (a x, b x)).comp x
    (ha.prodMk hb)

Premises used: ContinuousLinearMap.comp, HasStrictFDerivAt.prodMk, MulOpposite.unop, HasStrictFDerivAt.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 d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
⊢ HasStrictFDerivAt (c * d) (c x •> d' + c' <• d x) x

Tactic:
hc.mul' hd

Premises used: HasStrictFDerivAt.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
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
h : Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul (d x)) (HSMul.hSMul (MulOpposite.op (d x)))
⊢ HasStrictFDerivAt (c * d) (c x •> d' + d x •> c') x

Tactic:
convert! hc.mul' hd

Premises used: HasStrictFDerivAt.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
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
h :
  ∀ (z : E →L[𝕜] 𝔸') (x_1 : E),
    Eq.{u_6 + 1} (α := 𝔸') ((d x •> z : (a : E) → 𝔸') x_1 : 𝔸') ((z <• d x : (a : E) → 𝔸') x_1 : 𝔸')
⊢ Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul (d x)) (HSMul.hSMul (MulOpposite.op (d x)))

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 d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
z : E →L[𝕜] 𝔸'
x_1 : E
⊢ Eq.{u_6 + 1} (α := 𝔸') ((d x •> z : (a : E) → 𝔸') x_1 : 𝔸') ((z <• d x : (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 b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
ha : HasFDerivWithinAt a a' s x
hb : HasFDerivWithinAt b b' s x
⊢ HasFDerivWithinAt (a * b) (a x •> b' + a' <• b x) s x

Tactic:
((ContinuousLinearMap.mul 𝕜 𝔸).isBoundedBilinearMap.hasFDerivAt
    (a x, b x)).comp_hasFDerivWithinAt x (ha.prodMk hb)

Premises used: ContinuousLinearMap.comp, HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.prodMk, MulOpposite.unop
-- 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 b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
ha : HasFDerivWithinAt a a' s x
hb : HasFDerivWithinAt b b' s x
⊢ HasFDerivWithinAt (a * b) (a x •> b' + a' <• b x) s x

Tactic:
exact ((ContinuousLinearMap.mul 𝕜 𝔸).isBoundedBilinearMap.hasFDerivAt
    (a x, b x)).comp_hasFDerivWithinAt x (ha.prodMk hb)

Premises used: HasFDerivAt.comp_hasFDerivWithinAt, HasFDerivWithinAt.prodMk
-- 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 d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
⊢ HasFDerivWithinAt (c * d) (c x •> d' + c' <• d x) s x

Tactic:
hc.mul' hd

Premises used: HasFDerivWithinAt.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_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
h : Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul (d x)) (HSMul.hSMul (MulOpposite.op (d x)))
⊢ HasFDerivWithinAt (c * d) (c x •> d' + d x •> c') s x

Tactic:
convert! hc.mul' hd

Premises used: HasFDerivWithinAt.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_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
h :
  ∀ (z : E →L[𝕜] 𝔸') (x_1 : E),
    Eq.{u_6 + 1} (α := 𝔸') ((d x •> z : (a : E) → 𝔸') x_1 : 𝔸') ((z <• d x : (a : E) → 𝔸') x_1 : 𝔸')
⊢ Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul (d x)) (HSMul.hSMul (MulOpposite.op (d x)))

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 d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
z : E →L[𝕜] 𝔸'
x_1 : E
⊢ Eq.{u_6 + 1} (α := 𝔸') ((d x •> z : (a : E) → 𝔸') x_1 : 𝔸') ((z <• d x : (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 b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
ha : HasFDerivAt a a' x
hb : HasFDerivAt b b' x
⊢ HasFDerivAt (a * b) (a x •> b' + a' <• b x) x

Tactic:
((ContinuousLinearMap.mul 𝕜 𝔸).isBoundedBilinearMap.hasFDerivAt
    (a x, b x)).comp x (ha.prodMk hb)

Premises used: ContinuousLinearMap.comp, HasFDerivAt.prodMk, MulOpposite.unop, 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_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
ha : HasFDerivAt a a' x
hb : HasFDerivAt b b' x
⊢ HasFDerivAt (a * b) (a x •> b' + a' <• b x) x

Tactic:
exact ((ContinuousLinearMap.mul 𝕜 𝔸).isBoundedBilinearMap.hasFDerivAt
    (a x, b x)).comp x (ha.prodMk hb)

Premises used: HasFDerivAt.prodMk, 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 d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
hd : HasFDerivAt d d' x
⊢ HasFDerivAt (c * d) (c x •> d' + c' <• d x) x

Tactic:
hc.mul' hd

Premises used: HasFDerivAt.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
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
hd : HasFDerivAt d d' x
h : Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul (d x)) (HSMul.hSMul (MulOpposite.op (d x)))
⊢ HasFDerivAt (c * d) (c x •> d' + d x •> c') x

Tactic:
convert! hc.mul' hd

Premises used: HasFDerivAt.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
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
hd : HasFDerivAt d d' x
h :
  ∀ (z : E →L[𝕜] 𝔸') (x_1 : E),
    Eq.{u_6 + 1} (α := 𝔸') ((d x •> z : (a : E) → 𝔸') x_1 : 𝔸') ((z <• d x : (a : E) → 𝔸') x_1 : 𝔸')
⊢ Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul (d x)) (HSMul.hSMul (MulOpposite.op (d x)))

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 d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
hd : HasFDerivAt d d' x
z : E →L[𝕜] 𝔸'
x_1 : E
⊢ Eq.{u_6 + 1} (α := 𝔸') ((d x •> z : (a : E) → 𝔸') x_1 : 𝔸') ((z <• d x : (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 b : E → 𝔸
ha : DifferentiableWithinAt 𝕜 a s x
hb : DifferentiableWithinAt 𝕜 b s x
⊢ DifferentiableWithinAt 𝕜 (a * b) s x

Tactic:
(ha.hasFDerivWithinAt.mul' hb.hasFDerivWithinAt).differentiableWithinAt

Premises used: HasFDerivWithinAt.differentiableWithinAt, HasFDerivWithinAt.mul', 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 b : E → 𝔸
ha : DifferentiableAt 𝕜 a x
hb : DifferentiableAt 𝕜 b x
⊢ DifferentiableAt 𝕜 (a * b) x

Tactic:
(ha.hasFDerivAt.mul' hb.hasFDerivAt).differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt, HasFDerivAt.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
s : Set E
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
a b : E → 𝔸
ha : DifferentiableOn 𝕜 a s
hb : DifferentiableOn 𝕜 b s
⊢ DifferentiableOn 𝕜 (a * b) s

Tactic:
fun x hx => (ha x hx).mul (hb x hx)

Premises used: DifferentiableWithinAt.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 b : E → 𝔸
ha : Differentiable 𝕜 a
hb : Differentiable 𝕜 b
⊢ Differentiable 𝕜 (a * b)

Tactic:
fun x => (ha x).mul (hb x)

Premises used: Differentiable, DifferentiableAt.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 b : E → 𝔸
hxs : UniqueDiffWithinAt 𝕜 s x
ha : DifferentiableWithinAt 𝕜 a s x
hb : DifferentiableWithinAt 𝕜 b s x
⊢ fderivWithin 𝕜 (fun (y : E) ↦ a y * b y) s x = a x •> fderivWithin 𝕜 b s x + fderivWithin 𝕜 a s x <• b x

Tactic:
(ha.hasFDerivWithinAt.mul' hb.hasFDerivWithinAt).fderivWithin hxs

Premises used: HasFDerivWithinAt.fderivWithin, HasFDerivWithinAt.mul', 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_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
a b : E → 𝔸
hxs : UniqueDiffWithinAt 𝕜 s x
ha : DifferentiableWithinAt 𝕜 a s x
hb : DifferentiableWithinAt 𝕜 b s x
⊢ fderivWithin 𝕜 (a * b) s x = a x •> fderivWithin 𝕜 b s x + fderivWithin 𝕜 a s x <• b x

Tactic:
(ha.hasFDerivWithinAt.mul' hb.hasFDerivWithinAt).fderivWithin hxs

Premises used: HasFDerivWithinAt.fderivWithin, HasFDerivWithinAt.mul', 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 d : E → 𝔸'
hxs : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
⊢ fderivWithin 𝕜 (fun (y : E) ↦ c y * d y) s x = c x •> fderivWithin 𝕜 d s x + d x •> fderivWithin 𝕜 c s x

Tactic:
(hc.hasFDerivWithinAt.mul hd.hasFDerivWithinAt).fderivWithin hxs

Premises used: HasFDerivWithinAt.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
s : Set E
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
hxs : UniqueDiffWithinAt 𝕜 s x
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
⊢ fderivWithin 𝕜 (c * d) s x = c x •> fderivWithin 𝕜 d s x + d x •> fderivWithin 𝕜 c s x

Tactic:
(hc.hasFDerivWithinAt.mul hd.hasFDerivWithinAt).fderivWithin hxs

Premises used: HasFDerivWithinAt.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 b : E → 𝔸
ha : DifferentiableAt 𝕜 a x
hb : DifferentiableAt 𝕜 b x
⊢ fderiv 𝕜 (fun (y : E) ↦ a y * b y) x = a x •> fderiv 𝕜 b x + fderiv 𝕜 a x <• b x

Tactic:
(ha.hasFDerivAt.mul' hb.hasFDerivAt).fderiv

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv, HasFDerivAt.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
𝔸 : Type u_5
inst_3 : NormedRing 𝔸
inst_4 : NormedAlgebra 𝕜 𝔸
a b : E → 𝔸
ha : DifferentiableAt 𝕜 a x
hb : DifferentiableAt 𝕜 b x
⊢ fderiv 𝕜 (a * b) x = a x •> fderiv 𝕜 b x + fderiv 𝕜 a x <• b x

Tactic:
(ha.hasFDerivAt.mul' hb.hasFDerivAt).fderiv

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv, HasFDerivAt.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
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
hc : DifferentiableAt 𝕜 c x
hd : DifferentiableAt 𝕜 d x
⊢ fderiv 𝕜 (fun (y : E) ↦ c y * d y) x = c x •> fderiv 𝕜 d x + d x •> fderiv 𝕜 c x

Tactic:
(hc.hasFDerivAt.mul hd.hasFDerivAt).fderiv

Premises used: HasFDerivAt.mul, 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_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c d : E → 𝔸'
hc : DifferentiableAt 𝕜 c x
hd : DifferentiableAt 𝕜 d x
⊢ fderiv 𝕜 (c * d) x = c x •> fderiv 𝕜 d x + d x •> fderiv 𝕜 c x

Tactic:
(hc.hasFDerivAt.mul hd.hasFDerivAt).fderiv

Premises used: HasFDerivAt.mul, 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) ↦ a y * b) (a' <• b) x

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

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.hasStrictFDerivAt, ContinuousLinearMap.mul, ContinuousLinearMap.flip, MulOpposite.unop, 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
𝔸' : Type u_6
inst_3 : NormedCommRing 𝔸'
inst_4 : NormedAlgebra 𝕜 𝔸'
c : E → 𝔸'
c' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
d : 𝔸'
⊢ HasStrictFDerivAt (fun (y : E) ↦ c y * d) (c' <• d) x

Tactic:
hc.mul_const' d

Premises used: HasStrictFDerivAt.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 : HasStrictFDerivAt c c' x
d : 𝔸'
h : Eq (α := (E →L[𝕜] 𝔸') → E →L[𝕜] 𝔸') (HSMul.hSMul d) (HSMul.hSMul (MulOpposite.op d))
⊢ HasStrictFDerivAt (fun (y : E) ↦ c y * d) (d •> c') x

Tactic:
convert! hc.mul_const' d

Premises used: HasStrictFDerivAt.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 : HasStrictFDerivAt 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 : HasStrictFDerivAt 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 → 𝔸
a' : E →L[𝕜] 𝔸
ha : HasFDerivWithinAt a a' s x
b : 𝔸
⊢ HasFDerivWithinAt (fun (y : E) ↦ a y * b) (a' <• b) s x

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

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.hasFDerivAt, HasFDerivAt.comp_hasFDerivWithinAt, ContinuousLinearMap.mul, ContinuousLinearMap.flip, MulOpposite.unop, DFunLike.coe