awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x ≠ 0
e_8 : instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
h :
  ∀ (y : E),
    Eq (α := ℝ) ((HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) f' : (a : E) → ℝ) y : ℝ)
      ((ContinuousLinearMap.toSpanSingleton ℝ (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) ∘SL f' : (a : E) → ℝ)
          y :
        ℝ)
⊢ HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) f' =
    ContinuousLinearMap.toSpanSingleton ℝ (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) ∘SL f'

Tactic:
ext y
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasStrictFDerivAt f f' x
h₀ : f x ≠ 0
e_8 : instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
y : E
⊢ Eq (α := ℝ) ((HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) f' : (a : E) → ℝ) y : ℝ)
    ((ContinuousLinearMap.toSpanSingleton ℝ (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) ∘SL f' : (a : E) → ℝ)
        y :
      ℝ)

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasFDerivAt f f' x
h₀ : f x ≠ 0
⊢ HasFDerivAt (F := ℝ) ((fun (x : ℝ) ↦ |x|) ∘ f)
    (ContinuousLinearMap.toSpanSingleton ℝ (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) ∘SL f') x

Tactic:
(hasDerivAt_abs h₀).hasFDerivAt.comp x hf

Premises used: HasDerivAt.hasFDerivAt, hasDerivAt_abs, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasFDerivAt f f' x
h₀ : f x ≠ 0
h :
  instAddCommGroup = NormedAddCommGroup.toAddCommGroup →
    HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule →
      HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) f' =
        ContinuousLinearMap.toSpanSingleton ℝ (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) ∘SL f'
⊢ HasFDerivAt (fun (x : E) ↦ |f x|) (HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) f') x

Tactic:
convert! (hasDerivAt_abs h₀).hasFDerivAt.comp x hf using 1

Premises used: HasDerivAt.hasFDerivAt, hasDerivAt_abs, HasFDerivAt.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasFDerivAt f f' x
h₀ : f x ≠ 0
e_8 : instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
h :
  ∀ (y : E),
    Eq (α := ℝ) ((HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) f' : (a : E) → ℝ) y : ℝ)
      ((ContinuousLinearMap.toSpanSingleton ℝ (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) ∘SL f' : (a : E) → ℝ)
          y :
        ℝ)
⊢ HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) f' =
    ContinuousLinearMap.toSpanSingleton ℝ (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) ∘SL f'

Tactic:
ext y
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
x : E
hf : HasFDerivAt f f' x
h₀ : f x ≠ 0
e_8 : instAddCommGroup = NormedAddCommGroup.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
y : E
⊢ Eq (α := ℝ) ((HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) f' : (a : E) → ℝ) y : ℝ)
    ((ContinuousLinearMap.toSpanSingleton ℝ (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) ∘SL f' : (a : E) → ℝ)
        y :
      ℝ)

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
s : Set ℝ
x : ℝ
hx : x < 0
⊢ HasDerivWithinAt (F := ℝ) (fun (x : ℝ) ↦ |x|) (-1) s x

Tactic:
(hasDerivAt_abs_neg hx).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, hasDerivAt_abs_neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
s : Set ℝ
x : ℝ
hx : 0 < x
⊢ HasDerivWithinAt (F := ℝ) (fun (x : ℝ) ↦ |x|) 1 s x

Tactic:
(hasDerivAt_abs_pos hx).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, hasDerivAt_abs_pos
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
s : Set ℝ
x : ℝ
hx : x ≠ 0
⊢ HasDerivWithinAt (F := ℝ) (fun (x : ℝ) ↦ |x|) (↑((SignType.sign : (a : ℝ) → SignType) x) : ℝ) s x

Tactic:
(hasDerivAt_abs hx).hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, hasDerivAt_abs
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
x : E
hf : HasFDerivWithinAt f f' s x
h₀ : f x < 0
⊢ HasFDerivWithinAt ((fun (x : ℝ) ↦ |x|) ∘ f) (HSMul.hSMul (α := ℝ) (-1) f') s x

Tactic:
(hasDerivAt_abs_neg h₀).comp_hasFDerivWithinAt x hf

Premises used: HasDerivAt.comp_hasFDerivWithinAt, hasDerivAt_abs_neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
x : E
hf : HasFDerivWithinAt f f' s x
h₀ : f x < 0
h :
  instAddCommGroup = Ring.toAddCommGroup →
    HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule → -f' = HSMul.hSMul (α := ℝ) (-1) f'
⊢ HasFDerivWithinAt (fun (x : E) ↦ |f x|) (-f') s x

Tactic:
convert! (hasDerivAt_abs_neg h₀).comp_hasFDerivWithinAt x hf using 1

Premises used: HasDerivAt.comp_hasFDerivWithinAt, hasDerivAt_abs_neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
x : E
hf : HasFDerivWithinAt f f' s x
h₀ : f x < 0
e_8 : instAddCommGroup = Ring.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
⊢ -f' = HSMul.hSMul (α := ℝ) (-1) f'

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
x : E
hf : HasFDerivWithinAt f f' s x
h₀ : 0 < f x
⊢ HasFDerivWithinAt ((fun (x : ℝ) ↦ |x|) ∘ f) (HSMul.hSMul (α := ℝ) 1 f') s x

Tactic:
(hasDerivAt_abs_pos h₀).comp_hasFDerivWithinAt x hf

Premises used: HasDerivAt.comp_hasFDerivWithinAt, hasDerivAt_abs_pos
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
x : E
hf : HasFDerivWithinAt f f' s x
h₀ : 0 < f x
h :
  instAddCommGroup = Ring.toAddCommGroup →
    HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule → f' = HSMul.hSMul (α := ℝ) 1 f'
⊢ HasFDerivWithinAt (fun (x : E) ↦ |f x|) f' s x

Tactic:
convert! (hasDerivAt_abs_pos h₀).comp_hasFDerivWithinAt x hf using 1

Premises used: HasDerivAt.comp_hasFDerivWithinAt, hasDerivAt_abs_pos
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
x : E
hf : HasFDerivWithinAt f f' s x
h₀ : 0 < f x
e_8 : instAddCommGroup = Ring.toAddCommGroup
e_9 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) NormedSpace.toModule
⊢ f' = HSMul.hSMul (α := ℝ) 1 f'

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
x : E
hf : HasFDerivWithinAt f f' s x
h₀ : f x ≠ 0
⊢ HasFDerivWithinAt (fun (x : E) ↦ |f x|) (HSMul.hSMul (α := ℝ) (↑((SignType.sign : (a : ℝ) → SignType) (f x)) : ℝ) f')
    s x

Tactic:
(hasDerivAt_abs h₀).comp_hasFDerivWithinAt x hf

Premises used: abs, HasDerivAt.comp_hasFDerivWithinAt, hasDerivAt_abs
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
x : ℝ
hx : x < 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ |x|) x

Tactic:
(hasDerivAt_abs_neg hx).differentiableAt

Premises used: hasDerivAt_abs_neg, HasDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ |x|) x

Tactic:
(hasDerivAt_abs_pos hx).differentiableAt

Premises used: HasDerivAt.differentiableAt, hasDerivAt_abs_pos
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
x : ℝ
hx : x ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : ℝ) ↦ |x|) x

Tactic:
(hasDerivAt_abs hx).differentiableAt

Premises used: HasDerivAt.differentiableAt, hasDerivAt_abs
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
hf : DifferentiableAt ℝ f x
h₀ : f x < 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ |f x|) x

Tactic:
(differentiableAt_abs_neg h₀).comp x hf

Premises used: abs, differentiableAt_abs_neg, DifferentiableAt.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
hf : DifferentiableAt ℝ f x
h₀ : 0 < f x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ |f x|) x

Tactic:
(differentiableAt_abs_pos h₀).comp x hf

Premises used: abs, differentiableAt_abs_pos, DifferentiableAt.comp
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
hf : DifferentiableAt ℝ f x
h₀ : f x ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (x : E) ↦ |f x|) x

Tactic:
(differentiableAt_abs h₀).comp x hf

Premises used: abs, DifferentiableAt.comp, differentiableAt_abs
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
s : Set ℝ
x : ℝ
hx : x < 0
⊢ DifferentiableWithinAt ℝ (F := ℝ) (fun (x : ℝ) ↦ |x|) s x

Tactic:
(differentiableAt_abs_neg hx).differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, differentiableAt_abs_neg
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
s : Set ℝ
x : ℝ
hx : 0 < x
⊢ DifferentiableWithinAt ℝ (F := ℝ) (fun (x : ℝ) ↦ |x|) s x

Tactic:
(differentiableAt_abs_pos hx).differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, differentiableAt_abs_pos
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
s : Set ℝ
x : ℝ
hx : x ≠ 0
⊢ DifferentiableWithinAt ℝ (F := ℝ) (fun (x : ℝ) ↦ |x|) s x

Tactic:
(differentiableAt_abs hx).differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, differentiableAt_abs
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x : E
hf : DifferentiableWithinAt ℝ f s x
h₀ : f x < 0
⊢ DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ |f x|) s x

Tactic:
(differentiableAt_abs_neg h₀).comp_differentiableWithinAt x hf

Premises used: abs, differentiableAt_abs_neg, DifferentiableAt.comp_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x : E
hf : DifferentiableWithinAt ℝ f s x
h₀ : 0 < f x
⊢ DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ |f x|) s x

