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 g : 𝕜 → F
x : 𝕜
s : Set 𝕜
hf : DifferentiableWithinAt 𝕜 f s x
hg : DifferentiableWithinAt 𝕜 g s x
⊢ derivWithin (fun (y : 𝕜) ↦ f y - g y) s x = derivWithin f s x - derivWithin g s x

Tactic:
simp only [sub_eq_add_neg, derivWithin_fun_add hf hg.fun_neg, derivWithin.fun_neg]

Premises used: derivWithin.fun_neg, sub_eq_add_neg, DifferentiableWithinAt.fun_neg, 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 : 𝕜
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_sub hf hg

Premises used: derivWithin_fun_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
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.sub hg.hasDerivAt).deriv

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

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

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.deriv, HasDerivAt.sub
-- 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_sub_const_iff c

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

Tactic:
hasDerivAtFilter_sub_const_iff c

Premises used: HasDerivWithinAt, hasDerivAtFilter_sub_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_sub_const_iff c

Premises used: HasDerivAt, hasDerivAtFilter_sub_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_sub_const]

Premises used: fderivWithin_sub_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
c : F
h : ∀ (x : Set 𝕜) (x_1 : 𝕜), derivWithin (fun (x : 𝕜) ↦ f x - c) x x_1 = derivWithin f x x_1
⊢ (derivWithin fun (x : 𝕜) ↦ f x - c) = 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 : 𝕜) ↦ f x - c) x x_1 = derivWithin f x x_1

Tactic:
apply derivWithin_sub_const

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

Tactic:
simp only [deriv, fderiv_sub_const]

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

Tactic:
apply deriv_sub_const

Premises used: deriv_sub_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
hf : HasDerivAtFilter f f' L
⊢ HasDerivAtFilter (fun (x : 𝕜) ↦ c - f x) (-f') L

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

Premises used: sub_eq_add_neg, HasDerivAtFilter.const_add, 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 : 𝕜
s : Set 𝕜
c : F
hf : HasDerivWithinAt f f' s x
⊢ HasDerivWithinAt (fun (x : 𝕜) ↦ c - f x) (-f') s x

Tactic:
HasDerivAtFilter.const_sub c hf

Premises used: HasDerivWithinAt, HasDerivAtFilter.const_sub
-- 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
hf : HasStrictDerivAt f f' x
⊢ HasStrictDerivAt (fun (x : 𝕜) ↦ c - f x) (-f') x

Tactic:
HasDerivAtFilter.const_sub c hf

Premises used: HasStrictDerivAt, HasDerivAtFilter.const_sub
-- 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
hf : HasDerivAt f f' x
⊢ HasDerivAt (fun (x : 𝕜) ↦ c - f x) (-f') x

Tactic:
hf.const_sub c

Premises used: HasDerivAt, HasDerivAtFilter.const_sub
-- 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 : 𝕜) ↦ c - f y) s x = -derivWithin f s x

Tactic:
simp [sub_eq_add_neg, derivWithin.fun_neg]

Premises used: derivWithin.fun_neg, sub_eq_add_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 : 𝕜
c : F
⊢ deriv (fun (x : 𝕜) ↦ c - f x) x = -deriv f x

Tactic:
simp only [← derivWithin_univ, derivWithin_const_sub]

Premises used: derivWithin_univ, derivWithin_const_sub
-- 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
⊢ Eq (α := (x : 𝕜) → F) (deriv fun (x : 𝕜) ↦ c - f x) fun (x : 𝕜) ↦ -deriv f x

Tactic:
funext fun _ => deriv_const_sub c

Premises used: funext, deriv_const_sub
-- 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_sub c, deriv_id'']

Premises used: deriv_id'', deriv_const_sub
-- 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_sub_id c

Premises used: deriv_const_sub_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:
simp [sub_eq_add_neg, differentiableAt_comp_add_const]

Premises used: differentiableAt_comp_add_const, sub_eq_add_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
a b : 𝕜
⊢ DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (b - x)) a ↔ DifferentiableAt 𝕜 f (b - a)

Tactic:
⟨fun H ↦ ?_, fun H ↦ H.comp a (differentiable_id.const_sub _).differentiableAt⟩

Premises used: Differentiable.const_sub, Differentiable.differentiableAt, Iff.intro, DifferentiableAt.comp, differentiable_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 b : 𝕜
refine : ∀ (H : DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (b - x)) a), DifferentiableAt 𝕜 f (b - a)
⊢ DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (b - x)) a ↔ DifferentiableAt 𝕜 f (b - a)

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ H.comp a (differentiable_id.const_sub _).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 b : 𝕜
H : DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (b - x)) a
h : f = (fun (x : 𝕜) ↦ f (b - x)) ∘ HSub.hSub b
⊢ DifferentiableAt 𝕜 f (b - a)

