awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
s : Set E
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
⊢ DifferentiableOn 𝕜 (f + g) s

Tactic:
fun x hx => (hf x hx).add (hg x hx)

Premises used: DifferentiableWithinAt.add, DifferentiableOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
hf : Differentiable 𝕜 f
hg : Differentiable 𝕜 g
⊢ Differentiable 𝕜 (f + g)

Tactic:
fun x => (hf x).add (hg x)

Premises used: Differentiable, DifferentiableAt.add
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
⊢ fderivWithin 𝕜 (f + g) s x = HAdd.hAdd (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 g s x)

Tactic:
(hf.hasFDerivWithinAt.add hg.hasFDerivWithinAt).fderivWithin hxs

Premises used: HasFDerivWithinAt.add, HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
⊢ fderivWithin 𝕜 (fun (y : E) ↦ f y + g y) s x =
    HAdd.hAdd (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 g s x)

Tactic:
fderivWithin_add hxs hf hg

Premises used: fderivWithin_add
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
x : E
hf : DifferentiableAt 𝕜 f x
hg : DifferentiableAt 𝕜 g x
⊢ fderiv 𝕜 (f + g) x = HAdd.hAdd (α := E →L[𝕜] F) (fderiv 𝕜 f x) (fderiv 𝕜 g x)

Tactic:
(hf.hasFDerivAt.add hg.hasFDerivAt).fderiv

Premises used: HasFDerivAt.add, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
x : E
hf : DifferentiableAt 𝕜 f x
hg : DifferentiableAt 𝕜 g x
⊢ fderiv 𝕜 (fun (y : E) ↦ f y + g y) x = HAdd.hAdd (α := E →L[𝕜] F) (fderiv 𝕜 f x) (fderiv 𝕜 g x)

Tactic:
fderiv_add hf hg

Premises used: fderiv_add
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
c : F
⊢ HasFDerivAtFilter (fun (x : E) ↦ f x + c) f' L ↔ HasFDerivAtFilter f f' L

Tactic:
simp [hasFDerivAtFilter_iff_isLittleOTVS]

Premises used: hasFDerivAtFilter_iff_isLittleOTVS
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
c : F
⊢ HasStrictFDerivAt (fun (x : E) ↦ f x + c) f' x ↔ HasStrictFDerivAt f f' x

Tactic:
simp [hasStrictFDerivAt_iff_isLittleO]

Premises used: hasStrictFDerivAt_iff_isLittleO
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
c : F
⊢ HasFDerivWithinAt (fun (x : E) ↦ f x + c) f' s x ↔ HasFDerivWithinAt f f' s x

Tactic:
hasFDerivAtFilter_add_const_iff c

Premises used: HasFDerivWithinAt, hasFDerivAtFilter_add_const_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
c : F
⊢ HasFDerivAt (fun (x : E) ↦ f x + c) f' x ↔ HasFDerivAt f f' x

Tactic:
hasFDerivAtFilter_add_const_iff c

Premises used: HasFDerivAt, hasFDerivAtFilter_add_const_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
c : F
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ f y + c) s x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
exists_congr fun _ ↦ hasFDerivWithinAt_add_const_iff c

Premises used: exists_congr, DifferentiableWithinAt, hasFDerivWithinAt_add_const_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
c : F
⊢ DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ f y + c) x ↔ DifferentiableAt 𝕜 f x

Tactic:
exists_congr fun _ ↦ hasFDerivAt_add_const_iff c

Premises used: DifferentiableAt, hasFDerivAt_add_const_iff, exists_congr
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
c : F
⊢ DifferentiableOn.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ f y + c) s ↔ DifferentiableOn 𝕜 f s

Tactic:
forall₂_congr fun _ _ ↦ differentiableWithinAt_add_const_iff c

Premises used: forall₂_congr, DifferentiableOn, differentiableWithinAt_add_const_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
c : F
⊢ (Differentiable.{u_1, u_2, u_3} 𝕜 (F := F) fun (y : E) ↦ f y + c) ↔ Differentiable 𝕜 f

Tactic:
forall_congr' fun _ ↦ differentiableAt_add_const_iff c

Premises used: Differentiable, differentiableAt_add_const_iff, forall_congr'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
c : F
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (y : E) ↦ f y + c) s x) (fderivWithin 𝕜 f s x)

Tactic:
simp [fderivWithin]

