awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
s : Set 𝕜
ι : Type u_2
𝔸' : Type u_3
inst_1 : NormedCommRing 𝔸'
inst_2 : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hd : ∀ i ∈ u, DifferentiableOn 𝕜 (f i) s
⊢ DifferentiableOn.{u, u, u_3} 𝕜 (F := 𝔸') (fun (x : 𝕜) ↦ ∏ i ∈ u, f i x) s

Tactic:
fun x hx ↦ .fun_finsetProd (fun i hi ↦ hd i hi x hx)

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

Tactic:
fun x hx ↦ .finsetProd (fun i hi ↦ hd i hi x hx)

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

Tactic:
fun x ↦ .fun_finsetProd (fun i hi ↦ hd i hi x)

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

Tactic:
fun x ↦ .finsetProd (fun i hi ↦ hd i hi x)

Premises used: Differentiable, DifferentiableAt.finsetProd
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivAt c c' x
d : 𝕜'
⊢ HasDerivAt (fun (x : 𝕜) ↦ c x / d) (c' / d) x

Tactic:
simpa only [div_eq_mul_inv] using hc.mul_const d⁻¹

Premises used: div_eq_mul_inv, Inv.inv, HasDerivAt.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 𝕜 𝕜'
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' s x
d : 𝕜'
⊢ HasDerivWithinAt (fun (x : 𝕜) ↦ c x / d) (c' / d) s x

Tactic:
simpa only [div_eq_mul_inv] using hc.mul_const d⁻¹

Premises used: div_eq_mul_inv, Inv.inv, HasDerivWithinAt.mul_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasStrictDerivAt c c' x
d : 𝕜'
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ c x / d) (c' / d) x

Tactic:
simpa only [div_eq_mul_inv] using hc.mul_const d⁻¹

Premises used: HasStrictDerivAt.mul_const, div_eq_mul_inv, Inv.inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
d : 𝕜'
⊢ DifferentiableWithinAt.{u, u, u_2} 𝕜 (F := 𝕜') (fun (x : 𝕜) ↦ c x / d) s x

Tactic:
(hc.hasDerivWithinAt.div_const _).differentiableWithinAt

Premises used: HasDerivWithinAt.div_const, DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c : 𝕜 → 𝕜'
hc : DifferentiableAt 𝕜 c x
d : 𝕜'
⊢ DifferentiableAt.{u, u, u_2} 𝕜 (F := 𝕜') (fun (x : 𝕜) ↦ c x / d) x

Tactic:
(hc.hasDerivAt.div_const _).differentiableAt

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.differentiableAt, HasDerivAt.div_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c : 𝕜 → 𝕜'
hc : DifferentiableOn 𝕜 c s
d : 𝕜'
⊢ DifferentiableOn.{u, u, u_2} 𝕜 (F := 𝕜') (fun (x : 𝕜) ↦ c x / d) s

Tactic:
fun x hx => (hc x hx).div_const d

Premises used: DifferentiableWithinAt.div_const, DifferentiableOn
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c : 𝕜 → 𝕜'
hc : Differentiable 𝕜 c
d : 𝕜'
⊢ Differentiable.{u, u, u_2} 𝕜 (F := 𝕜') fun (x : 𝕜) ↦ c x / d

Tactic:
fun x => (hc x).div_const d

Premises used: Differentiable, DifferentiableAt.div_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c : 𝕜 → 𝕜'
d : 𝕜'
⊢ derivWithin (fun (x : 𝕜) ↦ c x / d) s x = derivWithin c s x / d

Tactic:
simp [div_eq_mul_inv, derivWithin_mul_const_field]

Premises used: derivWithin_mul_const_field, div_eq_mul_inv
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
𝕜' : Type u_2
inst_1 : NormedDivisionRing 𝕜'
inst_2 : NormedAlgebra 𝕜 𝕜'
c : 𝕜 → 𝕜'
d : 𝕜'
⊢ deriv (fun (x : 𝕜) ↦ c x / d) x = deriv c x / d

Tactic:
simp only [div_eq_mul_inv, deriv_mul_const_field]

Premises used: deriv_mul_const_field, div_eq_mul_inv
-- 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
x : 𝕜
G : Type u_2
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
d' : E →L[𝕜] F
hc : HasStrictDerivAt c c' x
hd : HasStrictDerivAt d d' x
⊢ HasStrictDerivAt (fun (y : 𝕜) ↦ c y ∘SL d y) (c' ∘SL d x + c x ∘SL d') x

Tactic:
simpa [add_comm] using (hc.hasStrictFDerivAt.clm_comp hd.hasStrictFDerivAt).hasStrictDerivAt

Premises used: HasStrictDerivAt.hasStrictFDerivAt, add_comm, HasStrictFDerivAt.hasStrictDerivAt, HasStrictFDerivAt.clm_comp
-- 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
x : 𝕜
s : Set 𝕜
G : Type u_2
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
d' : E →L[𝕜] F
hc : HasDerivWithinAt c c' s x
hd : HasDerivWithinAt d d' s x
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ c y ∘SL d y) (c' ∘SL d x + c x ∘SL d') s x

Tactic:
simpa [add_comm] using (hc.hasFDerivWithinAt.clm_comp hd.hasFDerivWithinAt).hasDerivWithinAt

Premises used: HasDerivWithinAt.hasFDerivWithinAt, add_comm, HasFDerivWithinAt.hasDerivWithinAt, HasFDerivWithinAt.clm_comp
-- 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
x : 𝕜
G : Type u_2
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
d' : E →L[𝕜] F
hc : HasDerivAt c c' x
hd : HasDerivAt d d' x
rw :
  ∀ (hc : HasDerivWithinAt c c' univ x) (hd : HasDerivWithinAt d d' univ x),
    HasDerivWithinAt (fun (y : 𝕜) ↦ c y ∘SL d y) (c' ∘SL d x + c x ∘SL d') univ x
⊢ HasDerivAt (fun (y : 𝕜) ↦ c y ∘SL d y) (c' ∘SL d x + c x ∘SL d') 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
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
x : 𝕜
G : Type u_2
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
d' : E →L[𝕜] F
hc : HasDerivWithinAt c c' univ x
hd : HasDerivWithinAt d d' univ x
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ c y ∘SL d y) (c' ∘SL d x + c x ∘SL d') univ x

Tactic:
hc.clm_comp hd

Premises used: HasDerivWithinAt.clm_comp
-- 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
x : 𝕜
G : Type u_2
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
d' : E →L[𝕜] F
hc : HasDerivWithinAt c c' univ x
hd : HasDerivWithinAt d d' univ x
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ c y ∘SL d y) (c' ∘SL d x + c x ∘SL d') univ x

Tactic:
exact hc.clm_comp hd

Premises used: HasDerivWithinAt.clm_comp
-- 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
x : 𝕜
s : Set 𝕜
G : Type u_2
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    derivWithin (fun (y : 𝕜) ↦ c y ∘SL d y) s x = derivWithin c s x ∘SL d x + c x ∘SL derivWithin d s x
neg :
  ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
    derivWithin (fun (y : 𝕜) ↦ c y ∘SL d y) s x = derivWithin c s x ∘SL d x + c x ∘SL derivWithin d s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y ∘SL d y) s x = derivWithin c s x ∘SL d x + c x ∘SL 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 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
x : 𝕜
s : Set 𝕜
G : Type u_2
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y ∘SL d y) s x = derivWithin c s x ∘SL d x + c x ∘SL derivWithin d s x

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

Premises used: HasDerivWithinAt.clm_comp, DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin
-- 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
x : 𝕜
s : Set 𝕜
G : Type u_2
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y ∘SL d y) s x = derivWithin c s x ∘SL d x + c x ∘SL derivWithin d s x

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

Premises used: HasDerivWithinAt.clm_comp, DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin
-- 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
x : 𝕜
s : Set 𝕜
G : Type u_2
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
hc : DifferentiableWithinAt 𝕜 c s x
hd : DifferentiableWithinAt 𝕜 d s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ c y ∘SL d y) s x = derivWithin c s x ∘SL d x + c x ∘SL 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 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
x : 𝕜
G : Type u_2
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
hc : DifferentiableAt 𝕜 c x
hd : DifferentiableAt 𝕜 d x
⊢ deriv (fun (y : 𝕜) ↦ c y ∘SL d y) x = deriv c x ∘SL d x + c x ∘SL deriv d x

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

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.clm_comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
G : Type u_2
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
u : 𝕜 → F
u' : F
hc : HasStrictDerivAt c c' x
hu : HasStrictDerivAt u u' x
⊢ HasStrictDerivAt (fun (y : 𝕜) ↦ (c y : (a : F) → G) (u y))
    (HAdd.hAdd (α := G) (β := G) ((c' : (a : F) → G) (u x) : G) ((c x : (a : F) → G) u' : G)) x

Tactic:
simpa [add_comm] using (hc.hasStrictFDerivAt.clm_apply hu.hasStrictFDerivAt).hasStrictDerivAt

Premises used: HasStrictDerivAt.hasStrictFDerivAt, add_comm, HasStrictFDerivAt.hasStrictDerivAt, HasStrictFDerivAt.clm_apply
-- 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 𝕜
G : Type u_2
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
u : 𝕜 → F
u' : F
hc : HasDerivWithinAt c c' s x
hu : HasDerivWithinAt u u' s x
⊢ HasDerivWithinAt (fun (y : 𝕜) ↦ (c y : (a : F) → G) (u y))
    (HAdd.hAdd (α := G) (β := G) ((c' : (a : F) → G) (u x) : G) ((c x : (a : F) → G) u' : G)) s x

Tactic:
simpa [add_comm] using (hc.hasFDerivWithinAt.clm_apply hu.hasFDerivWithinAt).hasDerivWithinAt

Premises used: HasFDerivWithinAt.clm_apply, HasDerivWithinAt.hasFDerivWithinAt, add_comm, HasFDerivWithinAt.hasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Mul
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
G : Type u_2
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
u : 𝕜 → F
u' : F
hc : HasDerivAt c c' x
hu : HasDerivAt u u' x
⊢ HasDerivAt (fun (y : 𝕜) ↦ (c y : (a : F) → G) (u y))
    (HAdd.hAdd (α := G) (β := G) ((c' : (a : F) → G) (u x) : G) ((c x : (a : F) → G) u' : G)) x

Tactic:
simpa [add_comm] using (hc.hasFDerivAt.clm_apply hu.hasFDerivAt).hasDerivAt

Premises used: HasFDerivAt.clm_apply, HasDerivAt.hasFDerivAt, add_comm, HasFDerivAt.hasDerivAt
-- 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 𝕜
G : Type u_2
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
u : 𝕜 → F
hc : DifferentiableWithinAt 𝕜 c s x
hu : DifferentiableWithinAt 𝕜 u s x
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    derivWithin (fun (y : 𝕜) ↦ (c y : (a : F) → G) (u y)) s x =
      HAdd.hAdd (α := G) (β := G) ((derivWithin c s x : (a : F) → G) (u x) : G)
        ((c x : (a : F) → G) (derivWithin u s x) : G)
neg :
  ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
    derivWithin (fun (y : 𝕜) ↦ (c y : (a : F) → G) (u y)) s x =
      HAdd.hAdd (α := G) (β := G) ((derivWithin c s x : (a : F) → G) (u x) : G)
        ((c x : (a : F) → G) (derivWithin u s x) : G)
⊢ derivWithin (fun (y : 𝕜) ↦ (c y : (a : F) → G) (u y)) s x =
    HAdd.hAdd (α := G) (β := G) ((derivWithin c s x : (a : F) → G) (u x) : G)
      ((c x : (a : F) → G) (derivWithin u s x) : G)

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 𝕜
G : Type u_2
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
u : 𝕜 → F
hc : DifferentiableWithinAt 𝕜 c s x
hu : DifferentiableWithinAt 𝕜 u s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ (c y : (a : F) → G) (u y)) s x =
    HAdd.hAdd (α := G) (β := G) ((derivWithin c s x : (a : F) → G) (u x) : G)
      ((c x : (a : F) → G) (derivWithin u s x) : G)

Tactic:
(hc.hasDerivWithinAt.clm_apply hu.hasDerivWithinAt).derivWithin hsx

Premises used: HasDerivWithinAt.clm_apply, DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin
-- 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 𝕜
G : Type u_2
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
u : 𝕜 → F
hc : DifferentiableWithinAt 𝕜 c s x
hu : DifferentiableWithinAt 𝕜 u s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ (c y : (a : F) → G) (u y)) s x =
    HAdd.hAdd (α := G) (β := G) ((derivWithin c s x : (a : F) → G) (u x) : G)
      ((c x : (a : F) → G) (derivWithin u s x) : G)

Tactic:
exact (hc.hasDerivWithinAt.clm_apply hu.hasDerivWithinAt).derivWithin hsx

Premises used: HasDerivWithinAt.clm_apply, DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin
-- 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 𝕜
G : Type u_2
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
u : 𝕜 → F
hc : DifferentiableWithinAt 𝕜 c s x
hu : DifferentiableWithinAt 𝕜 u s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ (c y : (a : F) → G) (u y)) s x =
    HAdd.hAdd (α := G) (β := G) ((derivWithin c s x : (a : F) → G) (u x) : G)
      ((c x : (a : F) → G) (derivWithin u s x) : G)

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 : 𝕜
G : Type u_2
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
u : 𝕜 → F
hc : DifferentiableAt 𝕜 c x
hu : DifferentiableAt 𝕜 u x
⊢ deriv (fun (y : 𝕜) ↦ (c y : (a : F) → G) (u y)) x =
    HAdd.hAdd (α := G) (β := G) ((deriv c x : (a : F) → G) (u x) : G) ((c x : (a : F) → G) (deriv u x) : G)