Tactic:
convert!
    ((sub_sub_cancel _ a).symm ▸ H).comp (b - a) (differentiable_id.const_sub _).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 b : 𝕜
H : DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (b - x)) a
h : ∀ (x : 𝕜), f x = ((fun (x : 𝕜) ↦ f (b - x)) ∘ HSub.hSub b) x
⊢ f = (fun (x : 𝕜) ↦ f (b - x)) ∘ HSub.hSub b

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 b : 𝕜
H : DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (b - x)) a
x : 𝕜
⊢ f x = ((fun (x : 𝕜) ↦ f (b - x)) ∘ HSub.hSub b) 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
f : 𝕜 → F
a b : 𝕜
⊢ DifferentiableAt 𝕜 f a ↔ DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (x - b)) (a + b)

Tactic:
simp [sub_eq_add_neg, differentiableAt_comp_add_const]

Premises used: differentiableAt_comp_add_const, sub_eq_add_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
a b : 𝕜
⊢ DifferentiableAt 𝕜 f a ↔ DifferentiableAt.{u, u, v} 𝕜 (F := F) (fun (x : 𝕜) ↦ f (b - x)) (b - a)

Tactic:
simp [differentiableAt_comp_const_sub]

Premises used: differentiableAt_comp_const_sub
-- Module: Mathlib.Analysis.Calculus.Deriv.AffineMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
L : Filter (𝕜 × 𝕜)
rw :
  HasDerivAtFilter (HAdd.hAdd (α := (a : 𝕜) → E) (⇑f.linear : (a : 𝕜) → E) fun (x : 𝕜) ↦ (f : (a : 𝕜) → E) 0)
    ((f.linear : (a : 𝕜) → E) 1) L
⊢ HasDerivAtFilter.{u_1, u_2} (F := E) ((⇑f : (a : 𝕜) → E) : (a : 𝕜) → E) ((f.linear : (a : 𝕜) → E) 1 : E) L

Tactic:
rw [f.decomp]

Premises used: AffineMap.decomp
-- Module: Mathlib.Analysis.Calculus.Deriv.AffineMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
L : Filter (𝕜 × 𝕜)
⊢ HasDerivAtFilter (HAdd.hAdd (α := (a : 𝕜) → E) (⇑f.linear : (a : 𝕜) → E) fun (x : 𝕜) ↦ (f : (a : 𝕜) → E) 0)
    ((f.linear : (a : 𝕜) → E) 1) L

Tactic:
f.linear.hasDerivAtFilter.add_const (f 0)

Premises used: HasDerivAtFilter.add_const, AffineMap.linear, OfNat.ofNat, LinearMap.hasDerivAtFilter, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.Deriv.AffineMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
L : Filter (𝕜 × 𝕜)
⊢ HasDerivAtFilter (HAdd.hAdd (α := (a : 𝕜) → E) (⇑f.linear : (a : 𝕜) → E) fun (x : 𝕜) ↦ (f : (a : 𝕜) → E) 0)
    ((f.linear : (a : 𝕜) → E) 1) L

Tactic:
exact f.linear.hasDerivAtFilter.add_const (f 0)

Premises used: HasDerivAtFilter.add_const, AffineMap.linear, OfNat.ofNat, LinearMap.hasDerivAtFilter, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.Deriv.AffineMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
x : 𝕜
⊢ HasStrictDerivAt.{u_1, u_2} (F := E) ((⇑f : (a : 𝕜) → E) : (a : 𝕜) → E) ((f.linear : (a : 𝕜) → E) 1 : E) x

Tactic:
f.hasDerivAtFilter

Premises used: AffineMap.hasDerivAtFilter, HasStrictDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.AffineMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
s : Set 𝕜
x : 𝕜
⊢ HasDerivWithinAt.{u_1, u_2} (F := E) ((⇑f : (a : 𝕜) → E) : (a : 𝕜) → E) ((f.linear : (a : 𝕜) → E) 1 : E) s x

Tactic:
f.hasDerivAtFilter

Premises used: AffineMap.hasDerivAtFilter, HasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.AffineMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
x : 𝕜
⊢ HasDerivAt.{u_1, u_2} (F := E) ((⇑f : (a : 𝕜) → E) : (a : 𝕜) → E) ((f.linear : (a : 𝕜) → E) 1 : E) x

