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
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) (∑ i ∈ u, A i) (∑ i ∈ u, A' i) s x

Tactic:
HasFDerivAtFilter.sum h

Premises used: HasFDerivWithinAt, HasFDerivAtFilter.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, HasFDerivAt (A i) (A' i) x
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (fun (y : E) ↦ ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x

Tactic:
HasFDerivAtFilter.fun_sum h

Premises used: HasFDerivAt, 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
x : E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, HasFDerivAt (A i) (A' i) x
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) (F := F) (∑ i ∈ u, A i) (∑ i ∈ u, A' i) x

Tactic:
HasFDerivAtFilter.sum h

Premises used: HasFDerivAt, HasFDerivAtFilter.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
s : Set E
ι : Type u_4
u : Finset ι
A : ι → E → F
h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ ∑ i ∈ u, A i y) s x

Tactic:
HasFDerivWithinAt.differentiableWithinAt <|
    HasFDerivWithinAt.fun_sum fun i hi => (h i hi).hasFDerivWithinAt

Premises used: HasFDerivWithinAt.differentiableWithinAt, HasFDerivWithinAt.fun_sum, 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
x : E
s : Set E
ι : Type u_4
u : Finset ι
A : ι → E → F
h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (∑ i ∈ u, A i) s x

Tactic:
HasFDerivWithinAt.differentiableWithinAt <|
    HasFDerivWithinAt.sum fun i hi => (h i hi).hasFDerivWithinAt

Premises used: HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.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
h : ∀ i ∈ u, DifferentiableAt 𝕜 (A i) x
⊢ DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ ∑ i ∈ u, A i y) x

Tactic:
HasFDerivAt.differentiableAt <| HasFDerivAt.fun_sum fun i hi => (h i hi).hasFDerivAt

Premises used: HasFDerivAt.fun_sum, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- 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
h : ∀ i ∈ u, DifferentiableAt 𝕜 (A i) x
⊢ DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) (∑ i ∈ u, A i) x

Tactic:
HasFDerivAt.differentiableAt <| HasFDerivAt.sum fun i hi => (h i hi).hasFDerivAt

Premises used: HasFDerivAt.sum, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- 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
s : Set E
ι : Type u_4
u : Finset ι
A : ι → E → F
h : ∀ i ∈ u, DifferentiableOn 𝕜 (A i) s
⊢ DifferentiableOn.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ ∑ i ∈ u, A i y) s

Tactic:
fun x hx =>
  DifferentiableWithinAt.fun_sum fun i hi => h i hi x hx

Premises used: DifferentiableWithinAt.fun_sum, 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
s : Set E
ι : Type u_4
u : Finset ι
A : ι → E → F
h : ∀ i ∈ u, DifferentiableOn 𝕜 (A i) s
⊢ DifferentiableOn.{u_1, u_2, u_3} 𝕜 (F := F) (∑ i ∈ u, A i) s

Tactic:
fun x hx =>
  DifferentiableWithinAt.sum fun i hi => h i hi x hx

Premises used: DifferentiableWithinAt.sum, 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
ι : Type u_4
u : Finset ι
A : ι → E → F
h : ∀ i ∈ u, Differentiable 𝕜 (A i)
⊢ Differentiable.{u_1, u_2, u_3} 𝕜 (F := F) fun (y : E) ↦ ∑ i ∈ u, A i y

Tactic:
fun x => DifferentiableAt.fun_sum fun i hi => h i hi x

Premises used: Differentiable, DifferentiableAt.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
ι : Type u_4
u : Finset ι
A : ι → E → F
h : ∀ i ∈ u, Differentiable 𝕜 (A i)
⊢ Differentiable.{u_1, u_2, u_3} 𝕜 (E := E) (F := F) (∑ i ∈ u, A i)

Tactic:
fun x => DifferentiableAt.sum fun i hi => h i hi x

Premises used: Differentiable, DifferentiableAt.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
s : Set E
ι : Type u_4
u : Finset ι
A : ι → E → F
hxs : UniqueDiffWithinAt 𝕜 s x
h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (y : E) ↦ ∑ i ∈ u, A i y) s x) (∑ i ∈ u, fderivWithin 𝕜 (A i) s x)

Tactic:
(HasFDerivWithinAt.fun_sum fun i hi => (h i hi).hasFDerivWithinAt).fderivWithin hxs

Premises used: HasFDerivWithinAt.fderivWithin, HasFDerivWithinAt.fun_sum, 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
x : E
s : Set E
ι : Type u_4
u : Finset ι
A : ι → E → F
hxs : UniqueDiffWithinAt 𝕜 s x
h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (∑ i ∈ u, A i) s x) (∑ i ∈ u, fderivWithin 𝕜 (A i) s x)

Tactic:
(HasFDerivWithinAt.sum fun i hi => (h i hi).hasFDerivWithinAt).fderivWithin hxs