Tactic:
(hc.hasDerivAt.clm_apply hu.hasDerivAt).deriv

Premises used: HasDerivAt.clm_apply, DifferentiableAt.hasDerivAt, HasDerivAt.deriv
-- Module: Mathlib.Analysis.Calculus.Deriv.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y : 𝕜
⊢ HasDerivAt (Function.update (β := fun (i : ι) ↦ 𝕜) x i)
    ((ContinuousLinearMap.pi (φ := fun (i : ι) ↦ 𝕜)
          (Pi.single (M := fun (i : ι) ↦ 𝕜 →L[𝕜] 𝕜) i (ContinuousLinearMap.id 𝕜 𝕜)) :
        (a : 𝕜) → (a : ι) → 𝕜)
      1)
    y

Tactic:
(hasFDerivAt_update x y).hasDerivAt

Premises used: hasFDerivAt_update, HasFDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y : 𝕜
h :
  Eq (α := (x : 𝕜) → (j : ι) → 𝕜) (Pi.single (M := fun (a : ι) ↦ 𝕜) i : (x : 𝕜) → (j : ι) → 𝕜)
    ((⇑(ContinuousLinearMap.pi (φ := fun (i : ι) ↦ 𝕜)
            (Pi.single (M := fun (i : ι) ↦ 𝕜 →L[𝕜] 𝕜) i (ContinuousLinearMap.id 𝕜 𝕜))) :
        (a : 𝕜) → (a : ι) → 𝕜) :
      (a : 𝕜) → (a : ι) → 𝕜)
