awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact hd.const_mul c

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

Tactic:
simpa only [mul_one] using (hasDerivAt_id' x).const_mul c

Premises used: hasDerivAt_id', HasDerivAt.const_mul, mul_one
-- 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 : HasStrictDerivAt d d' x
⊢ HasStrictDerivAt ((fun (x : 𝕜) ↦ c) * d) (0 * d x + c * d') x

Tactic:
(hasStrictDerivAt_const _ _).mul hd

Premises used: HasStrictDerivAt.mul
-- 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 : HasStrictDerivAt d d' x
h : c * d' = 0 * d x + c * d'
⊢ HasStrictDerivAt (fun (y : 𝕜) ↦ c * d y) (c * d') x

Tactic:
convert! (hasStrictDerivAt_const _ _).mul hd using 1

Premises used: HasStrictDerivAt.mul
-- 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 : HasStrictDerivAt d d' 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 : 𝕜
s : Set 𝕜
𝔸 : Type u_3
inst_1 : NormedRing 𝔸
inst_2 : NormedAlgebra 𝕜 𝔸
d : 𝕜 → 𝔸
c : 𝔸
hd : DifferentiableWithinAt 𝕜 d s x
pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c * d y) s x = c * derivWithin d s x
neg : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ c * d y) s x = c * derivWithin d s x
⊢ derivWithin (fun (y : 𝕜) ↦ c * d y) s x = c * 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 𝕜 𝔸
d : 𝕜 → 𝔸
c : 𝔸
hd : DifferentiableWithinAt 𝕜 d s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ c * d y) s x = c * derivWithin d s x

Tactic:
(hd.hasDerivWithinAt.const_mul c).derivWithin hsx

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

Tactic:
exact (hd.hasDerivWithinAt.const_mul c).derivWithin hsx

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

Tactic:
apply derivWithin_const_smul_field (c := u)

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

Tactic:
(hd.hasDerivAt.const_mul c).deriv

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

Tactic:
simpa only [← derivWithin_univ] using derivWithin_const_mul_field u

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

Tactic:
funext fun _ => deriv_const_mul_field u

Premises used: deriv_const_mul_field, funext
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x c : 𝕜
⊢ deriv (fun (y : 𝕜) ↦ c * y) x = c

Tactic:
simp only [deriv_const_mul c differentiableAt_fun_id, deriv_id'', mul_one]

Premises used: deriv_id'', differentiableAt_fun_id, deriv_const_mul, mul_one
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
c x : 𝕜
⊢ deriv (fun (x : 𝕜) ↦ c * x) x = c

Tactic:
simp only [deriv_const_mul_id]

