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
x : E
hg : DifferentiableAt 𝕜 f x
⊢ DifferentiableAt 𝕜 (f + g) x ↔ DifferentiableAt 𝕜 g x

Tactic:
simp only [add_comm f, hg.add_iff_left]

Premises used: DifferentiableAt.add_iff_left, 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 g : E → F
x : E
hg : DifferentiableAt 𝕜 g x
⊢ DifferentiableAt 𝕜 (f - g) x ↔ DifferentiableAt 𝕜 f x

Tactic:
simp only [sub_eq_add_neg, differentiableAt_neg_iff, hg, add_iff_left]

Premises used: DifferentiableAt.add_iff_left, sub_eq_add_neg, differentiableAt_neg_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 g : E → F
x : E
hg : DifferentiableAt 𝕜 f x
⊢ DifferentiableAt 𝕜 (f - g) x ↔ DifferentiableAt 𝕜 g x

Tactic:
simp only [sub_eq_add_neg, hg, add_iff_right, differentiableAt_neg_iff]

Premises used: sub_eq_add_neg, differentiableAt_neg_iff, DifferentiableAt.add_iff_right
-- 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).sub (hg x hx)

Premises used: DifferentiableWithinAt.sub, 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
s : Set E
hg : DifferentiableOn 𝕜 g s
⊢ DifferentiableOn 𝕜 (f + g) s ↔ DifferentiableOn 𝕜 f s

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

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

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
s : Set E
hg : DifferentiableOn 𝕜 g s
h : DifferentiableOn 𝕜 (f + g) s
⊢ DifferentiableOn 𝕜 f s

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

Premises used: DifferentiableOn.sub, add_sub_cancel_right
-- 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
hg : DifferentiableOn 𝕜 f s
⊢ DifferentiableOn 𝕜 (f + g) s ↔ DifferentiableOn 𝕜 g s

Tactic:
simp only [add_comm f, hg.add_iff_left]

Premises used: add_comm, DifferentiableOn.add_iff_left
-- 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
hg : DifferentiableOn 𝕜 g s
⊢ DifferentiableOn 𝕜 (f - g) s ↔ DifferentiableOn 𝕜 f s

Tactic:
simp only [sub_eq_add_neg, differentiableOn_neg_iff, hg, add_iff_left]

Premises used: sub_eq_add_neg, DifferentiableOn.add_iff_left, differentiableOn_neg_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 g : E → F
s : Set E
hg : DifferentiableOn 𝕜 f s
⊢ DifferentiableOn 𝕜 (f - g) s ↔ DifferentiableOn 𝕜 g s

Tactic:
simp only [sub_eq_add_neg, differentiableOn_neg_iff, hg, add_iff_right]

Premises used: sub_eq_add_neg, DifferentiableOn.add_iff_right, differentiableOn_neg_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 g : E → F
hf : Differentiable 𝕜 f
hg : Differentiable 𝕜 g
⊢ Differentiable 𝕜 (f - g)

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

Premises used: Differentiable, DifferentiableAt.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
hg : Differentiable 𝕜 g
⊢ Differentiable 𝕜 (f + g) ↔ Differentiable 𝕜 f

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

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

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
hg : Differentiable 𝕜 g
h : Differentiable 𝕜 (f + g)
⊢ Differentiable 𝕜 f

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

Premises used: Differentiable.sub, add_sub_cancel_right
-- 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
hg : Differentiable 𝕜 f
⊢ Differentiable 𝕜 (f + g) ↔ Differentiable 𝕜 g

Tactic:
simp only [add_comm f, hg.add_iff_left]

Premises used: Differentiable.add_iff_left, 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 g : E → F
hg : Differentiable 𝕜 g
⊢ Differentiable 𝕜 (f - g) ↔ Differentiable 𝕜 f

Tactic:
simp only [sub_eq_add_neg, differentiable_neg_iff, hg, add_iff_left]

Premises used: sub_eq_add_neg, Differentiable.add_iff_left, differentiable_neg_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 g : E → F
hg : Differentiable 𝕜 f
⊢ Differentiable 𝕜 (f - g) ↔ Differentiable 𝕜 g