⊢ HasDerivAt (Function.update (β := fun (a : ι) ↦ 𝕜) x i) (Pi.single (M := fun (a : ι) ↦ 𝕜) i 1) y

Tactic:
convert! (hasFDerivAt_update x y).hasDerivAt

Premises used: hasFDerivAt_update, HasFDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y : 𝕜
h :
  ∀ (z : 𝕜) (j : ι),
    Eq.{u_1 + 1} (α := 𝕜) (Pi.single (M := fun (a : ι) ↦ 𝕜) i z j : 𝕜)
      ((ContinuousLinearMap.pi (φ := fun (i : ι) ↦ 𝕜)
              (Pi.single (M := fun (i : ι) ↦ 𝕜 →L[𝕜] 𝕜) i (ContinuousLinearMap.id 𝕜 𝕜)) :
            (a : 𝕜) → (a : ι) → 𝕜)
          z j :
        𝕜)
⊢ Eq (α := (x : 𝕜) → (j : ι) → 𝕜) (Pi.single (M := fun (a : ι) ↦ 𝕜) i : (x : 𝕜) → (j : ι) → 𝕜)
    ((⇑(ContinuousLinearMap.pi (φ := fun (i : ι) ↦ 𝕜)
            (Pi.single (M := fun (i : ι) ↦ 𝕜 →L[𝕜] 𝕜) i (ContinuousLinearMap.id 𝕜 𝕜))) :
        (a : 𝕜) → (a : ι) → 𝕜) :
      (a : 𝕜) → (a : ι) → 𝕜)

