awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
c : F
⊢ HasDerivAt (fun (x : 𝕜) ↦ c + f x) f' x ↔ HasDerivAt f f' x

Tactic:
hasDerivAtFilter_const_add_iff c

Premises used: HasDerivAt, hasDerivAtFilter_const_add_iff
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
c : F
⊢ derivWithin (fun (x : 𝕜) ↦ c + f x) s x = derivWithin f s x

Tactic:
simp only [derivWithin, fderivWithin_const_add]

Premises used: fderivWithin_const_add, derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
c : F
h : ∀ (x : Set 𝕜) (x_1 : 𝕜), derivWithin (fun (x : 𝕜) ↦ c + f x) x x_1 = derivWithin f x x_1
⊢ (derivWithin fun (x : 𝕜) ↦ c + f x) = derivWithin f

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
c : F
x : Set 𝕜
x_1 : 𝕜
⊢ derivWithin (fun (x : 𝕜) ↦ c + f x) x x_1 = derivWithin f x x_1

Tactic:
apply derivWithin_const_add

Premises used: derivWithin_const_add
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
c : F
⊢ deriv (fun (x : 𝕜) ↦ c + f x) x = deriv f x

Tactic:
simp only [deriv, fderiv_const_add]

Premises used: deriv, fderiv_const_add
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
c : F
⊢ (deriv fun (x : 𝕜) ↦ c + f x) = deriv f

Tactic:
funext fun _ ↦ deriv_const_add c

Premises used: funext, deriv_const_add
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x c : 𝕜
rw : Eq (α := 𝕜) (deriv (fun (x : 𝕜) ↦ x) x) 1
rw₁ rw₂ : Eq.{u + 1} (α := 𝕜) ((fun (x : 𝕜) ↦ (1 : 𝕜)) x) 1
⊢ Eq (α := 𝕜) (deriv (fun (x : 𝕜) ↦ c + x) x) 1

Tactic:
rw [deriv_const_add c, deriv_id'']

Premises used: deriv_id'', deriv_const_add
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
c : 𝕜
⊢ Eq.{u + 1} (α := (x : 𝕜) → 𝕜) (deriv fun (x : 𝕜) ↦ c + x) fun (x : 𝕜) ↦ 1

Tactic:
funext fun _ ↦ deriv_const_add_id c

Premises used: deriv_const_add_id, funext
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
⊢ DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (x + b)) a ↔ DifferentiableAt 𝕜 f (a + b)

Tactic:
grind [add_comm, differentiableAt_comp_add_left]

Premises used: add_comm, differentiableAt_comp_add_left
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
⊢ DifferentiableAt 𝕜 f a ↔ DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (b + x)) (-b + a)

Tactic:
simp [differentiableAt_comp_add_left]

Premises used: differentiableAt_comp_add_left
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a b : 𝕜
⊢ DifferentiableAt 𝕜 f a ↔ DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (x + b)) (a - b)

Tactic:
simp [differentiableAt_comp_add_const]

