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
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 (c • f) x = c • deriv f x

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

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.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 : 𝕜
𝕝 : Type u_3
inst_3 : DivisionSemiring 𝕝
inst_4 : Module 𝕝 F
inst_5 : SMulCommClass 𝕜 𝕝 F
inst_6 : ContinuousConstSMul 𝕝 F
c : 𝕝
f : 𝕜 → F
⊢ deriv (fun (y : 𝕜) ↦ c • f y) x = c • deriv f x

Tactic:
simp only [← derivWithin_univ, derivWithin_fun_const_smul_field]

Premises used: derivWithin_fun_const_smul_field, derivWithin_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_3
inst_3 : DivisionSemiring 𝕝
inst_4 : Module 𝕝 F
inst_5 : SMulCommClass 𝕜 𝕝 F
inst_6 : ContinuousConstSMul 𝕝 F
c : 𝕝
f : 𝕜 → F
⊢ deriv (c • f) x = c • deriv f x

Tactic:
simp only [← derivWithin_univ, derivWithin_const_smul_field]

Premises used: derivWithin_univ, derivWithin_const_smul_field
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
c' d' : 𝔸
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
⊢ HasDerivWithinAt (c * d) (c' * d x + c x * d') s x

Tactic:
simpa [add_comm] using (HasFDerivWithinAt.mul' hc hd).hasDerivWithinAt

Premises used: add_comm, HasFDerivWithinAt.hasDerivWithinAt, HasFDerivWithinAt.mul'
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
c' d' : 𝔸
hc : HasDerivAt c c' x
hd : HasDerivAt d d' x
rw :
  ∀ (hc : HasDerivWithinAt c c' univ x) (hd : HasDerivWithinAt d d' univ x),
    HasDerivWithinAt (c * d) (c' * d x + c x * d') univ x
⊢ HasDerivAt (c * d) (c' * d x + c x * d') x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Premises used: hasDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
c' d' : 𝔸
hc : HasDerivWithinAt c c' univ x
hd : HasDerivWithinAt d d' univ x
⊢ HasDerivWithinAt (c * d) (c' * d x + c x * d') univ x

Tactic:
HasDerivWithinAt.mul hc hd

Premises used: HasDerivWithinAt.mul
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
c' d' : 𝔸
hc : HasDerivWithinAt c c' univ x
hd : HasDerivWithinAt d d' univ x
⊢ HasDerivWithinAt (c * d) (c' * d x + c x * d') univ x

Tactic:
exact HasDerivWithinAt.mul hc hd

Premises used: HasDerivWithinAt.mul
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
c' d' : 𝔸
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
⊢ HasStrictDerivAt (c * d) (c' * d x + c x * d') x

Tactic:
simpa [add_comm] using (HasStrictFDerivAt.mul' hc hd).hasStrictDerivAt

Premises used: HasStrictFDerivAt.mul', add_comm, HasStrictFDerivAt.hasStrictDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    derivWithin (fun (y : 𝕜) ↦ c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x
neg :
  ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
    derivWithin (fun (y : 𝕜) ↦ c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Premises used: UniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x

Tactic:
(hc.hasDerivWithinAt.mul hd.hasDerivWithinAt).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.mul, HasDerivWithinAt.derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x

Tactic:
exact (hc.hasDerivWithinAt.mul hd.hasDerivWithinAt).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.mul, HasDerivWithinAt.derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d 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 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
⊢ derivWithin (c * d) s x = derivWithin c s x * d x + c x * derivWithin d s x

Tactic:
derivWithin_fun_mul hc hd

Premises used: derivWithin_fun_mul
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
hc : DifferentiableAt 𝕜 c x
hd : DifferentiableAt 𝕜 d x
⊢ deriv (fun (y : 𝕜) ↦ c y * d y) x = deriv c x * d x + c x * deriv d x

Tactic:
(hc.hasDerivAt.mul hd.hasDerivAt).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.mul
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c d : 𝕜 → 𝔸
hc : DifferentiableAt 𝕜 c x
hd : DifferentiableAt 𝕜 d x
⊢ deriv (c * d) x = deriv c x * d x + c x * deriv d x

Tactic:
(hc.hasDerivAt.mul hd.hasDerivAt).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.mul
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasDerivWithinAt c c' s x
d : 𝔸
⊢ HasDerivWithinAt (c * fun (x : 𝕜) ↦ d) (c' * d + c x * 0) s x

Tactic:
hc.mul (hasDerivWithinAt_const x s d)

Premises used: HasDerivWithinAt.mul, hasDerivWithinAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasDerivWithinAt c c' s x
d : 𝔸
h : c' * d = c' * d + c x * 0
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ c y * d) (c' * d) s x

Tactic:
convert! hc.mul (hasDerivWithinAt_const x s d) using 1

Premises used: HasDerivWithinAt.mul, hasDerivWithinAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasDerivWithinAt c c' s x
d : 𝔸
h : c' * d = c' * d + 0
h₁ h₂ : c' * d = c' * d
⊢ c' * d = c' * d + c x * 0

Tactic:
rw [mul_zero, add_zero]

Premises used: MulZeroClass.mul_zero, add_zero
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasDerivAt c c' x
d : 𝔸
rw : ∀ (hc : HasDerivWithinAt c c' univ x) (d : 𝔸), HasDerivWithinAt (fun (y : 𝕜) ↦ c y * d) (c' * d) univ x
⊢ HasDerivAt (fun (y : 𝕜) ↦ c y * d) (c' * d) x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Premises used: hasDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasDerivWithinAt c c' univ x
d : 𝔸
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ c y * d) (c' * d) univ x

Tactic:
hc.mul_const d

Premises used: HasDerivWithinAt.mul_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasDerivWithinAt c c' univ x
d : 𝔸
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ c y * d) (c' * d) univ x

Tactic:
exact hc.mul_const d

Premises used: HasDerivWithinAt.mul_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x c : 𝕜
⊢ HasDerivAt (fun (x : 𝕜) ↦ x * c) c x

Tactic:
simpa only [one_mul] using (hasDerivAt_id' x).mul_const c

Premises used: hasDerivAt_id', one_mul, HasDerivAt.mul_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasStrictDerivAt c c' x
d : 𝔸
⊢ HasStrictDerivAt (c * fun (x : 𝕜) ↦ d) (c' * d + c x * 0) x

Tactic:
hc.mul (hasStrictDerivAt_const x d)

Premises used: HasStrictDerivAt.mul, hasStrictDerivAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasStrictDerivAt c c' x
d : 𝔸
h : c' * d = c' * d + c x * 0
⊢ HasStrictDerivAt (fun (y : 𝕜) ↦ c y * d) (c' * d) x

Tactic:
convert! hc.mul (hasStrictDerivAt_const x d) using 1

Premises used: HasStrictDerivAt.mul, hasStrictDerivAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
c' : 𝔸
hc : HasStrictDerivAt c c' x
d : 𝔸
h : c' * d = c' * d + 0
h₁ h₂ : c' * d = c' * d
⊢ c' * d = c' * d + c x * 0

Tactic:
rw [mul_zero, add_zero]

Premises used: MulZeroClass.mul_zero, add_zero
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
d : 𝔸
pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c y * d) s x = derivWithin c s x * d
neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c y * d) s x = derivWithin c s x * d
⊢ derivWithin (fun (y : 𝕜) ↦ c y * d) s x = derivWithin c s x * d

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Premises used: UniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
d : 𝔸
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y * d) s x = derivWithin c s x * d

Tactic:
(hc.hasDerivWithinAt.mul_const d).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.mul_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
d : 𝔸
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y * d) s x = derivWithin c s x * d

Tactic:
exact (hc.hasDerivWithinAt.mul_const d).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.mul_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
hc : DifferentiableWithinAt 𝕜 c s x
d : 𝔸
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y * d) s x = derivWithin c s x * d

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 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
pos : ∀ (hv : DifferentiableWithinAt 𝕜 v s x), derivWithin (fun (y : 𝕜) ↦ v y * u) s x = derivWithin v s x * u
neg : ∀ (hv : ¬DifferentiableWithinAt 𝕜 v s x), derivWithin (fun (y : 𝕜) ↦ v y * u) s x = derivWithin v s x * u
⊢ derivWithin (fun (y : 𝕜) ↦ v y * u) s x = derivWithin v s x * u

Tactic:
by_cases hv : DifferentiableWithinAt 𝕜 v s x

Premises used: DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : DifferentiableWithinAt 𝕜 v s x
pos pos₁ : derivWithin v s x * u = derivWithin v s x * u
⊢ derivWithin (fun (y : 𝕜) ↦ v y * u) s x = derivWithin v s x * u

Tactic:
rw [derivWithin_mul_const hv u]

Premises used: derivWithin_mul_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
pos : ∀ (hu : u = 0), derivWithin (fun (y : 𝕜) ↦ v y * u) s x = derivWithin v s x * u
neg : ∀ (hu : ¬u = 0), derivWithin (fun (y : 𝕜) ↦ v y * u) s x = derivWithin v s x * u
⊢ derivWithin (fun (y : 𝕜) ↦ v y * u) s x = derivWithin v s x * u

Tactic:
by_cases hu : u = 0
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : u = 0
⊢ derivWithin (fun (y : 𝕜) ↦ v y * u) s x = derivWithin v s x * u

Tactic:
simp [hu]
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : ¬u = 0
neg : ¬DifferentiableWithinAt.{u, u, u_2} 𝕜 (F := 𝕜') (fun (y : 𝕜) ↦ v y * u) s x
⊢ derivWithin (fun (y : 𝕜) ↦ v y * u) s x = derivWithin v s x * u

Tactic:
rw [derivWithin_zero_of_not_differentiableWithinAt hv, zero_mul,
      derivWithin_zero_of_not_differentiableWithinAt]

Premises used: MulZeroClass.zero_mul, derivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : ¬u = 0
h : ∀ (x : 𝕜), v x = v x * u * u⁻¹
⊢ v = fun (x : 𝕜) ↦ v x * u * u⁻¹

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : ¬u = 0
x_1 : 𝕜
⊢ v x_1 = v x_1 * u * u⁻¹

Tactic:
simp [hu]
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : ¬u = 0
⊢ v = fun (x : 𝕜) ↦ v x * u * u⁻¹

Tactic:
have : v = fun x ↦ (v x * u) * u⁻¹ := by ext; simp [hu]
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : ¬u = 0
this : v = fun (x : 𝕜) ↦ v x * u * u⁻¹
⊢ ¬DifferentiableWithinAt.{u, u, u_2} 𝕜 (F := 𝕜') (fun (y : 𝕜) ↦ v y * u) s x

Tactic:
fun h_diff ↦ hv <| this ▸ h_diff.mul_const _

Premises used: Eq.rec, Inv.inv, Eq.symm, DifferentiableWithinAt.mul_const, Not
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
v : 𝕜 → 𝕜'
u : 𝕜'
hv : ¬DifferentiableWithinAt 𝕜 v s x
hu : ¬u = 0
this : v = fun (x : 𝕜) ↦ v x * u * u⁻¹
⊢ ¬DifferentiableWithinAt.{u, u, u_2} 𝕜 (F := 𝕜') (fun (y : 𝕜) ↦ v y * u) s x

Tactic:
exact fun h_diff ↦ hv <| this ▸ h_diff.mul_const _

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
c : 𝕜 → 𝔸
hc : DifferentiableAt 𝕜 c x
d : 𝔸
⊢ deriv (fun (y : 𝕜) ↦ c y * d) x = deriv c x * d

Tactic:
(hc.hasDerivAt.mul_const d).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.mul_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
u : 𝕜 → 𝕜'
v : 𝕜'
pos : ∀ (hu : DifferentiableAt 𝕜 u x), deriv (fun (y : 𝕜) ↦ u y * v) x = deriv u x * v
neg : ∀ (hu : ¬DifferentiableAt 𝕜 u x), deriv (fun (y : 𝕜) ↦ u y * v) x = deriv u x * v
⊢ deriv (fun (y : 𝕜) ↦ u y * v) x = deriv u x * v

Tactic:
by_cases hu : DifferentiableAt 𝕜 u x

Premises used: DifferentiableAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
u : 𝕜 → 𝕜'
v : 𝕜'
hu : DifferentiableAt 𝕜 u x
⊢ deriv (fun (y : 𝕜) ↦ u y * v) x = deriv u x * v

Tactic:
deriv_mul_const hu v

Premises used: deriv_mul_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
u : 𝕜 → 𝕜'
v : 𝕜'
hu : DifferentiableAt 𝕜 u x
⊢ deriv (fun (y : 𝕜) ↦ u y * v) x = deriv u x * v

Tactic:
exact deriv_mul_const hu v

Premises used: deriv_mul_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
u : 𝕜 → 𝕜'
v : 𝕜'
hu : ¬DifferentiableAt 𝕜 u x
neg : Eq.{u_2 + 1} (α := 𝕜') (deriv (fun (y : 𝕜) ↦ u y * v) x) 0
⊢ deriv (fun (y : 𝕜) ↦ u y * v) x = deriv u x * v

Tactic:
rw [deriv_zero_of_not_differentiableAt hu, zero_mul]

Premises used: deriv_zero_of_not_differentiableAt, MulZeroClass.zero_mul
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
u : 𝕜 → 𝕜'
v : 𝕜'
hu : ¬DifferentiableAt 𝕜 u x
neg : Eq.{u_2 + 1} (α := 𝕜') (deriv (fun (y : 𝕜) ↦ u y * 0) x) 0
neg₁ : ∀ (hd : v ≠ 0), Eq.{u_2 + 1} (α := 𝕜') (deriv (fun (y : 𝕜) ↦ u y * v) x) 0
⊢ Eq.{u_2 + 1} (α := 𝕜') (deriv (fun (y : 𝕜) ↦ u y * v) x) 0

Tactic:
rcases eq_or_ne v 0 with (rfl | hd)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
u : 𝕜 → 𝕜'
hu : ¬DifferentiableAt 𝕜 u x
⊢ Eq.{u_2 + 1} (α := 𝕜') (deriv (fun (y : 𝕜) ↦ u y * 0) x) 0

Tactic:
simp only [mul_zero, deriv_const]

Premises used: MulZeroClass.mul_zero, deriv_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
u : 𝕜 → 𝕜'
v : 𝕜'
hu : ¬DifferentiableAt 𝕜 u x
hd : v ≠ 0
⊢ Eq.{u_2 + 1} (α := 𝕜') (deriv (fun (y : 𝕜) ↦ u y * v) x) 0

Tactic:
deriv_zero_of_not_differentiableAt (mt (fun H => ?_) hu)

Premises used: deriv_zero_of_not_differentiableAt, mt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
u : 𝕜 → 𝕜'
v : 𝕜'
hu : ¬DifferentiableAt 𝕜 u x
hd : v ≠ 0
neg : ∀ (H : DifferentiableAt.{u, u, u_2} 𝕜 (F := 𝕜') (fun (y : 𝕜) ↦ u y * v) x), DifferentiableAt 𝕜 u x
⊢ Eq.{u_2 + 1} (α := 𝕜') (deriv (fun (y : 𝕜) ↦ u y * v) x) 0

Tactic:
refine deriv_zero_of_not_differentiableAt (mt (fun H => ?_) hu)

Premises used: deriv_zero_of_not_differentiableAt, mt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
u : 𝕜 → 𝕜'
v : 𝕜'
hu : ¬DifferentiableAt 𝕜 u x
hd : v ≠ 0
H : DifferentiableAt.{u, u, u_2} 𝕜 (F := 𝕜') (fun (y : 𝕜) ↦ u y * v) x
⊢ DifferentiableAt 𝕜 u x

Tactic:
simpa only [mul_inv_cancel_right₀ hd] using H.mul_const v⁻¹

Premises used: mul_inv_cancel_right₀, DifferentiableAt.mul_const, Inv.inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
u : 𝕜 → 𝕜'
v : 𝕜'
⊢ Eq (α := (x : 𝕜) → 𝕜') (deriv fun (x : 𝕜) ↦ u x * v) fun (x : 𝕜) ↦ deriv u x * v

Tactic:
funext fun _ => deriv_mul_const_field v

Premises used: deriv_mul_const_field, funext
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasDerivWithinAt d d' s x
⊢ HasDerivWithinAt ((fun (x : 𝕜) ↦ c) * d) (0 * d x + c * d') s x

Tactic:
(hasDerivWithinAt_const x s c).mul hd

Premises used: HasDerivWithinAt.mul, hasDerivWithinAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasDerivWithinAt d d' s x
h : c * d' = 0 * d x + c * d'
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ c * d y) (c * d') s x

Tactic:
convert! (hasDerivWithinAt_const x s c).mul hd using 1

Premises used: HasDerivWithinAt.mul, hasDerivWithinAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasDerivWithinAt d d' s x
h : c * d' = 0 + c * d'
h₁ h₂ : c * d' = c * d'
⊢ c * d' = 0 * d x + c * d'

Tactic:
rw [zero_mul, zero_add]

Premises used: MulZeroClass.zero_mul, zero_add
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasDerivAt d d' x
rw : ∀ (hd : HasDerivWithinAt d d' univ x), HasDerivWithinAt (fun (y : 𝕜) ↦ c * d y) (c * d') univ x
⊢ HasDerivAt (fun (y : 𝕜) ↦ c * d y) (c * d') x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Premises used: hasDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
d' c : 𝔸
hd : HasDerivWithinAt d d' univ x
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ c * d y) (c * d') univ x

Tactic:
hd.const_mul c

Premises used: HasDerivWithinAt.const_mul