Tactic:
f.hasDerivAtFilter

Premises used: AffineMap.hasDerivAtFilter, HasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.AffineMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
s : Set 𝕜
x : 𝕜
hs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq.{u_2 + 1} (α := E) (derivWithin (⇑f : (a : 𝕜) → E) s x : E) ((f.linear : (a : 𝕜) → E) 1 : E)

Tactic:
f.hasDerivWithinAt.derivWithin hs

Premises used: AffineMap.hasDerivWithinAt, HasDerivWithinAt.derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.AffineMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
x : 𝕜
⊢ Eq.{u_2 + 1} (α := E) (deriv (⇑f : (a : 𝕜) → E) x : E) ((f.linear : (a : 𝕜) → E) 1 : E)

Tactic:
f.hasDerivAt.deriv

Premises used: HasDerivAt.deriv, AffineMap.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.AffineMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
x : 𝕜
⊢ DifferentiableAt.{u_1, u_1, u_2} 𝕜 (F := E) (⇑f : (a : 𝕜) → E) x

Tactic:
f.hasDerivAt.differentiableAt

Premises used: HasDerivAt.differentiableAt, AffineMap.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.AffineMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
⊢ Differentiable.{u_1, u_1, u_2} 𝕜 (E := 𝕜) (F := E) (⇑f : (a : 𝕜) → E)

Tactic:
fun _ ↦ f.differentiableAt

Premises used: Differentiable, AffineMap.differentiableAt
-- Module: Mathlib.Analysis.Calculus.Deriv.AffineMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
s : Set 𝕜
x : 𝕜
⊢ DifferentiableWithinAt.{u_1, u_1, u_2} 𝕜 (F := E) (⇑f : (a : 𝕜) → E) s x

Tactic:
f.differentiableAt.differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, AffineMap.differentiableAt
-- Module: Mathlib.Analysis.Calculus.Deriv.AffineMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
s : Set 𝕜
⊢ DifferentiableOn.{u_1, u_1, u_2} 𝕜 (F := E) (⇑f : (a : 𝕜) → E) s

Tactic:
fun _ _ ↦ f.differentiableWithinAt

Premises used: AffineMap.differentiableWithinAt, DifferentiableOn
-- Module: Mathlib.Analysis.Calculus.Deriv.AffineMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : E
x : 𝕜
⊢ HasStrictDerivAt (⇑(lineMap a b) : (a : 𝕜) → E) (b - a) x

Tactic:
simpa using (lineMap a b : 𝕜 →ᵃ[𝕜] E).hasStrictDerivAt

Premises used: AffineMap.lineMap, AffineMap.hasStrictDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.AffineMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : E
x : 𝕜
⊢ HasDerivAt (⇑(lineMap a b) : (a : 𝕜) → E) (b - a) x

Tactic:
hasStrictDerivAt_lineMap.hasDerivAt

Premises used: AffineMap.hasStrictDerivAt_lineMap, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.AffineMap
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
a b : E
s : Set 𝕜
x : 𝕜
⊢ HasDerivWithinAt (⇑(lineMap a b) : (a : 𝕜) → E) (b - a) s x

Tactic:
hasDerivAt_lineMap.hasDerivWithinAt

Premises used: HasDerivAt.hasDerivWithinAt, AffineMap.hasDerivAt_lineMap
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : TopologicalSpace F
f : 𝕜 → F
L : Filter (𝕜 × 𝕜)
inst_4 : ContinuousSMul 𝕜 F
f' : 𝕜 →L[𝕜] F
⊢ HasFDerivAtFilter (𝕜 := 𝕜) f f' L ↔ HasDerivAtFilter f ((f' : (a : 𝕜) → F) 1) L

Tactic:
simp [HasDerivAtFilter]

Premises used: HasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : TopologicalSpace F
f : 𝕜 → F
f' : F
L : Filter (𝕜 × 𝕜)
inst_4 : ContinuousSMul 𝕜 F
⊢ HasDerivAtFilter f f' L ↔ HasFDerivAtFilter (𝕜 := 𝕜) f (toSpanSingleton 𝕜 f') L

Tactic:
.rfl

Premises used: Iff.rfl, HasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
inst_4 : ContinuousSMul 𝕜 F
f' : 𝕜 →L[𝕜] F
⊢ HasFDerivWithinAt (𝕜 := 𝕜) f f' s x ↔ HasDerivWithinAt f ((f' : (a : 𝕜) → F) 1) s x