Tactic:
(differentiableAt_abs_pos h₀).comp_differentiableWithinAt x hf

Premises used: abs, differentiableAt_abs_pos, DifferentiableAt.comp_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x : E
hf : DifferentiableWithinAt ℝ f s x
h₀ : f x ≠ 0
⊢ DifferentiableWithinAt ℝ (F := ℝ) (fun (x : E) ↦ |f x|) s x

Tactic:
(differentiableAt_abs h₀).comp_differentiableWithinAt x hf

Premises used: abs, DifferentiableAt.comp_differentiableWithinAt, differentiableAt_abs
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
s : Set ℝ
hs : ∀ x ∈ s, x ≠ 0
⊢ DifferentiableOn ℝ (F := ℝ) (fun (x : ℝ) ↦ |x|) s

Tactic:
fun x hx ↦ differentiableWithinAt_abs s (hs x hx)

Premises used: differentiableWithinAt_abs, DifferentiableOn
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
hf : DifferentiableOn ℝ f s
h₀ : ∀ x ∈ s, f x ≠ 0
⊢ DifferentiableOn ℝ (F := ℝ) (fun (x : E) ↦ |f x|) s

Tactic:
fun x hx ↦ (hf x hx).abs (h₀ x hx)

Premises used: DifferentiableWithinAt.abs, DifferentiableOn
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
hf : Differentiable ℝ f
h₀ : ∀ (x : E), f x ≠ 0
⊢ Differentiable ℝ (F := ℝ) fun (x : E) ↦ |f x|