Tactic:
simp only [sub_eq_add_neg, differentiable_neg_iff, hg, add_iff_right]

Premises used: Differentiable.add_iff_right, sub_eq_add_neg, differentiable_neg_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 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 =
    HSub.hSub (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 g s x)

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

Premises used: HasFDerivWithinAt.fderivWithin, HasFDerivWithinAt.sub, 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 𝕜 (f - g) s x = HSub.hSub (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 g s x)

Tactic:
fderivWithin_fun_sub hxs hf hg

Premises used: fderivWithin_fun_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
hf : DifferentiableAt 𝕜 f x
hg : DifferentiableAt 𝕜 g x
⊢ fderiv 𝕜 (fun (y : E) ↦ f y - g y) x = HSub.hSub (α := E →L[𝕜] F) (fderiv 𝕜 f x) (fderiv 𝕜 g x)

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

Premises used: HasFDerivAt.sub, 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 𝕜 (f - g) x = HSub.hSub (α := E →L[𝕜] F) (fderiv 𝕜 f x) (fderiv 𝕜 g x)

Tactic:
fderiv_fun_sub hf hg

Premises used: fderiv_fun_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 : 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 only [sub_eq_add_neg, hasFDerivAtFilter_add_const_iff]

Premises used: sub_eq_add_neg, 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) ↦ f x - c) f' x ↔ HasStrictFDerivAt f f' x

Tactic:
hasFDerivAtFilter_sub_const_iff c

Premises used: hasFDerivAtFilter_sub_const_iff, 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
c : F
⊢ HasFDerivWithinAt (fun (x : E) ↦ f x - c) f' s x ↔ HasFDerivWithinAt f f' s x

Tactic:
hasFDerivAtFilter_sub_const_iff c

Premises used: hasFDerivAtFilter_sub_const_iff, 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
c : F
⊢ HasFDerivAt (fun (x : E) ↦ f x - c) f' x ↔ HasFDerivAt f f' x

Tactic:
hasFDerivAtFilter_sub_const_iff c

Premises used: HasFDerivAt, hasFDerivAtFilter_sub_const_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x c : F
⊢ HasStrictFDerivAt (fun (x : F) ↦ x - c) (ContinuousLinearMap.id 𝕜 F) x

Tactic:
(hasStrictFDerivAt_id x).sub_const c

Premises used: HasStrictFDerivAt.sub_const, hasStrictFDerivAt_id
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x c : F
⊢ HasFDerivAt (fun (x : F) ↦ x - c) (ContinuousLinearMap.id 𝕜 F) x

Tactic:
(hasFDerivAt_id x).sub_const c

Premises used: hasFDerivAt_id, HasFDerivAt.sub_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
x : E
s : Set E
hf : DifferentiableWithinAt 𝕜 f s x
c : F
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ f y - c) s x

Tactic:
(hf.hasFDerivWithinAt.sub_const c).differentiableWithinAt

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

Tactic:
simp only [sub_eq_add_neg, differentiableWithinAt_add_const_iff]

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

Tactic:
(hf.hasFDerivAt.sub_const c).differentiableAt

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

Tactic:
fun x hx => (hf x hx).sub_const c

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

Tactic:
fun x => (hf x).sub_const c

Premises used: Differentiable, DifferentiableAt.sub_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
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 only [sub_eq_add_neg, fderivWithin_add_const]

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

Tactic:
simp only [sub_eq_add_neg, fderiv_add_const]