Tactic:
hasFDerivAtFilter_iff_hasDerivAtFilter

Premises used: HasDerivWithinAt, HasFDerivWithinAt, hasFDerivAtFilter_iff_hasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
inst_4 : ContinuousSMul 𝕜 F
f' : F
⊢ HasDerivWithinAt f f' s x ↔ HasFDerivWithinAt (𝕜 := 𝕜) f (toSpanSingleton 𝕜 f') s x

Tactic:
Iff.rfl

Premises used: Iff.rfl, HasFDerivWithinAt, HasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
inst_4 : ContinuousSMul 𝕜 F
f' : 𝕜 →L[𝕜] F
⊢ HasFDerivAt (𝕜 := 𝕜) f f' x ↔ HasDerivAt f ((f' : (a : 𝕜) → F) 1) x

Tactic:
hasFDerivAtFilter_iff_hasDerivAtFilter

Premises used: HasFDerivAt, HasDerivAt, hasFDerivAtFilter_iff_hasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
inst_4 : ContinuousSMul 𝕜 F
f' : F
⊢ HasDerivAt f f' x ↔ HasFDerivAt (𝕜 := 𝕜) f (toSpanSingleton 𝕜 f') x

Tactic:
Iff.rfl

Premises used: HasFDerivAt, Iff.rfl, HasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
inst_4 : ContinuousSMul 𝕜 F
f' : 𝕜 →L[𝕜] F
⊢ HasStrictFDerivAt (𝕜 := 𝕜) f f' x ↔ HasStrictDerivAt f ((f' : (a : 𝕜) → F) 1) x

Tactic:
hasFDerivAtFilter_iff_hasDerivAtFilter

Premises used: hasFDerivAtFilter_iff_hasDerivAtFilter, HasStrictFDerivAt, HasStrictDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : TopologicalSpace F
f : 𝕜 → F
f' : F
x : 𝕜
inst_4 : ContinuousSMul 𝕜 F
⊢ HasStrictDerivAt f f' x ↔ HasStrictFDerivAt (𝕜 := 𝕜) f (toSpanSingleton 𝕜 f') x

Tactic:
Iff.rfl

Premises used: Iff.rfl, HasDerivAtFilter, HasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬DifferentiableWithinAt 𝕜 f s x
unfold : Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F) (0 : F)
⊢ derivWithin f s x = 0

Tactic:
unfold derivWithin

Premises used: derivWithin
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬DifferentiableWithinAt 𝕜 f s x
rw : Eq.{v + 1} (α := F) ((0 : (a : 𝕜) → F) 1 : F) (0 : F)
⊢ Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F) (0 : F)

Tactic:
rw [fderivWithin_zero_of_not_differentiableWithinAt h]

Premises used: fderivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬DifferentiableWithinAt 𝕜 f s x
⊢ Eq.{v + 1} (α := F) ((0 : (a : 𝕜) → F) 1 : F) (0 : F)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : derivWithin f s x ≠ 0
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
not_imp_comm.1 derivWithin_zero_of_not_differentiableWithinAt h

Premises used: not_imp_comm, Iff.mp, derivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬AccPt x (𝓟 s)
rw : Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F) (0 : F)
rw₁ : Eq.{v + 1} (α := F) ((0 : (a : 𝕜) → F) 1 : F) (0 : F)
rw₂ rw₃ : Eq.{v + 1} (α := F) 0 0
⊢ derivWithin f s x = 0

Tactic:
rw [derivWithin, fderivWithin_zero_of_not_accPt h, ContinuousLinearMap.zero_apply]

Premises used: fderivWithin_zero_of_not_accPt, derivWithin, ContinuousLinearMap.zero_apply
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin f s x = 0

Tactic:
derivWithin_zero_of_not_accPt <| mt AccPt.uniqueDiffWithinAt h

Premises used: mt, derivWithin_zero_of_not_accPt, AccPt.uniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : x ∉ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
rw : Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F) (0 : F)
rw₁ : Eq.{v + 1} (α := F) ((0 : (a : 𝕜) → F) 1 : F) (0 : F)
rw₂ rw₃ : Eq.{v + 1} (α := F) 0 0
⊢ derivWithin f s x = 0

Tactic:
rw [derivWithin, fderivWithin_zero_of_notMem_closure h, ContinuousLinearMap.zero_apply]

Premises used: fderivWithin_zero_of_notMem_closure, derivWithin, ContinuousLinearMap.zero_apply