Premises used: HasFDerivWithinAt.fderivWithin, DifferentiableWithinAt.hasFDerivWithinAt, HasFDerivWithinAt.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
h : ∀ i ∈ u, DifferentiableAt 𝕜 (A i) x
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (fun (y : E) ↦ ∑ i ∈ u, A i y) x) (∑ i ∈ u, fderiv 𝕜 (A i) x)

Tactic:
(HasFDerivAt.fun_sum fun i hi => (h i hi).hasFDerivAt).fderiv

Premises used: HasFDerivAt.fun_sum, 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
x : E
ι : Type u_4
u : Finset ι
A : ι → E → F
h : ∀ i ∈ u, DifferentiableAt 𝕜 (A i) x
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (∑ i ∈ u, A i) x) (∑ i ∈ u, fderiv 𝕜 (A i) x)

Tactic:
(HasFDerivAt.sum fun i hi => (h i hi).hasFDerivAt).fderiv

Premises used: HasFDerivAt.sum, 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 : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
h : HasFDerivAtFilter f f' L
⊢ HasFDerivAtFilter (-f) (-f') L

Tactic:
(-1 : F →L[𝕜] F).hasFDerivAtFilter.comp h tendsto_map

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.hasFDerivAtFilter, HasFDerivAtFilter.comp, Filter.tendsto_map, OfNat.ofNat, Neg.neg
-- 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
h : HasStrictFDerivAt f f' x
⊢ HasStrictFDerivAt (-f) (-f') x

Tactic:
HasFDerivAtFilter.neg h

Premises used: HasFDerivAtFilter.neg, HasStrictFDerivAt
-- 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
h : HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt (-f) (-f') s x

Tactic:
HasFDerivAtFilter.neg h

Premises used: HasFDerivAtFilter.neg, 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 : E → F
f' : E →L[𝕜] F
x : E
h : HasFDerivAt f f' x
⊢ HasFDerivAt (-f) (-f') x

Tactic:
HasFDerivAtFilter.neg h

Premises used: HasFDerivAt, HasFDerivAtFilter.neg
-- 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
h : DifferentiableWithinAt 𝕜 f s x
⊢ DifferentiableWithinAt 𝕜 (-f) s x

Tactic:
h.hasFDerivWithinAt.neg.differentiableWithinAt

Premises used: HasFDerivWithinAt.neg, HasFDerivWithinAt.differentiableWithinAt, 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 : E → F
x : E
s : Set E
h : DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ -f y) s x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
simpa only [neg_neg] using h.fun_neg

Premises used: neg_neg, DifferentiableWithinAt.fun_neg
-- 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
h : DifferentiableWithinAt 𝕜 (-f) s x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
simpa only [neg_neg] using h.neg

Premises used: neg_neg, DifferentiableWithinAt.neg
-- 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
h : DifferentiableAt 𝕜 f x
⊢ DifferentiableAt 𝕜 (-f) x

Tactic:
h.hasFDerivAt.neg.differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt, HasFDerivAt.neg
-- 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
h : DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ -f y) x
⊢ DifferentiableAt 𝕜 f x

Tactic:
simpa only [neg_neg] using h.fun_neg

Premises used: DifferentiableAt.fun_neg, neg_neg
-- 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
h : DifferentiableAt 𝕜 (-f) x
⊢ DifferentiableAt 𝕜 f x

Tactic:
simpa only [neg_neg] using h.neg

Premises used: DifferentiableAt.neg, neg_neg
-- 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
h : DifferentiableOn 𝕜 f s
⊢ DifferentiableOn 𝕜 (-f) s

Tactic:
fun x hx => (h x hx).neg

Premises used: DifferentiableWithinAt.neg, 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 : E → F
s : Set E
h : DifferentiableOn.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ -f y) s
⊢ DifferentiableOn 𝕜 f s

Tactic:
simpa only [neg_neg] using h.fun_neg

Premises used: neg_neg, DifferentiableOn.fun_neg
-- 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
h : DifferentiableOn 𝕜 (-f) s
⊢ DifferentiableOn 𝕜 f s

Tactic:
simpa only [neg_neg] using h.neg

Premises used: neg_neg, DifferentiableOn.neg
-- 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
h : Differentiable 𝕜 f
⊢ Differentiable 𝕜 (-f)

Tactic:
fun x =>
  (h x).neg

Premises used: Differentiable, DifferentiableAt.neg
-- 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
h : Differentiable.{u_1, u_2, u_3} 𝕜 (F := F) fun (y : E) ↦ -f y
⊢ Differentiable 𝕜 f

Tactic:
simpa only [neg_neg] using h.fun_neg

Premises used: Differentiable.fun_neg, neg_neg
-- 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
h : Differentiable 𝕜 (-f)
⊢ Differentiable 𝕜 f

Tactic:
simpa only [neg_neg] using h.neg

Premises used: neg_neg, Differentiable.neg
-- 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
hxs : UniqueDiffWithinAt 𝕜 s x
pos :
  ∀ (h : DifferentiableWithinAt 𝕜 f s x),
    Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (y : E) ↦ -f y) s x) (-fderivWithin 𝕜 f s x)