Tactic:
ext z j
-- Module: Mathlib.Analysis.Calculus.Deriv.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y z : 𝕜
j : ι
h :
  (if j = i then z else 0 j) =
    (ContinuousLinearMap.pi (φ := fun (i : ι) ↦ 𝕜)
          (Pi.single (M := fun (i : ι) ↦ 𝕜 →L[𝕜] 𝕜) i (ContinuousLinearMap.id 𝕜 𝕜)) :
        (a : 𝕜) → (a : ι) → 𝕜)
      z j
⊢ Eq.{u_1 + 1} (α := 𝕜) (Pi.single (M := fun (a : ι) ↦ 𝕜) i z j : 𝕜)
    ((ContinuousLinearMap.pi (φ := fun (i : ι) ↦ 𝕜)
            (Pi.single (M := fun (i : ι) ↦ 𝕜 →L[𝕜] 𝕜) i (ContinuousLinearMap.id 𝕜 𝕜)) :
          (a : 𝕜) → (a : ι) → 𝕜)
        z j :
      𝕜)

Tactic:
rw [Pi.single, Function.update_apply]

Premises used: Function.update_apply, Pi.single
-- Module: Mathlib.Analysis.Calculus.Deriv.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y z : 𝕜
j : ι
pos :
  ∀ (h : j = i),
    z =
      (ContinuousLinearMap.pi (φ := fun (i : ι) ↦ 𝕜)
            (Pi.single (M := fun (i : ι) ↦ 𝕜 →L[𝕜] 𝕜) i (ContinuousLinearMap.id 𝕜 𝕜)) :
          (a : 𝕜) → (a : ι) → 𝕜)
        z j