Premises used: differentiableAt_comp_add_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
L : Filter (𝕜 × 𝕜)
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
A' : ι → F
h : ∀ i ∈ u, HasDerivAtFilter (A i) (A' i) L
⊢ HasDerivAtFilter.{u, v} (F := F) (fun (y : 𝕜) ↦ ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) L

Tactic:
simpa using (HasFDerivAtFilter.fun_sum h).hasDerivAtFilter

Premises used: HasFDerivAtFilter.fun_sum, HasFDerivAtFilter.hasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
L : Filter (𝕜 × 𝕜)
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
A' : ι → F
h : ∀ i ∈ u, HasDerivAtFilter (A i) (A' i) L
⊢ HasDerivAtFilter.{u, v} (F := F) (fun (y : 𝕜) ↦ ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) L

Tactic:
HasDerivAtFilter.fun_sum h

Premises used: HasDerivAtFilter.fun_sum
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
L : Filter (𝕜 × 𝕜)
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
A' : ι → F
h : ∀ i ∈ u, HasDerivAtFilter (A i) (A' i) L
h₁ : ∀ (x : 𝕜), Eq.{v + 1} (α := F) ((∑ i ∈ u, A i) x) (∑ i ∈ u, A i x)
⊢ HasDerivAtFilter.{u, v} (F := F) (∑ i ∈ u, A i) (∑ i ∈ u, A' i) L

Tactic:
convert! HasDerivAtFilter.fun_sum h

Premises used: HasDerivAtFilter.fun_sum
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
L : Filter (𝕜 × 𝕜)
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
A' : ι → F
h : ∀ i ∈ u, HasDerivAtFilter (A i) (A' i) L
x : 𝕜
⊢ Eq.{v + 1} (α := F) ((∑ i ∈ u, A i) x) (∑ i ∈ u, A i x)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
A' : ι → F
h : ∀ i ∈ u, HasStrictDerivAt (A i) (A' i) x
⊢ HasStrictDerivAt.{u, v} (F := F) (fun (y : 𝕜) ↦ ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x

Tactic:
HasDerivAtFilter.fun_sum h

Premises used: HasStrictDerivAt, HasDerivAtFilter.fun_sum
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
A' : ι → F
h : ∀ i ∈ u, HasStrictDerivAt (A i) (A' i) x
⊢ HasStrictDerivAt.{u, v} (F := F) (∑ i ∈ u, A i) (∑ i ∈ u, A' i) x

Tactic:
HasDerivAtFilter.sum h

Premises used: HasDerivAtFilter.sum, HasStrictDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
A' : ι → F
h : ∀ i ∈ u, HasDerivWithinAt (A i) (A' i) s x
⊢ HasDerivWithinAt.{u, v} (F := F) (fun (y : 𝕜) ↦ ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) s x

Tactic:
HasDerivAtFilter.fun_sum h

Premises used: HasDerivWithinAt, HasDerivAtFilter.fun_sum
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
A' : ι → F
h : ∀ i ∈ u, HasDerivWithinAt (A i) (A' i) s x
⊢ HasDerivWithinAt.{u, v} (F := F) (∑ i ∈ u, A i) (∑ i ∈ u, A' i) s x

Tactic:
HasDerivAtFilter.sum h

Premises used: HasDerivAtFilter.sum, HasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
A' : ι → F
h : ∀ i ∈ u, HasDerivAt (A i) (A' i) x
⊢ HasDerivAt.{u, v} (F := F) (fun (y : 𝕜) ↦ ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x

Tactic:
HasDerivAtFilter.fun_sum h

Premises used: HasDerivAt, HasDerivAtFilter.fun_sum
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
A' : ι → F
h : ∀ i ∈ u, HasDerivAt (A i) (A' i) x
⊢ HasDerivAt.{u, v} (F := F) (∑ i ∈ u, A i) (∑ i ∈ u, A' i) x

Tactic:
HasDerivAtFilter.sum h

Premises used: HasDerivAtFilter.sum, HasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    Eq.{v + 1} (α := F) (derivWithin (fun (y : 𝕜) ↦ ∑ i ∈ u, A i y) s x) (∑ i ∈ u, derivWithin (A i) s x)
neg :
  ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
    Eq.{v + 1} (α := F) (derivWithin (fun (y : 𝕜) ↦ ∑ i ∈ u, A i y) s x) (∑ i ∈ u, derivWithin (A i) s x)
⊢ Eq.{v + 1} (α := F) (derivWithin (fun (y : 𝕜) ↦ ∑ i ∈ u, A i y) s x) (∑ i ∈ u, derivWithin (A i) s x)

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Premises used: UniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ Eq.{v + 1} (α := F) (derivWithin (fun (y : 𝕜) ↦ ∑ i ∈ u, A i y) s x) (∑ i ∈ u, derivWithin (A i) s x)

Tactic:
(HasDerivWithinAt.fun_sum fun i hi ↦ (h i hi).hasDerivWithinAt).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.fun_sum
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ Eq.{v + 1} (α := F) (derivWithin (fun (y : 𝕜) ↦ ∑ i ∈ u, A i y) s x) (∑ i ∈ u, derivWithin (A i) s x)

Tactic:
exact (HasDerivWithinAt.fun_sum fun i hi ↦ (h i hi).hasDerivWithinAt).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.fun_sum
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ Eq.{v + 1} (α := F) (derivWithin (fun (y : 𝕜) ↦ ∑ i ∈ u, A i y) s x) (∑ i ∈ u, derivWithin (A i) s x)

Tactic:
simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

Premises used: derivWithin_zero_of_not_uniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x),
    Eq.{v + 1} (α := F) (derivWithin (∑ i ∈ u, A i) s x) (∑ i ∈ u, derivWithin (A i) s x)
neg :
  ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x),
    Eq.{v + 1} (α := F) (derivWithin (∑ i ∈ u, A i) s x) (∑ i ∈ u, derivWithin (A i) s x)
⊢ Eq.{v + 1} (α := F) (derivWithin (∑ i ∈ u, A i) s x) (∑ i ∈ u, derivWithin (A i) s x)

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Premises used: UniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ Eq.{v + 1} (α := F) (derivWithin (∑ i ∈ u, A i) s x) (∑ i ∈ u, derivWithin (A i) s x)

Tactic:
(HasDerivWithinAt.sum fun i hi ↦ (h i hi).hasDerivWithinAt).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.sum
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ Eq.{v + 1} (α := F) (derivWithin (∑ i ∈ u, A i) s x) (∑ i ∈ u, derivWithin (A i) s x)

Tactic:
exact (HasDerivWithinAt.sum fun i hi ↦ (h i hi).hasDerivWithinAt).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.sum
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ Eq.{v + 1} (α := F) (derivWithin (∑ i ∈ u, A i) s x) (∑ i ∈ u, derivWithin (A i) s x)

Tactic:
simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

Premises used: derivWithin_zero_of_not_uniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
h : ∀ i ∈ u, DifferentiableAt 𝕜 (A i) x
⊢ Eq.{v + 1} (α := F) (deriv (fun (y : 𝕜) ↦ ∑ i ∈ u, A i y) x) (∑ i ∈ u, deriv (A i) x)

Tactic:
(HasDerivAt.fun_sum fun i hi ↦ (h i hi).hasDerivAt).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.fun_sum
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
ι : Type u_1
u : Finset ι
A : ι → 𝕜 → F
h : ∀ i ∈ u, DifferentiableAt 𝕜 (A i) x
⊢ Eq.{v + 1} (α := F) (deriv (∑ i ∈ u, A i) x) (∑ i ∈ u, deriv (A i) x)

Tactic:
(HasDerivAt.sum fun i hi ↦ (h i hi).hasDerivAt).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.sum
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
L : Filter (𝕜 × 𝕜)
h : HasDerivAtFilter f f' L
⊢ HasDerivAtFilter (-f) (-f') L

Tactic:
simpa using (HasFDerivAtFilter.neg h).hasDerivAtFilter

Premises used: HasFDerivAtFilter.neg, HasFDerivAtFilter.hasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
h : HasDerivWithinAt f f' s x
⊢ HasDerivWithinAt (-f) (-f') s x

Tactic:
HasDerivAtFilter.neg h

Premises used: HasDerivWithinAt, HasDerivAtFilter.neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
h : HasDerivAt f f' x
⊢ HasDerivAt (-f) (-f') x

Tactic:
HasDerivAtFilter.neg h

Premises used: HasDerivAt, HasDerivAtFilter.neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
h : HasStrictDerivAt f f' x
⊢ HasStrictDerivAt (-f) (-f') x

Tactic:
HasDerivAtFilter.neg h

Premises used: HasStrictDerivAt, HasDerivAtFilter.neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
pos : ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (-f) s x = -derivWithin f s x
neg₁ : ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (-f) s x = -derivWithin f s x
⊢ derivWithin (-f) s x = -derivWithin f s x

Tactic:
by_cases hsx : UniqueDiffWithinAt 𝕜 s x

Premises used: UniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (-f) s x = -derivWithin f s x

Tactic:
simp only [derivWithin, fderivWithin_neg hsx, ContinuousLinearMap.neg_apply]

Premises used: derivWithin, fderivWithin_neg, ContinuousLinearMap.neg_apply
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (-f) s x = -derivWithin f s x

Tactic:
simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]

Premises used: derivWithin_zero_of_not_uniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
⊢ deriv (-f) x = -deriv f x

Tactic:
simp only [deriv, fderiv_neg, ContinuousLinearMap.neg_apply]

Premises used: fderiv_neg, deriv, ContinuousLinearMap.neg_apply
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
⊢ deriv (-f) = fun (x : 𝕜) ↦ -deriv f x

Tactic:
funext fun _ ↦ deriv.neg

Premises used: deriv.neg, funext
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
L : Filter (𝕜 × 𝕜)
⊢ HasDerivAtFilter Neg.neg (-1) L

Tactic:
HasDerivAtFilter.neg <| hasDerivAtFilter_id _

Premises used: hasDerivAtFilter_id, HasDerivAtFilter.neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
⊢ HasDerivWithinAt Neg.neg (-1) s x

Tactic:
hasDerivAtFilter_neg _

Premises used: HasDerivWithinAt, hasDerivAtFilter_neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
⊢ HasDerivAt Neg.neg (-1) x

Tactic:
hasDerivAtFilter_neg _

Premises used: HasDerivAt, hasDerivAtFilter_neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
⊢ HasDerivAt (F := 𝕜) (fun (x : 𝕜) ↦ -x) (-1) x

Tactic:
hasDerivAtFilter_neg _

Premises used: HasDerivAt, hasDerivAtFilter_neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
⊢ HasStrictDerivAt Neg.neg (-1) x

Tactic:
HasStrictDerivAt.neg <| hasStrictDerivAt_id _

Premises used: hasStrictDerivAt_id, HasStrictDerivAt.neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
⊢ deriv Neg.neg x = -1

Tactic:
HasDerivAt.deriv (hasDerivAt_neg x)

Premises used: HasDerivAt.deriv, hasDerivAt_neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
⊢ Eq.{u + 1} (α := (x : 𝕜) → 𝕜) (deriv Neg.neg) fun (x : 𝕜) ↦ -1

Tactic:
funext deriv_neg

Premises used: funext, deriv_neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
⊢ Eq (α := 𝕜) (deriv (fun (x : 𝕜) ↦ -x) x) (-1)

Tactic:
deriv_neg x

Premises used: deriv_neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin Neg.neg s x = -1

Tactic:
(hasDerivWithinAt_neg x s).derivWithin hxs

Premises used: hasDerivWithinAt_neg, HasDerivWithinAt.derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
⊢ Differentiable 𝕜 (E := 𝕜) Neg.neg

Tactic:
Differentiable.neg differentiable_id

Premises used: Differentiable.neg, differentiable_id
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
s : Set 𝕜
⊢ DifferentiableOn 𝕜 Neg.neg s

Tactic:
DifferentiableOn.neg differentiableOn_id

Premises used: DifferentiableOn.neg, differentiableOn_id
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
⊢ DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (-x)) a ↔ DifferentiableAt 𝕜 f (-a)

Tactic:
⟨fun H ↦ ?_, fun H ↦ H.comp a differentiable_neg.differentiableAt⟩

Premises used: Differentiable.differentiableAt, Iff.intro, differentiable_neg, DifferentiableAt.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
refine : ∀ (H : DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (-x)) a), DifferentiableAt 𝕜 f (-a)
⊢ DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (-x)) a ↔ DifferentiableAt 𝕜 f (-a)

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ H.comp a differentiable_neg.differentiableAt⟩
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
H : DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (-x)) a
h : f = (fun (x : 𝕜) ↦ f (-x)) ∘ Neg.neg
⊢ DifferentiableAt 𝕜 f (-a)

Tactic:
convert! ((neg_neg a).symm ▸ H).comp (-a) differentiable_neg.differentiableAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
H : DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (-x)) a
h : ∀ (x : 𝕜), f x = ((fun (x : 𝕜) ↦ f (-x)) ∘ Neg.neg) x
⊢ f = (fun (x : 𝕜) ↦ f (-x)) ∘ Neg.neg

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
H : DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (-x)) a
x : 𝕜
⊢ f x = ((fun (x : 𝕜) ↦ f (-x)) ∘ Neg.neg) x

Tactic:
simp only [Function.comp_apply, neg_neg]

Premises used: neg_neg, Function.comp_apply
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
a : 𝕜
simp_rw : DifferentiableAt 𝕜 f a ↔ DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (- -x)) a
⊢ DifferentiableAt 𝕜 f a ↔ DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (-x)) (-a)

Tactic:
simp_rw [← differentiableAt_comp_neg, neg_neg]

Premises used: differentiableAt_comp_neg, neg_neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f g : 𝕜 → F
f' g' : F
L : Filter (𝕜 × 𝕜)
hf : HasDerivAtFilter f f' L
hg : HasDerivAtFilter g g' L
⊢ HasDerivAtFilter (f - g) (f' - g') L

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

Premises used: HasDerivAtFilter.add, sub_eq_add_neg, HasDerivAtFilter.neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f g : 𝕜 → F
f' g' : F
x : 𝕜
s : Set 𝕜
hf : HasDerivWithinAt f f' s x
hg : HasDerivWithinAt g g' s x
⊢ HasDerivWithinAt (f - g) (f' - g') s x

Tactic:
HasDerivAtFilter.sub hf hg

Premises used: HasDerivAtFilter.sub, HasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f g : 𝕜 → F
f' g' : F
x : 𝕜
hf : HasDerivAt f f' x
hg : HasDerivAt g g' x
⊢ HasDerivAt (f - g) (f' - g') x

Tactic:
HasDerivAtFilter.sub hf hg

Premises used: HasDerivAt, HasDerivAtFilter.sub
-- Module: Mathlib.Analysis.Calculus.Deriv.Add
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f g : 𝕜 → F
f' g' : F
x : 𝕜
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
⊢ HasStrictDerivAt (f - g) (f' - g') x

Tactic:
HasDerivAtFilter.sub hf hg

Premises used: HasDerivAtFilter.sub, HasStrictDerivAt