Premises used: fderivWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
c : F
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (y : E) ↦ f y + c) s x) (fderivWithin 𝕜 f s x)

Tactic:
classical simp [fderivWithin]

Premises used: fderivWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
c : F
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (fun (y : E) ↦ f y + c) x) (fderiv 𝕜 f x)

Tactic:
simp only [← fderivWithin_univ, fderivWithin_add_const]

Premises used: fderivWithin_univ, fderivWithin_add_const
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
c : F
⊢ HasFDerivAtFilter (fun (x : E) ↦ c + f x) f' L ↔ HasFDerivAtFilter f f' L

Tactic:
simpa only [add_comm] using hasFDerivAtFilter_add_const_iff c

Premises used: add_comm, hasFDerivAtFilter_add_const_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
c : F
⊢ HasStrictFDerivAt (fun (x : E) ↦ c + f x) f' x ↔ HasStrictFDerivAt f f' x

Tactic:
simpa only [add_comm] using hasStrictFDerivAt_add_const_iff c

Premises used: add_comm, hasStrictFDerivAt_add_const_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
c : F
⊢ HasFDerivWithinAt (fun (x : E) ↦ c + f x) f' s x ↔ HasFDerivWithinAt f f' s x

Tactic:
hasFDerivAtFilter_const_add_iff c

Premises used: HasFDerivWithinAt, hasFDerivAtFilter_const_add_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
c : F
⊢ HasFDerivAt (fun (x : E) ↦ c + f x) f' x ↔ HasFDerivAt f f' x

Tactic:
hasFDerivAtFilter_const_add_iff c

Premises used: HasFDerivAt, hasFDerivAtFilter_const_add_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
c : F
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ c + f y) s x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
exists_congr fun _ ↦ hasFDerivWithinAt_const_add_iff c

Premises used: hasFDerivWithinAt_const_add_iff, exists_congr, DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
c : F
⊢ DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ c + f y) x ↔ DifferentiableAt 𝕜 f x

Tactic:
exists_congr fun _ ↦ hasFDerivAt_const_add_iff c

Premises used: DifferentiableAt, hasFDerivAt_const_add_iff, exists_congr
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
c : F
⊢ DifferentiableOn.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ c + f y) s ↔ DifferentiableOn 𝕜 f s

Tactic:
forall₂_congr fun _ _ ↦ differentiableWithinAt_const_add_iff c

Premises used: forall₂_congr, DifferentiableOn, differentiableWithinAt_const_add_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
c : F
⊢ (Differentiable.{u_1, u_2, u_3} 𝕜 (F := F) fun (y : E) ↦ c + f y) ↔ Differentiable 𝕜 f

Tactic:
forall_congr' fun _ ↦ differentiableAt_const_add_iff c

Premises used: Differentiable, differentiableAt_const_add_iff, forall_congr'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
s : Set E
c : F
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (y : E) ↦ c + f y) s x) (fderivWithin 𝕜 f s x)

Tactic:
simpa only [add_comm] using fderivWithin_add_const c

Premises used: fderivWithin_add_const, add_comm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
c : F
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (fun (y : E) ↦ c + f y) x) (fderiv 𝕜 f x)

Tactic:
simp only [add_comm c, fderiv_add_const]

