awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
G : Type u_1
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : 𝕜
B : E →L[𝕜] F →L[𝕜] G
u : 𝕜 → E
v : 𝕜 → F
hu : x ∈ tsupport v → DifferentiableAt 𝕜 u x
hv : x ∈ tsupport u → DifferentiableAt 𝕜 v x
⊢ deriv (fun (y : 𝕜) ↦ (((B : (a : E) → F →L[𝕜] G) (u y) : F →L[𝕜] G) : (a : F) → G) (v y)) x =
    HAdd.hAdd (α := G) (β := G) ((((B : (a : E) → F →L[𝕜] G) (u x) : F →L[𝕜] G) : (a : F) → G) (deriv v x) : G)
      ((((B : (a : E) → F →L[𝕜] G) (deriv u x) : F →L[𝕜] G) : (a : F) → G) (v x) : G)

Tactic:
(B.hasDerivAt_of_bilinear (fun hx ↦ (hu hx).hasDerivAt) fun hx ↦ (hv hx).hasDerivAt).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, ContinuousLinearMap.hasDerivAt_of_bilinear
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' s x
hf : HasDerivWithinAt f f' s x
⊢ HasDerivWithinAt (c • f) (c x • f' + c' • f x) s x

Tactic:
simpa using (HasFDerivWithinAt.smul hc hf).hasDerivWithinAt

Premises used: HasFDerivWithinAt.hasDerivWithinAt, HasFDerivWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivAt c c' x
hf : HasDerivAt f f' x
rw :
  ∀ (hc : HasDerivWithinAt c c' univ x) (hf : HasDerivWithinAt f f' univ x),
    HasDerivWithinAt (c • f) (c x • f' + c' • f x) univ x
⊢ HasDerivAt (c • f) (c x • f' + c' • f x) x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Premises used: hasDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' univ x
hf : HasDerivWithinAt f f' univ x
⊢ HasDerivWithinAt (c • f) (c x • f' + c' • f x) univ x

Tactic:
hc.smul hf

Premises used: HasDerivWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' univ x
hf : HasDerivWithinAt f f' univ x
⊢ HasDerivWithinAt (c • f) (c x • f' + c' • f x) univ x

Tactic:
exact hc.smul hf

Premises used: HasDerivWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasStrictDerivAt c c' x
hf : HasStrictDerivAt f f' x
⊢ HasStrictDerivAt (c • f) (c x • f' + c' • f x) x

Tactic:
simpa using (HasStrictFDerivAt.smul hc hf).hasStrictDerivAt