Premises used: deriv_const_mul_id
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasDerivAt (f i) (f' i) x
⊢ HasDerivAt.{u, u_3} (F := 𝔸') (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x)
    (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (f' i)) x

Tactic:
simpa [ContinuousLinearMap.sum_apply, ContinuousLinearMap.smul_apply] using
    (HasFDerivAt.finsetProd (fun i hi ↦ (hf i hi).hasFDerivAt)).hasDerivAt

Premises used: ContinuousLinearMap.smul_apply, ContinuousLinearMap.sum_apply, HasDerivAt.hasFDerivAt, HasFDerivAt.finsetProd, HasFDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasDerivAt (f i) (f' i) x
⊢ HasDerivAt.{u, u_3} (F := 𝔸') (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x)
    (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (f' i)) x

Tactic:
HasDerivAt.fun_finsetProd hf

Premises used: HasDerivAt.fun_finsetProd
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasDerivAt (f i) (f' i) x
h : ∀ (x : 𝕜), Eq.{u_3 + 1} (α := 𝔸') ((∏ i ∈ u, f i) x) (∏ i ∈ u, f i x)
⊢ HasDerivAt.{u, u_3} (F := 𝔸') (∏ i ∈ u, f i) (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (f' i)) x

Tactic:
convert! HasDerivAt.fun_finsetProd hf

Premises used: HasDerivAt.fun_finsetProd
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasDerivAt (f i) (f' i) x
x_1 : 𝕜
⊢ Eq.{u_3 + 1} (α := 𝔸') ((∏ i ∈ u, f i) x_1) (∏ i ∈ u, f i x_1)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x
⊢ HasDerivWithinAt.{u, u_3} (F := 𝔸') (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x)
    (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (f' i)) s x

Tactic:
simpa [ContinuousLinearMap.sum_apply, ContinuousLinearMap.smul_apply] using
    (HasFDerivWithinAt.finsetProd (fun i hi ↦ (hf i hi).hasFDerivWithinAt)).hasDerivWithinAt

Premises used: ContinuousLinearMap.smul_apply, ContinuousLinearMap.sum_apply, HasDerivWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.hasDerivWithinAt, HasFDerivWithinAt.finsetProd
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x
⊢ HasDerivWithinAt.{u, u_3} (F := 𝔸') (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x)
    (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (f' i)) s x

Tactic:
HasDerivWithinAt.fun_finsetProd hf

Premises used: HasDerivWithinAt.fun_finsetProd
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x
h : ∀ (x : 𝕜), Eq.{u_3 + 1} (α := 𝔸') ((∏ i ∈ u, f i) x) (∏ i ∈ u, f i x)
⊢ HasDerivWithinAt.{u, u_3} (F := 𝔸') (∏ i ∈ u, f i) (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (f' i)) s
    x

Tactic:
convert! HasDerivWithinAt.fun_finsetProd hf

Premises used: HasDerivWithinAt.fun_finsetProd
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x
x_1 : 𝕜
⊢ Eq.{u_3 + 1} (α := 𝔸') ((∏ i ∈ u, f i) x_1) (∏ i ∈ u, f i x_1)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasStrictDerivAt (f i) (f' i) x
⊢ HasStrictDerivAt.{u, u_3} (F := 𝔸') (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x)
    (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (f' i)) x

Tactic:
simpa [ContinuousLinearMap.sum_apply, ContinuousLinearMap.smul_apply] using
    (HasStrictFDerivAt.finsetProd (fun i hi ↦ (hf i hi).hasStrictFDerivAt)).hasStrictDerivAt

Premises used: ContinuousLinearMap.smul_apply, ContinuousLinearMap.sum_apply, HasStrictDerivAt.hasStrictFDerivAt, HasStrictFDerivAt.hasStrictDerivAt, HasStrictFDerivAt.finsetProd
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasStrictDerivAt (f i) (f' i) x
⊢ HasStrictDerivAt.{u, u_3} (F := 𝔸') (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x)
    (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (f' i)) x

Tactic:
HasStrictDerivAt.fun_finsetProd hf

Premises used: HasStrictDerivAt.fun_finsetProd
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasStrictDerivAt (f i) (f' i) x
h : ∀ (x : 𝕜), Eq.{u_3 + 1} (α := 𝔸') ((∏ i ∈ u, f i) x) (∏ i ∈ u, f i x)
⊢ HasStrictDerivAt.{u, u_3} (F := 𝔸') (∏ i ∈ u, f i) (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (f' i)) x

Tactic:
convert! HasStrictDerivAt.fun_finsetProd hf

Premises used: HasStrictDerivAt.fun_finsetProd
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
f' : ι → 𝔸'
hf : ∀ i ∈ u, HasStrictDerivAt (f i) (f' i) x
x_1 : 𝕜
⊢ Eq.{u_3 + 1} (α := 𝔸') ((∏ i ∈ u, f i) x_1) (∏ i ∈ u, f i x_1)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hf : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x
⊢ Eq.{u_3 + 1} (α := 𝔸') (deriv (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) x)
    (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (deriv (f i) x))

Tactic:
(HasDerivAt.fun_finsetProd fun i hi ↦ (hf i hi).hasDerivAt).deriv

Premises used: HasDerivAt.fun_finsetProd, DifferentiableAt.hasDerivAt, HasDerivAt.deriv
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hf : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x
⊢ Eq.{u_3 + 1} (α := 𝔸') (deriv (∏ i ∈ u, f i) x)
    (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (deriv (f i) x))

Tactic:
(HasDerivAt.finsetProd fun i hi ↦ (hf i hi).hasDerivAt).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.finsetProd
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    Eq.{u_3 + 1} (α := 𝔸') (derivWithin (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) s x)
      (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (derivWithin (f i) s x))
neg :
  ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
    Eq.{u_3 + 1} (α := 𝔸') (derivWithin (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) s x)
      (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (derivWithin (f i) s x))
⊢ Eq.{u_3 + 1} (α := 𝔸') (derivWithin (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) s x)
    (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (derivWithin (f i) 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_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ Eq.{u_3 + 1} (α := 𝔸') (derivWithin (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) s x)
    (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (derivWithin (f i) s x))

Tactic:
(HasDerivWithinAt.fun_finsetProd fun i hi ↦ (hf i hi).hasDerivWithinAt).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.fun_finsetProd
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ Eq.{u_3 + 1} (α := 𝔸') (derivWithin (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) s x)
    (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (derivWithin (f i) s x))

Tactic:
exact (HasDerivWithinAt.fun_finsetProd fun i hi ↦ (hf i hi).hasDerivWithinAt).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.fun_finsetProd
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ Eq.{u_3 + 1} (α := 𝔸') (derivWithin (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) s x)
    (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (derivWithin (f i) 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_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
⊢ Eq.{u_3 + 1} (α := 𝔸') (derivWithin (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) s x)
    (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (derivWithin (f i) s x))

Tactic:
derivWithin_fun_finsetProd hf

Premises used: derivWithin_fun_finsetProd
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
h : ∀ (x : 𝕜), Eq.{u_3 + 1} (α := 𝔸') ((∏ i ∈ u, f i) x) (∏ i ∈ u, f i x)
⊢ Eq.{u_3 + 1} (α := 𝔸') (derivWithin (∏ i ∈ u, f i) s x)
    (∑ i ∈ u, HSMul.hSMul (α := 𝔸') (∏ j ∈ u.erase i, f j x) (derivWithin (f i) s x))

Tactic:
convert! derivWithin_fun_finsetProd hf

Premises used: derivWithin_fun_finsetProd
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
inst_1 : DecidableEq ι
𝔸' : Type u_3
inst_2 : NormedCommRing 𝔸'
inst_3 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
x_1 : 𝕜
⊢ Eq.{u_3 + 1} (α := 𝔸') ((∏ i ∈ u, f i) x_1) (∏ i ∈ u, f i x_1)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
𝔸' : Type u_3
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x
⊢ DifferentiableAt.{u, u, u_3} 𝕜 (F := 𝔸') (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) x

Tactic:
(HasDerivAt.fun_finsetProd (fun i hi ↦ DifferentiableAt.hasDerivAt (hd i hi))).differentiableAt

Premises used: HasDerivAt.fun_finsetProd, DifferentiableAt.hasDerivAt, HasDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
𝔸' : Type u_3
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x
⊢ DifferentiableAt.{u, u, u_3} 𝕜 (F := 𝔸') (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) x

Tactic:
exact
    (HasDerivAt.fun_finsetProd (fun i hi ↦ DifferentiableAt.hasDerivAt (hd i hi))).differentiableAt

Premises used: HasDerivAt.fun_finsetProd, DifferentiableAt.hasDerivAt, HasDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
𝔸' : Type u_3
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x
⊢ DifferentiableAt.{u, u, u_3} 𝕜 (F := 𝔸') (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) x

Tactic:
classical
  exact
    (HasDerivAt.fun_finsetProd (fun i hi ↦ DifferentiableAt.hasDerivAt (hd i hi))).differentiableAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
𝔸' : Type u_3
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x
⊢ DifferentiableAt.{u, u, u_3} 𝕜 (F := 𝔸') (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) x

Tactic:
DifferentiableAt.fun_finsetProd hd

Premises used: DifferentiableAt.fun_finsetProd
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
𝔸' : Type u_3
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x
h : ∀ (x : 𝕜), Eq.{u_3 + 1} (α := 𝔸') ((∏ i ∈ u, f i) x) (∏ i ∈ u, f i x)
⊢ DifferentiableAt.{u, u, u_3} 𝕜 (F := 𝔸') (∏ i ∈ u, f i) x

Tactic:
convert! DifferentiableAt.fun_finsetProd hd

Premises used: DifferentiableAt.fun_finsetProd
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
ι : Type u_2
𝔸' : Type u_3
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x
x_1 : 𝕜
⊢ Eq.{u_3 + 1} (α := 𝔸') ((∏ i ∈ u, f i) x_1) (∏ i ∈ u, f i x_1)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
𝔸' : Type u_3
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
⊢ DifferentiableWithinAt.{u, u, u_3} 𝕜 (F := 𝔸') (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) s x

Tactic:
(HasDerivWithinAt.fun_finsetProd (fun i hi ↦
    DifferentiableWithinAt.hasDerivWithinAt (hd i hi))).differentiableWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.fun_finsetProd, HasDerivWithinAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
𝔸' : Type u_3
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
⊢ DifferentiableWithinAt.{u, u, u_3} 𝕜 (F := 𝔸') (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) s x

Tactic:
exact (HasDerivWithinAt.fun_finsetProd (fun i hi ↦
    DifferentiableWithinAt.hasDerivWithinAt (hd i hi))).differentiableWithinAt

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.fun_finsetProd, HasDerivWithinAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
𝔸' : Type u_3
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
⊢ DifferentiableWithinAt.{u, u, u_3} 𝕜 (F := 𝔸') (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) s x

Tactic:
classical
  exact (HasDerivWithinAt.fun_finsetProd (fun i hi ↦
    DifferentiableWithinAt.hasDerivWithinAt (hd i hi))).differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
𝔸' : Type u_3
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
⊢ DifferentiableWithinAt.{u, u, u_3} 𝕜 (F := 𝔸') (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) s x

Tactic:
DifferentiableWithinAt.fun_finsetProd hd

Premises used: DifferentiableWithinAt.fun_finsetProd
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
𝔸' : Type u_3
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
h : ∀ (x : 𝕜), Eq.{u_3 + 1} (α := 𝔸') ((∏ i ∈ u, f i) x) (∏ i ∈ u, f i x)
⊢ DifferentiableWithinAt.{u, u, u_3} 𝕜 (F := 𝔸') (∏ i ∈ u, f i) s x

Tactic:
convert! DifferentiableWithinAt.fun_finsetProd hd

Premises used: DifferentiableWithinAt.fun_finsetProd
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
𝔸' : Type u_3
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
x_1 : 𝕜
⊢ Eq.{u_3 + 1} (α := 𝔸') ((∏ i ∈ u, f i) x_1) (∏ i ∈ u, f i x_1)

Tactic:
simp