Premises used: fderiv_add_const, sub_eq_add_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
L : Filter (E × E)
hf : HasFDerivAtFilter f f' L
c : F
⊢ HasFDerivAtFilter (fun (x : E) ↦ c - f x) (-f') L

Tactic:
simpa only [sub_eq_add_neg] using hf.neg.const_add c

Premises used: HasFDerivAtFilter.const_add, HasFDerivAtFilter.neg, sub_eq_add_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
hf : HasStrictFDerivAt f f' x
c : F
⊢ HasStrictFDerivAt (fun (x : E) ↦ c - f x) (-f') x

Tactic:
HasFDerivAtFilter.const_sub hf c

Premises used: HasFDerivAtFilter.const_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 : E → F
f' : E →L[𝕜] F
x : E
s : Set E
hf : HasFDerivWithinAt f f' s x
c : F
⊢ HasFDerivWithinAt (fun (x : E) ↦ c - f x) (-f') s x

Tactic:
HasFDerivAtFilter.const_sub hf c

Premises used: HasFDerivAtFilter.const_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 : E → F
f' : E →L[𝕜] F
x : E
hf : HasFDerivAt f f' x
c : F
⊢ HasFDerivAt (fun (x : E) ↦ c - f x) (-f') x

Tactic:
HasFDerivAtFilter.const_sub hf c

Premises used: HasFDerivAt, HasFDerivAtFilter.const_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 : E → F
x : E
s : Set E
hf : DifferentiableWithinAt 𝕜 f s x
c : F
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ c - f y) s x

Tactic:
(hf.hasFDerivWithinAt.const_sub c).differentiableWithinAt

Premises used: HasFDerivWithinAt.const_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 : 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:
simp [sub_eq_add_neg]

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

Tactic:
(hf.hasFDerivAt.const_sub c).differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt, HasFDerivAt.const_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 : E → F
s : Set E
hf : DifferentiableOn 𝕜 f s
c : F
⊢ DifferentiableOn.{u_1, u_2, u_3} 𝕜 (F := F) (fun (y : E) ↦ c - f y) s

Tactic:
fun x hx => (hf x hx).const_sub c

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

Tactic:
fun x => (hf x).const_sub c

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

Tactic:
simp only [sub_eq_add_neg, fderivWithin_const_add, fderivWithin_fun_neg, hxs]

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

Tactic:
simp only [← fderivWithin_univ, fderivWithin_const_sub uniqueDiffWithinAt_univ]

Premises used: fderivWithin_const_sub, 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
f' : E →L[𝕜] F
x : E
s : Set E
a : E
simp : map (fun (x : E) ↦ a + x) (𝓝 x) ⊓ map (fun (x : E) ↦ a + x) (𝓟 s) = 𝓝 (a + x) ⊓ 𝓟 (a +ᵥ s)
⊢ map (fun (x : E) ↦ a + x) (𝓝[s] x) = 𝓝[a +ᵥ s] (a + x)

Tactic:
simp only [nhdsWithin, Filter.map_inf (add_right_injective a)]

Premises used: Filter.map_inf, add_right_injective, nhdsWithin
-- 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
a : E
⊢ map (fun (x : E) ↦ a + x) (𝓝 x) ⊓ map (fun (x : E) ↦ a + x) (𝓟 s) = 𝓝 (a + x) ⊓ 𝓟 (a +ᵥ s)

Tactic:
simp [← Set.image_vadd]

Premises used: Set.image_vadd
-- 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
a : E
⊢ map (fun (x : E) ↦ a + x) (𝓝[s] x) = 𝓝[a +ᵥ s] (a + x)

Tactic:
have : map (a + ·) (𝓝[s] x) = 𝓝[a +ᵥ s] (a + x) := by
    simp only [nhdsWithin, Filter.map_inf (add_right_injective a)]
    simp [← Set.image_vadd]
-- 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
a : E
this : map (fun (x : E) ↦ a + x) (𝓝[s] x) = 𝓝[a +ᵥ s] (a + x)
⊢ HasFDerivWithinAt (fun (x : E) ↦ f (a + x)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (a + x)

Tactic:
simp [HasFDerivWithinAt, hasFDerivAtFilter_iff_isLittleOTVS, ← this, Function.comp_def]

Premises used: HasFDerivWithinAt, hasFDerivAtFilter_iff_isLittleOTVS, Function.comp_def
-- 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
a : E
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (x : E) ↦ f (a + x)) s x ↔
    DifferentiableWithinAt 𝕜 f (a +ᵥ s) (a + x)

Tactic:
simp [DifferentiableWithinAt, hasFDerivWithinAt_comp_add_left]

Premises used: DifferentiableWithinAt, hasFDerivWithinAt_comp_add_left