neg :
  ∀ (h : ¬DifferentiableWithinAt 𝕜 f s x),
    Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (y : E) ↦ -f y) s x) (-fderivWithin 𝕜 f s x)
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (y : E) ↦ -f y) s x) (-fderivWithin 𝕜 f s x)

Tactic:
by_cases h : DifferentiableWithinAt 𝕜 f s x

Premises used: 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
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f s x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (y : E) ↦ -f y) s x) (-fderivWithin 𝕜 f s x)

Tactic:
h.hasFDerivWithinAt.neg.fderivWithin hxs

Premises used: HasFDerivWithinAt.neg, 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 : E → F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
h : DifferentiableWithinAt 𝕜 f s x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (y : E) ↦ -f y) s x) (-fderivWithin 𝕜 f s x)

Tactic:
exact h.hasFDerivWithinAt.neg.fderivWithin hxs

Premises used: HasFDerivWithinAt.neg, 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 : E → F
x : E
s : Set E
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
neg : ¬DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ -f y) s x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (y : E) ↦ -f y) s x) (-fderivWithin 𝕜 f s x)

Tactic:
rw [fderivWithin_zero_of_not_differentiableWithinAt h,
      fderivWithin_zero_of_not_differentiableWithinAt, neg_zero]

Premises used: fderivWithin_zero_of_not_differentiableWithinAt, neg_zero
-- 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
hxs : UniqueDiffWithinAt 𝕜 s x
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ ¬DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ -f y) s x

Tactic:
simpa
-- 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
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (-f) s x) (-fderivWithin 𝕜 f s x)

Tactic:
fderivWithin_fun_neg hxs

Premises used: fderivWithin_fun_neg
-- 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
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (fun (y : E) ↦ -f y) x) (-fderiv 𝕜 f x)

Tactic:
simp only [← fderivWithin_univ, fderivWithin_fun_neg uniqueDiffWithinAt_univ]

Premises used: fderivWithin_fun_neg, fderivWithin_univ, uniqueDiffWithinAt_univ
-- 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
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (-f) x) (-fderiv 𝕜 f x)

Tactic:
fderiv_fun_neg

Premises used: fderiv_fun_neg
-- 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
f' g' : E →L[𝕜] F
L : Filter (E × E)
hf : HasFDerivAtFilter f f' L
hg : HasFDerivAtFilter g g' L
⊢ HasFDerivAtFilter (f - g) (f' - g') L

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Premises used: HasFDerivAtFilter.neg, sub_eq_add_neg, HasFDerivAtFilter.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
f' g' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
hg : HasStrictFDerivAt g g' x
⊢ HasStrictFDerivAt (f - g) (f' - g') x

Tactic:
HasFDerivAtFilter.sub hf hg

Premises used: HasFDerivAtFilter.sub, HasStrictFDerivAt
-- 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
f' g' : E →L[𝕜] F
x : E
s : Set E
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt g g' s x
⊢ HasFDerivWithinAt (f - g) (f' - g') s x

Tactic:
HasFDerivAtFilter.sub hf hg

Premises used: HasFDerivAtFilter.sub, 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
f' g' : E →L[𝕜] F
x : E
hf : HasFDerivAt f f' x
hg : HasFDerivAt g g' x
⊢ HasFDerivAt (f - g) (f' - g') x

Tactic:
HasFDerivAtFilter.sub hf hg

Premises used: HasFDerivAt, HasFDerivAtFilter.sub
-- 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
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
⊢ DifferentiableWithinAt 𝕜 (f - g) s x

Tactic:
(hf.hasFDerivWithinAt.sub hg.hasFDerivWithinAt).differentiableWithinAt

Premises used: HasFDerivWithinAt.sub, HasFDerivWithinAt.differentiableWithinAt, 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
hf : DifferentiableAt 𝕜 f x
hg : DifferentiableAt 𝕜 g x
⊢ DifferentiableAt 𝕜 (f - g) x

Tactic:
(hf.hasFDerivAt.sub hg.hasFDerivAt).differentiableAt

Premises used: HasFDerivAt.sub, DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt
-- 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
hg : DifferentiableAt 𝕜 g x
⊢ DifferentiableAt 𝕜 (f + g) x ↔ DifferentiableAt 𝕜 f x

Tactic:
⟨fun h ↦ ?_, fun hf ↦ hf.add hg⟩

Premises used: Iff.intro, 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
hg : DifferentiableAt 𝕜 g x
refine : ∀ (h : DifferentiableAt 𝕜 (f + g) x), DifferentiableAt 𝕜 f x
⊢ DifferentiableAt 𝕜 (f + g) x ↔ DifferentiableAt 𝕜 f x

Tactic:
refine ⟨fun h ↦ ?_, fun hf ↦ hf.add hg⟩
-- 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
hg : DifferentiableAt 𝕜 g x
h : DifferentiableAt 𝕜 (f + g) x
⊢ DifferentiableAt 𝕜 f x

Tactic:
simpa only [add_sub_cancel_right] using h.sub hg

Premises used: DifferentiableAt.sub, add_sub_cancel_right