Premises used: HasStrictFDerivAt.hasStrictDerivAt, HasStrictFDerivAt.smul
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    derivWithin (fun (y : 𝕜) ↦ c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x
neg :
  ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
    derivWithin (fun (y : 𝕜) ↦ c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x
⊢ derivWithin (fun (y : 𝕜) ↦ c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Premises used: UniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x

Tactic:
(hc.hasDerivWithinAt.smul hf.hasDerivWithinAt).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x

Tactic:
exact (hc.hasDerivWithinAt.smul hf.hasDerivWithinAt).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.smul
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x

Tactic:
simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

Premises used: derivWithin_zero_of_not_uniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin (c • f) s x = c x • derivWithin f s x + derivWithin c s x • f x

Tactic:
derivWithin_fun_smul hc hf

Premises used: derivWithin_fun_smul
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableAt 𝕜 c x
hf : DifferentiableAt 𝕜 f x
⊢ deriv (fun (y : 𝕜) ↦ c y • f y) x = c x • deriv f x + deriv c x • f x

Tactic:
(hc.hasDerivAt.smul hf.hasDerivAt).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.smul
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableAt 𝕜 c x
hf : DifferentiableAt 𝕜 f x
⊢ deriv (c • f) x = c x • deriv f x + deriv c x • f x

Tactic:
(hc.hasDerivAt.smul hf.hasDerivAt).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.smul
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasStrictDerivAt c c' x
f : F
⊢ HasStrictDerivAt (HSMul.hSMul (β := 𝕜 → F) c fun (x : 𝕜) ↦ f) (HSMul.hSMul (β := F) (c x) 0 + c' • f) x

Tactic:
have := hc.smul (hasStrictDerivAt_const x f)
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasStrictDerivAt c c' x
f : F
this : HasStrictDerivAt (HSMul.hSMul (β := 𝕜 → F) c fun (x : 𝕜) ↦ f) (HSMul.hSMul (β := F) (c x) 0 + c' • f) x
rwa :
  ∀ (this : HasStrictDerivAt (HSMul.hSMul (β := 𝕜 → F) c fun (x : 𝕜) ↦ f) (0 + c' • f) x),
    HasStrictDerivAt (fun (y : 𝕜) ↦ c y • f) (c' • f) x
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : HasStrictDerivAt (HSMul.hSMul (β := 𝕜 → F) c fun (x : 𝕜) ↦ f) (c' • f) x),
    HasStrictDerivAt (fun (y : 𝕜) ↦ c y • f) (c' • f) x
⊢ HasStrictDerivAt (fun (y : 𝕜) ↦ c y • f) (c' • f) x

Tactic:
rwa [smul_zero, zero_add] at this

Premises used: smul_zero, zero_add
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' s x
f : F
⊢ HasDerivWithinAt (HSMul.hSMul (β := 𝕜 → F) c fun (x : 𝕜) ↦ f) (HSMul.hSMul (β := F) (c x) 0 + c' • f) s x

Tactic:
have := hc.smul (hasDerivWithinAt_const x s f)
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' s x
f : F
this : HasDerivWithinAt (HSMul.hSMul (β := 𝕜 → F) c fun (x : 𝕜) ↦ f) (HSMul.hSMul (β := F) (c x) 0 + c' • f) s x
rwa :
  ∀ (this : HasDerivWithinAt (HSMul.hSMul (β := 𝕜 → F) c fun (x : 𝕜) ↦ f) (0 + c' • f) s x),
    HasDerivWithinAt (fun (y : 𝕜) ↦ c y • f) (c' • f) s x
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : HasDerivWithinAt (HSMul.hSMul (β := 𝕜 → F) c fun (x : 𝕜) ↦ f) (c' • f) s x),
    HasDerivWithinAt (fun (y : 𝕜) ↦ c y • f) (c' • f) s x
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ c y • f) (c' • f) s x

Tactic:
rwa [smul_zero, zero_add] at this

Premises used: smul_zero, zero_add
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivAt c c' x
f : F
rw : ∀ (hc : HasDerivWithinAt c c' univ x) (f : F), HasDerivWithinAt (fun (y : 𝕜) ↦ c y • f) (c' • f) univ x
⊢ HasDerivAt (fun (y : 𝕜) ↦ c y • f) (c' • f) x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Premises used: hasDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' univ x
f : F
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ c y • f) (c' • f) univ x

Tactic:
hc.smul_const f

Premises used: HasDerivWithinAt.smul_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' univ x
f : F
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ c y • f) (c' • f) univ x

Tactic:
exact hc.smul_const f

Premises used: HasDerivWithinAt.smul_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
f : F
pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c y • f) s x = derivWithin c s x • f
neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c y • f) s x = derivWithin c s x • f
⊢ derivWithin (fun (y : 𝕜) ↦ c y • f) s x = derivWithin c s x • f

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Premises used: UniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
f : F
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y • f) s x = derivWithin c s x • f

Tactic:
(hc.hasDerivWithinAt.smul_const f).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.smul_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
f : F
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y • f) s x = derivWithin c s x • f

Tactic:
exact (hc.hasDerivWithinAt.smul_const f).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.smul_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
f : F
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y • f) s x = derivWithin c s x • f

Tactic:
simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

Premises used: derivWithin_zero_of_not_uniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_2
inst_3 : NormedRing 𝕜'
inst_4 : NormedAlgebra 𝕜 𝕜'
inst_5 : Module 𝕜' F
inst_6 : IsBoundedSMul 𝕜' F
inst_7 : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableAt 𝕜 c x
f : F
⊢ deriv (fun (y : 𝕜) ↦ c y • f) x = deriv c x • f

Tactic:
(hc.hasDerivAt.smul_const f).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.smul_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
R : Type u_2
inst_3 : Monoid R
inst_4 : DistribMulAction R F
inst_5 : SMulCommClass 𝕜 R F
inst_6 : ContinuousConstSMul R F
c : R
hf : HasStrictDerivAt f f' x
⊢ HasStrictDerivAt (c • f) (c • f') x

Tactic:
simpa using (HasStrictFDerivAt.const_smul hf c).hasStrictDerivAt

Premises used: HasStrictFDerivAt.const_smul, HasStrictFDerivAt.hasStrictDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
L : Filter (𝕜 × 𝕜)
R : Type u_2
inst_3 : Monoid R
inst_4 : DistribMulAction R F
inst_5 : SMulCommClass 𝕜 R F
inst_6 : ContinuousConstSMul R F
c : R
hf : HasDerivAtFilter f f' L
⊢ HasDerivAtFilter (c • f) (c • f') L

Tactic:
simpa using (HasFDerivAtFilter.const_smul hf c).hasDerivAtFilter

Premises used: HasFDerivAtFilter.const_smul, HasFDerivAtFilter.hasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
R : Type u_2
inst_3 : Monoid R
inst_4 : DistribMulAction R F
inst_5 : SMulCommClass 𝕜 R F
inst_6 : ContinuousConstSMul R F
c : R
hf : HasDerivWithinAt f f' s x
⊢ HasDerivWithinAt (c • f) (c • f') s x

Tactic:
HasDerivAtFilter.const_smul c hf

Premises used: HasDerivAtFilter.const_smul, HasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
R : Type u_2
inst_3 : Monoid R
inst_4 : DistribMulAction R F
inst_5 : SMulCommClass 𝕜 R F
inst_6 : ContinuousConstSMul R F
c : R
hf : HasDerivAt f f' x
⊢ HasDerivAt (c • f) (c • f') x

Tactic:
HasDerivAtFilter.const_smul c hf

Premises used: HasDerivAt, HasDerivAtFilter.const_smul
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
R : Type u_2
inst_3 : Monoid R
inst_4 : DistribMulAction R F
inst_5 : SMulCommClass 𝕜 R F
inst_6 : ContinuousConstSMul R F
c : R
hf : DifferentiableWithinAt 𝕜 f s x
pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c • f y) s x = c • derivWithin f s x
neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c • f y) s x = c • derivWithin f s x
⊢ derivWithin (fun (y : 𝕜) ↦ c • f y) s x = c • derivWithin f s x

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Premises used: UniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
R : Type u_2
inst_3 : Monoid R
inst_4 : DistribMulAction R F
inst_5 : SMulCommClass 𝕜 R F
inst_6 : ContinuousConstSMul R F
c : R
hf : DifferentiableWithinAt 𝕜 f s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ c • f y) s x = c • derivWithin f s x

Tactic:
(hf.hasDerivWithinAt.const_smul c).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.const_smul
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
R : Type u_2
inst_3 : Monoid R
inst_4 : DistribMulAction R F
inst_5 : SMulCommClass 𝕜 R F
inst_6 : ContinuousConstSMul R F
c : R
hf : DifferentiableWithinAt 𝕜 f s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ c • f y) s x = c • derivWithin f s x

Tactic:
exact (hf.hasDerivWithinAt.const_smul c).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.const_smul
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
R : Type u_2
inst_3 : Monoid R
inst_4 : DistribMulAction R F
inst_5 : SMulCommClass 𝕜 R F
inst_6 : ContinuousConstSMul R F
c : R
hf : DifferentiableWithinAt 𝕜 f s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ c • f y) s x = c • derivWithin f s x

Tactic:
simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

Premises used: derivWithin_zero_of_not_uniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
R : Type u_2
inst_3 : Monoid R
inst_4 : DistribMulAction R F
inst_5 : SMulCommClass 𝕜 R F
inst_6 : ContinuousConstSMul R F
c : R
hf : DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin (c • f) s x = c • derivWithin f s x

Tactic:
derivWithin_fun_const_smul c hf

Premises used: derivWithin_fun_const_smul
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕝 : Type u_3
inst_3 : DivisionSemiring 𝕝
inst_4 : Module 𝕝 F
inst_5 : SMulCommClass 𝕜 𝕝 F
inst_6 : ContinuousConstSMul 𝕝 F
c : 𝕝
f : 𝕜 → F
pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c • f y) s x = c • derivWithin f s x
neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c • f y) s x = c • derivWithin f s x
⊢ derivWithin (fun (y : 𝕜) ↦ c • f y) s x = c • derivWithin f s x

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Premises used: UniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕝 : Type u_3
inst_3 : DivisionSemiring 𝕝
inst_4 : Module 𝕝 F
inst_5 : SMulCommClass 𝕜 𝕝 F
inst_6 : ContinuousConstSMul 𝕝 F
c : 𝕝
f : 𝕜 → F
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ c • f y) s x = c • derivWithin f s x

Tactic:
simp [← fderivWithin_derivWithin, ← Pi.smul_def, fderivWithin_const_smul_field c hsx]

Premises used: fderivWithin_derivWithin, fderivWithin_const_smul_field, Pi.smul_def
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕝 : Type u_3
inst_3 : DivisionSemiring 𝕝
inst_4 : Module 𝕝 F
inst_5 : SMulCommClass 𝕜 𝕝 F
inst_6 : ContinuousConstSMul 𝕝 F
c : 𝕝
f : 𝕜 → F
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ c • f y) s x = c • derivWithin f s x

Tactic:
simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

Premises used: derivWithin_zero_of_not_uniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
𝕝 : Type u_3
inst_3 : DivisionSemiring 𝕝
inst_4 : Module 𝕝 F
inst_5 : SMulCommClass 𝕜 𝕝 F
inst_6 : ContinuousConstSMul 𝕝 F
c : 𝕝
f : 𝕜 → F
⊢ derivWithin (c • f) s x = c • derivWithin f s x

Tactic:
derivWithin_fun_const_smul_field c f

Premises used: derivWithin_fun_const_smul_field
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
R : Type u_2
inst_3 : Monoid R
inst_4 : DistribMulAction R F
inst_5 : SMulCommClass 𝕜 R F
inst_6 : ContinuousConstSMul R F
c : R
hf : DifferentiableAt 𝕜 f x
⊢ deriv (fun (y : 𝕜) ↦ c • f y) x = c • deriv f x

Tactic:
(hf.hasDerivAt.const_smul c).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.const_smul