Premises used: fderiv_add_const, add_comm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, HasStrictFDerivAt (A i) (A' i) x
simp :
  ∀
    (h :
      ∀ i ∈ u,
        IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (nhds (x, x))
          (fun (p : E × E) ↦ HSub.hSub (β := F) (A i p.1 - A i p.2) ((A' i : (a : E) → F) (p.1 - p.2) : F))
          fun (p : E × E) ↦ p.1 - p.2),
    IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (nhds (x, x))
      (fun (p : E × E) ↦
        HSub.hSub (β := F) (HSub.hSub (α := F) (∑ i ∈ u, A i p.1) (∑ i ∈ u, A i p.2))
          ((∑ i ∈ u, A' i : (a : E) → F) (p.1 - p.2) : F))
      fun (p : E × E) ↦ p.1 - p.2
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (y : E) ↦ ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x

Tactic:
simp only [hasStrictFDerivAt_iff_isLittleO] at *

Premises used: hasStrictFDerivAt_iff_isLittleO
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h :
  ∀ i ∈ u,
    IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (nhds (x, x))
      (fun (p : E × E) ↦ HSub.hSub (β := F) (A i p.1 - A i p.2) ((A' i : (a : E) → F) (p.1 - p.2) : F))
      fun (p : E × E) ↦ p.1 - p.2
⊢ IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (nhds (x, x))
    (fun (x : E × E) ↦ ∑ i ∈ u, HSub.hSub (β := F) (A i x.1 - A i x.2) ((A' i : (a : E) → F) (x.1 - x.2) : F))
    fun (p : E × E) ↦ p.1 - p.2

Tactic:
IsLittleO.sum h

Premises used: Asymptotics.IsLittleO.sum
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h :
  ∀ i ∈ u,
    IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (nhds (x, x))
      (fun (p : E × E) ↦ HSub.hSub (β := F) (A i p.1 - A i p.2) ((A' i : (a : E) → F) (p.1 - p.2) : F))
      fun (p : E × E) ↦ p.1 - p.2
h₁ :
  ∀ (x : E × E),
    HSub.hSub (β := F) (HSub.hSub (α := F) (∑ i ∈ u, A i x.1) (∑ i ∈ u, A i x.2))
        ((∑ i ∈ u, A' i : (a : E) → F) (x.1 - x.2) : F) =
      ∑ i ∈ u, HSub.hSub (β := F) (A i x.1 - A i x.2) ((A' i : (a : E) → F) (x.1 - x.2) : F)
⊢ IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (nhds (x, x))
    (fun (p : E × E) ↦
      HSub.hSub (β := F) (HSub.hSub (α := F) (∑ i ∈ u, A i p.1) (∑ i ∈ u, A i p.2))
        ((∑ i ∈ u, A' i : (a : E) → F) (p.1 - p.2) : F))
    fun (p : E × E) ↦ p.1 - p.2

Tactic:
convert! IsLittleO.sum h

Premises used: Asymptotics.IsLittleO.sum
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h :
  ∀ i ∈ u,
    IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (nhds (x, x))
      (fun (p : E × E) ↦ HSub.hSub (β := F) (A i p.1 - A i p.2) ((A' i : (a : E) → F) (p.1 - p.2) : F))
      fun (p : E × E) ↦ p.1 - p.2
x_1 : E × E
⊢ HSub.hSub (β := F) (HSub.hSub (α := F) (∑ i ∈ u, A i x_1.1) (∑ i ∈ u, A i x_1.2))
      ((∑ i ∈ u, A' i : (a : E) → F) (x_1.1 - x_1.2) : F) =
    ∑ i ∈ u, HSub.hSub (β := F) (A i x_1.1 - A i x_1.2) ((A' i : (a : E) → F) (x_1.1 - x_1.2) : F)

Tactic:
simp [Finset.sum_sub_distrib, ContinuousLinearMap.sum_apply]

Premises used: ContinuousLinearMap.sum_apply, Finset.sum_sub_distrib
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, HasStrictFDerivAt (A i) (A' i) x
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (y : E) ↦ ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x

Tactic:
HasStrictFDerivAt.fun_sum h

Premises used: HasStrictFDerivAt.fun_sum
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, HasStrictFDerivAt (A i) (A' i) x
h₁ : ∀ (x : E), Eq.{u_3 + 1} (α := F) ((∑ i ∈ u, A i) x) (∑ i ∈ u, A i x)
⊢ HasStrictFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (∑ i ∈ u, A i) (∑ i ∈ u, A' i) x

Tactic:
convert! HasStrictFDerivAt.fun_sum h

Premises used: HasStrictFDerivAt.fun_sum
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, HasStrictFDerivAt (A i) (A' i) x
x_1 : E
⊢ Eq.{u_3 + 1} (α := F) ((∑ i ∈ u, A i) x_1) (∑ i ∈ u, A i x_1)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
L : Filter (E × E)
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, HasFDerivAtFilter (A i) (A' i) L
simp :
  ∀
    (h :
      ∀ i ∈ u,
        IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) L
          (fun (p : E × E) ↦ HSub.hSub (β := F) (A i p.1 - A i p.2) ((A' i : (a : E) → F) (p.1 - p.2) : F))
          fun (p : E × E) ↦ p.1 - p.2),
    IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) L
      (fun (p : E × E) ↦
        HSub.hSub (β := F) (HSub.hSub (α := F) (∑ i ∈ u, A i p.1) (∑ i ∈ u, A i p.2))
          ((∑ i ∈ u, A' i : (a : E) → F) (p.1 - p.2) : F))
      fun (p : E × E) ↦ p.1 - p.2
⊢ HasFDerivAtFilter.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (y : E) ↦ ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) L

Tactic:
simp only [hasFDerivAtFilter_iff_isLittleO] at *

Premises used: hasFDerivAtFilter_iff_isLittleO
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
L : Filter (E × E)
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h :
  ∀ i ∈ u,
    IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) L
      (fun (p : E × E) ↦ HSub.hSub (β := F) (A i p.1 - A i p.2) ((A' i : (a : E) → F) (p.1 - p.2) : F))
      fun (p : E × E) ↦ p.1 - p.2
⊢ IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) L
    (fun (x : E × E) ↦ ∑ i ∈ u, HSub.hSub (β := F) (A i x.1 - A i x.2) ((A' i : (a : E) → F) (x.1 - x.2) : F))
    fun (p : E × E) ↦ p.1 - p.2

Tactic:
IsLittleO.sum h

Premises used: Asymptotics.IsLittleO.sum
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
L : Filter (E × E)
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h :
  ∀ i ∈ u,
    IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) L
      (fun (p : E × E) ↦ HSub.hSub (β := F) (A i p.1 - A i p.2) ((A' i : (a : E) → F) (p.1 - p.2) : F))
      fun (p : E × E) ↦ p.1 - p.2
h₁ :
  ∀ (x : E × E),
    HSub.hSub (β := F) (HSub.hSub (α := F) (∑ i ∈ u, A i x.1) (∑ i ∈ u, A i x.2))
        ((∑ i ∈ u, A' i : (a : E) → F) (x.1 - x.2) : F) =
      ∑ i ∈ u, HSub.hSub (β := F) (A i x.1 - A i x.2) ((A' i : (a : E) → F) (x.1 - x.2) : F)
⊢ IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) L
    (fun (p : E × E) ↦
      HSub.hSub (β := F) (HSub.hSub (α := F) (∑ i ∈ u, A i p.1) (∑ i ∈ u, A i p.2))
        ((∑ i ∈ u, A' i : (a : E) → F) (p.1 - p.2) : F))
    fun (p : E × E) ↦ p.1 - p.2

Tactic:
convert! IsLittleO.sum h

Premises used: Asymptotics.IsLittleO.sum
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
L : Filter (E × E)
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h :
  ∀ i ∈ u,
    IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) L
      (fun (p : E × E) ↦ HSub.hSub (β := F) (A i p.1 - A i p.2) ((A' i : (a : E) → F) (p.1 - p.2) : F))
      fun (p : E × E) ↦ p.1 - p.2
x : E × E
⊢ HSub.hSub (β := F) (HSub.hSub (α := F) (∑ i ∈ u, A i x.1) (∑ i ∈ u, A i x.2))
      ((∑ i ∈ u, A' i : (a : E) → F) (x.1 - x.2) : F) =
    ∑ i ∈ u, HSub.hSub (β := F) (A i x.1 - A i x.2) ((A' i : (a : E) → F) (x.1 - x.2) : F)

Tactic:
simp [ContinuousLinearMap.sum_apply]

Premises used: ContinuousLinearMap.sum_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
L : Filter (E × E)
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, HasFDerivAtFilter (A i) (A' i) L
⊢ HasFDerivAtFilter.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (y : E) ↦ ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) L

Tactic:
HasFDerivAtFilter.fun_sum h

Premises used: HasFDerivAtFilter.fun_sum
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
L : Filter (E × E)
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, HasFDerivAtFilter (A i) (A' i) L
h₁ : ∀ (x : E), Eq.{u_3 + 1} (α := F) ((∑ i ∈ u, A i) x) (∑ i ∈ u, A i x)
⊢ HasFDerivAtFilter.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (∑ i ∈ u, A i) (∑ i ∈ u, A' i) L

Tactic:
convert! HasFDerivAtFilter.fun_sum h

Premises used: HasFDerivAtFilter.fun_sum
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
L : Filter (E × E)
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, HasFDerivAtFilter (A i) (A' i) L
x : E
⊢ Eq.{u_3 + 1} (α := F) ((∑ i ∈ u, A i) x) (∑ i ∈ u, A i x)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
x : E
s : Set E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, HasFDerivWithinAt (A i) (A' i) s x
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (y : E) ↦ ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) s x

Tactic:
HasFDerivAtFilter.fun_sum h

Premises used: HasFDerivAtFilter.fun_sum, HasFDerivWithinAt