neg :
  ∀ (h : ¬j = i),
    Eq.{u_1 + 1} (α := 𝕜) (0 j : 𝕜)
      ((ContinuousLinearMap.pi (φ := fun (i : ι) ↦ 𝕜)
              (Pi.single (M := fun (i : ι) ↦ 𝕜 →L[𝕜] 𝕜) i (ContinuousLinearMap.id 𝕜 𝕜)) :
            (a : 𝕜) → (a : ι) → 𝕜)
          z j :
        𝕜)
⊢ (if j = i then z else 0 j) =
    (ContinuousLinearMap.pi (φ := fun (i : ι) ↦ 𝕜)
          (Pi.single (M := fun (i : ι) ↦ 𝕜 →L[𝕜] 𝕜) i (ContinuousLinearMap.id 𝕜 𝕜)) :
        (a : 𝕜) → (a : ι) → 𝕜)
      z j

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.Calculus.Deriv.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y z : 𝕜
j : ι
h : j = i
⊢ z =
    (ContinuousLinearMap.pi (φ := fun (i : ι) ↦ 𝕜)
          (Pi.single (M := fun (i : ι) ↦ 𝕜 →L[𝕜] 𝕜) i (ContinuousLinearMap.id 𝕜 𝕜)) :
        (a : 𝕜) → (a : ι) → 𝕜)
      z j

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Calculus.Deriv.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
x : ι → 𝕜
i : ι
y z : 𝕜
j : ι
h : ¬j = i
⊢ Eq.{u_1 + 1} (α := 𝕜) (0 j : 𝕜)
    ((ContinuousLinearMap.pi (φ := fun (i : ι) ↦ 𝕜)
            (Pi.single (M := fun (i : ι) ↦ 𝕜 →L[𝕜] 𝕜) i (ContinuousLinearMap.id 𝕜 𝕜)) :
          (a : 𝕜) → (a : ι) → 𝕜)
        z j :
      𝕜)

Tactic:
simp [Pi.single_eq_of_ne h]

Premises used: Pi.single_eq_of_ne
-- Module: Mathlib.Analysis.Calculus.Deriv.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
i : ι
y : 𝕜
⊢ HasDerivAt (F := (j : ι) → 𝕜) (Pi.single (M := fun (x : ι) ↦ 𝕜) i) (Pi.single (M := fun (j : ι) ↦ 𝕜) i 1) y

Tactic:
hasDerivAt_update 0 i y

Premises used: hasDerivAt_update, Pi.single, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.Deriv.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
inst_2 : Finite ι
x : ι → 𝕜
i : ι
y : 𝕜
⊢ deriv (Function.update (β := fun (a : ι) ↦ 𝕜) x i) y = Pi.single (M := fun (j : ι) ↦ 𝕜) i 1

Tactic:
have := Fintype.ofFinite ι
  (hasDerivAt_update x i y).deriv

Premises used: Fintype.ofFinite, HasDerivAt.deriv, hasDerivAt_update
-- Module: Mathlib.Analysis.Calculus.Deriv.Pi
Goal:
𝕜 : Type u_1
ι : Type u_2
inst : DecidableEq ι
inst_1 : NontriviallyNormedField 𝕜
inst_2 : Finite ι
i : ι
y : 𝕜
⊢ Eq (α := (j : ι) → 𝕜) (deriv (Pi.single (M := fun (x : ι) ↦ 𝕜) i) y) (Pi.single (M := fun (j : ι) ↦ 𝕜) i 1)

Tactic:
deriv_update 0 i y

Premises used: Pi.single, deriv_update, OfNat.ofNat