Tactic:
fun x ↦ (hf x).abs (h₀ x)

Premises used: Differentiable, DifferentiableAt.abs
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
h : DifferentiableAt ℝ (E := ℝ) abs 0
⊢ Eq (α := ℝ) (deriv abs 0) 1

Tactic:
have h₁ : deriv abs (0 : ℝ) = 1 :=
    (uniqueDiffOn_Ici _ _ Set.self_mem_Ici).eq_deriv _ h.hasDerivAt.hasDerivWithinAt <|
      (hasDerivWithinAt_id _ _).congr_of_mem (fun _ h ↦ abs_of_nonneg h) Set.self_mem_Ici
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
h : DifferentiableAt ℝ (E := ℝ) abs 0
h₁ : Eq (α := ℝ) (deriv abs 0) 1
⊢ Eq (α := ℝ) (deriv abs 0) (-1)

Tactic:
have h₂ : deriv abs (0 : ℝ) = -1 :=
    (uniqueDiffOn_Iic _ _ Set.self_mem_Iic).eq_deriv _ h.hasDerivAt.hasDerivWithinAt <|
      (hasDerivWithinAt_neg _ _).congr_of_mem (fun _ h ↦ abs_of_nonpos h) Set.self_mem_Iic
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
h : DifferentiableAt ℝ (E := ℝ) abs 0
h₁ : Eq (α := ℝ) (deriv abs 0) 1
h₂ : Eq (α := ℝ) (deriv abs 0) (-1)
linarith : HMul.hMul (α := ℝ) 2 (-1) + -HSub.hSub (α := ℝ) (deriv abs 0) 1 + HSub.hSub (α := ℝ) (deriv abs 0) (-1) = 0
linarith₁ : GT.gt (α := ℝ) 2 0
⊢ False

Tactic:
linarith
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
x : ℝ
hx : x < 0
⊢ Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ |x|) x) (-1)

Tactic:
(hasDerivAt_abs_neg hx).deriv

Premises used: hasDerivAt_abs_neg, HasDerivAt.deriv
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
x : ℝ
hx : 0 < x
⊢ Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ |x|) x) 1

Tactic:
(hasDerivAt_abs_pos hx).deriv

Premises used: HasDerivAt.deriv, hasDerivAt_abs_pos
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
⊢ Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ |x|) 0) 0

Tactic:
deriv_zero_of_not_differentiableAt not_differentiableAt_abs_zero

Premises used: deriv_zero_of_not_differentiableAt, not_differentiableAt_abs_zero
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
x : ℝ
inl : Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ |x|) 0) (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℝ)
inr : ∀ (hx : x ≠ 0), Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ |x|) x) (↑((SignType.sign : (a : ℝ) → SignType) x) : ℝ)
⊢ Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ |x|) x) (↑((SignType.sign : (a : ℝ) → SignType) x) : ℝ)

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
⊢ Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ |x|) 0) (↑((SignType.sign : (a : ℝ) → SignType) 0) : ℝ)

Tactic:
simpa using deriv_abs_zero

Premises used: deriv_abs_zero
-- Module: Mathlib.Analysis.Calculus.Deriv.Abs
Goal:
x : ℝ
hx : x ≠ 0
⊢ Eq (α := ℝ) (deriv (fun (x : ℝ) ↦ |x|) x) (↑((SignType.sign : (a : ℝ) → SignType) x) : ℝ)

Tactic:
simpa [hx] using (hasDerivAt_abs hx).deriv

Premises used: HasDerivAt.deriv, hasDerivAt_abs
-- 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 using (hf.hasFDerivAtFilter.add hg.hasFDerivAtFilter).hasDerivAtFilter

Premises used: HasFDerivAtFilter.add, HasDerivAtFilter.hasFDerivAtFilter, 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 g : 𝕜 → F
f' g' : F
x : 𝕜
hf : HasStrictDerivAt f f' x
hg : HasStrictDerivAt g g' x
⊢ HasStrictDerivAt (f + g) (f' + g') x

Tactic:
HasDerivAtFilter.add hf hg

Premises used: HasDerivAtFilter.add, HasStrictDerivAt
-- 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.add hf hg

Premises used: HasDerivAtFilter.add, 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.add hf hg

Premises used: HasDerivAtFilter.add, HasDerivAt
-- 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
x : 𝕜
s : Set 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
pos :
  ∀ (hsx : UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ f y + g y) s x = derivWithin f s x + derivWithin g s x
neg :
  ∀ (hsx : ¬UniqueDiffWithinAt 𝕜 s x), derivWithin (fun (y : 𝕜) ↦ f y + g y) s x = derivWithin f s x + derivWithin g s x
⊢ derivWithin (fun (y : 𝕜) ↦ f y + g y) s x = derivWithin f s x + derivWithin g 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 g : 𝕜 → F
x : 𝕜
s : Set 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ f y + g y) s x = derivWithin f s x + derivWithin g s x

Tactic:
(hf.hasDerivWithinAt.add hg.hasDerivWithinAt).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.add
-- 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
x : 𝕜
s : Set 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
hsx : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ f y + g y) s x = derivWithin f s x + derivWithin g s x

Tactic:
exact (hf.hasDerivWithinAt.add hg.hasDerivWithinAt).derivWithin hsx

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.derivWithin, HasDerivWithinAt.add
-- 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
x : 𝕜
s : Set 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
hsx : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun (y : 𝕜) ↦ f y + g y) s x = derivWithin f s x + derivWithin g 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 g : 𝕜 → F
x : 𝕜
s : Set 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
⊢ derivWithin (f + g) s x = derivWithin f s x + derivWithin g s x

Tactic:
derivWithin_fun_add hf hg

Premises used: derivWithin_fun_add
-- 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
x : 𝕜
hf : DifferentiableAt 𝕜 f x
hg : DifferentiableAt 𝕜 g x
⊢ deriv (fun (y : 𝕜) ↦ f y + g y) x = deriv f x + deriv g x

Tactic:
(hf.hasDerivAt.add hg.hasDerivAt).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.add, HasDerivAt.deriv
-- 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
x : 𝕜
hf : DifferentiableAt 𝕜 f x
hg : DifferentiableAt 𝕜 g x
⊢ deriv (f + g) x = deriv f x + deriv g x

Tactic:
(hf.hasDerivAt.add hg.hasDerivAt).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.add, HasDerivAt.deriv
-- 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 (𝕜 × 𝕜)
c : F
⊢ HasDerivAtFilter (fun (x : 𝕜) ↦ f x + c) f' L ↔ HasDerivAtFilter f f' L

Tactic:
hasFDerivAtFilter_add_const_iff c

Premises used: HasDerivAtFilter, hasFDerivAtFilter_add_const_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
f' : F
x : 𝕜
c : F
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ f x + c) f' x ↔ HasStrictDerivAt f f' x

Tactic:
hasDerivAtFilter_add_const_iff c

Premises used: hasDerivAtFilter_add_const_iff, HasStrictDerivAt
-- 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 𝕜
c : F
⊢ HasDerivWithinAt (fun (x : 𝕜) ↦ f x + c) f' s x ↔ HasDerivWithinAt f f' s x

Tactic:
hasDerivAtFilter_add_const_iff c

Premises used: HasDerivWithinAt, hasDerivAtFilter_add_const_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
f' : F
x : 𝕜
c : F
⊢ HasDerivAt (fun (x : 𝕜) ↦ f x + c) f' x ↔ HasDerivAt f f' x

Tactic:
hasDerivAtFilter_add_const_iff c

Premises used: HasDerivAt, hasDerivAtFilter_add_const_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 (y : 𝕜) ↦ f y + c) s x = derivWithin f s x

Tactic:
simp only [derivWithin, fderivWithin_add_const]

Premises used: fderivWithin_add_const, 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
x : 𝕜
c : F
⊢ deriv (fun (y : 𝕜) ↦ f y + c) x = deriv f x

Tactic:
simp only [deriv, fderiv_add_const]

Premises used: fderiv_add_const, deriv
-- 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 (y : 𝕜) ↦ f y + c) = deriv f

Tactic:
funext fun _ ↦ deriv_add_const c

Premises used: funext, deriv_add_const
-- 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 (𝕜 × 𝕜)
c : F
⊢ HasDerivAtFilter (fun (x : 𝕜) ↦ c + f x) f' L ↔ HasDerivAtFilter f f' L

Tactic:
hasFDerivAtFilter_const_add_iff c

Premises used: HasDerivAtFilter, hasFDerivAtFilter_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
f' : F
x : 𝕜
c : F
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ c + f x) f' x ↔ HasStrictDerivAt f f' x

Tactic:
hasDerivAtFilter_const_add_iff c

Premises used: hasDerivAtFilter_const_add_iff, HasStrictDerivAt
-- 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 𝕜
c : F
⊢ HasDerivWithinAt (fun (x : 𝕜) ↦ c + f x) f' s x ↔ HasDerivWithinAt f f' s x

Tactic:
hasDerivAtFilter_const_add_iff c

Premises used: HasDerivWithinAt, hasDerivAtFilter_const_add_iff