awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 𝕜
h : ¬DifferentiableAt 𝕜 f x
unfold : Eq.{v + 1} (α := F) (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F) (0 : F)
⊢ deriv f x = 0

Tactic:
unfold deriv

Premises used: deriv
-- 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 : 𝕜
h : ¬DifferentiableAt 𝕜 f x
rw : Eq.{v + 1} (α := F) ((0 : (a : 𝕜) → F) 1 : F) (0 : F)
⊢ Eq.{v + 1} (α := F) (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F) (0 : F)

Tactic:
rw [fderiv_zero_of_not_differentiableAt h]

Premises used: fderiv_zero_of_not_differentiableAt
-- 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 : 𝕜
h : ¬DifferentiableAt 𝕜 f 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 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
h : deriv f x ≠ 0
⊢ DifferentiableAt 𝕜 f x

Tactic:
not_imp_comm.1 deriv_zero_of_not_differentiableAt h

Premises used: deriv_zero_of_not_differentiableAt, not_imp_comm, Iff.mp
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' f₁' : F
x : 𝕜
s : Set 𝕜
H : UniqueDiffWithinAt 𝕜 s x
h : HasDerivWithinAt f f' s x
h₁ : HasDerivWithinAt f f₁' s x
⊢ f' = f₁'

Tactic:
toSpanSingleton_inj.mp <| UniqueDiffWithinAt.eq H h h₁

Premises used: Iff.mp, ContinuousLinearMap.toSpanSingleton_inj, UniqueDiffWithinAt.eq
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
L : Filter (𝕜 × 𝕜)
⊢ HasDerivAtFilter f f' L ↔
    IsLittleO.{u, v, u} (E := F) (F := 𝕜) L (fun (p : 𝕜 × 𝕜) ↦ f p.1 - f p.2 - (p.1 - p.2) • f') fun (p : 𝕜 × 𝕜) ↦
      p.1 - p.2

Tactic:
hasFDerivAtFilter_iff_isLittleO ..

Premises used: hasFDerivAtFilter_iff_isLittleO, HasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
L : Filter (𝕜 × 𝕜)
⊢ HasDerivAtFilter f f' L ↔
    Tendsto (β := ℝ) (fun (p : 𝕜 × 𝕜) ↦ ‖p.1 - p.2‖⁻¹ * ‖f p.1 - f p.2 - (p.1 - p.2) • f'‖) L (𝓝 0)

Tactic:
hasFDerivAtFilter_iff_tendsto

Premises used: HasDerivAtFilter, hasFDerivAtFilter_iff_tendsto
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
⊢ HasDerivWithinAt f f' s x ↔
    IsLittleO.{u, v, u} (E := F) (F := 𝕜) (𝓝[s] x) (fun (x' : 𝕜) ↦ f x' - f x - (x' - x) • f') fun (x' : 𝕜) ↦ x' - x

Tactic:
hasFDerivWithinAt_iff_isLittleO

Premises used: Set.Mem, setOf, HasDerivWithinAt, hasFDerivWithinAt_iff_isLittleO, HasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
⊢ HasDerivWithinAt f f' s x ↔ Tendsto (β := ℝ) (fun (x' : 𝕜) ↦ ‖x' - x‖⁻¹ * ‖f x' - f x - (x' - x) • f'‖) (𝓝[s] x) (𝓝 0)

Tactic:
hasFDerivWithinAt_iff_tendsto

Premises used: Set.Mem, setOf, HasDerivWithinAt, HasDerivAtFilter, hasFDerivWithinAt_iff_tendsto
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
⊢ HasDerivAt f f' x ↔
    IsLittleO.{u, v, u} (E := F) (F := 𝕜) (𝓝 x) (fun (x' : 𝕜) ↦ f x' - f x - (x' - x) • f') fun (x' : 𝕜) ↦ x' - x

Tactic:
hasFDerivAt_iff_isLittleO ..

Premises used: Set.Mem, HasDerivAt, setOf, hasFDerivAt_iff_isLittleO, HasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
⊢ HasDerivAt f f' x ↔ Tendsto (β := ℝ) (fun (x' : 𝕜) ↦ ‖x' - x‖⁻¹ * ‖f x' - f x - (x' - x) • f'‖) (𝓝 x) (𝓝 0)

Tactic:
hasFDerivAt_iff_tendsto

Premises used: Set.Mem, HasDerivAt, setOf, hasFDerivAt_iff_tendsto, HasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
⊢ IsBigO.{u, v, u} (E := F) (F := 𝕜) L (fun (p : 𝕜 × 𝕜) ↦ f p.1 - f p.2) fun (p : 𝕜 × 𝕜) ↦ p.1 - p.2

Tactic:
HasFDerivAtFilter.isBigO_sub h

Premises used: HasFDerivAtFilter.isBigO_sub
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
⊢ IsBigO.{u, v, u} (E := F) (F := 𝕜) (𝓝 x) (fun (x_1 : 𝕜) ↦ f x_1 - f x) fun (x_1 : 𝕜) ↦ x_1 - x

Tactic:
h.hasFDerivAt.isBigO_sub

Premises used: HasDerivAt.hasFDerivAt, HasFDerivAt.isBigO_sub
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f' : F
hf' : f' ≠ 0
⊢ Topology.IsInducing.{u, v} (X := 𝕜) (Y := F) (⇑(toSpanSingleton 𝕜 f') : (a : 𝕜) → F)

Tactic:
AntilipschitzWith.isInducing (K := ‖f'‖₊⁻¹) ?_ (map_continuous _)

Premises used: AntilipschitzWith.isInducing, ContinuousMapClass.map_continuous
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f' : F
hf' : f' ≠ 0
refine : AntilipschitzWith.{u, v} (α := 𝕜) (β := F) ‖f'‖₊⁻¹ (⇑(toSpanSingleton 𝕜 f') : (a : 𝕜) → F)
⊢ Topology.IsInducing.{u, v} (X := 𝕜) (Y := F) (⇑(toSpanSingleton 𝕜 f') : (a : 𝕜) → F)

Tactic:
refine AntilipschitzWith.isInducing (K := ‖f'‖₊⁻¹) ?_ (map_continuous _)

Premises used: AntilipschitzWith.isInducing, ContinuousMapClass.map_continuous
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f' : F
hf' : f' ≠ 0
⊢ AntilipschitzWith.{u, v} (α := 𝕜) (β := F) ‖f'‖₊⁻¹ (⇑(toSpanSingleton 𝕜 f') : (a : 𝕜) → F)

Tactic:
simp [antilipschitzWith_iff_le_mul_dist, dist_eq_norm, ← sub_smul, norm_smul, field]

Premises used: dist_eq_norm, norm_smul, antilipschitzWith_iff_le_mul_dist, sub_smul
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
L : Filter (𝕜 × 𝕜)
hf : HasDerivAtFilter f f' L
hf' : f' ≠ 0
⊢ IsEquivalent.{u, v} (E' := F) L (fun (p : 𝕜 × 𝕜) ↦ f p.1 - f p.2) fun (p : 𝕜 × 𝕜) ↦ (p.1 - p.2) • f'

Tactic:
HasFDerivAtFilter.isEquivalent_sub hf <| isInducing_toSpanSingleton hf'

Premises used: _private.0.isInducing_toSpanSingleton, HasFDerivAtFilter.isEquivalent_sub
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
L : Filter (𝕜 × 𝕜)
hf : HasDerivAtFilter f f' L
hf' : f' ≠ 0
⊢ IsTheta.{u, v, u} (E := F) (F := 𝕜) L (fun (p : 𝕜 × 𝕜) ↦ f p.1 - f p.2) fun (p : 𝕜 × 𝕜) ↦ p.1 - p.2

Tactic:
HasFDerivAtFilter.isTheta_sub hf <| isInducing_toSpanSingleton hf'

Premises used: _private.0.isInducing_toSpanSingleton, HasFDerivAtFilter.isTheta_sub
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
L : Filter (𝕜 × 𝕜)
hf : HasDerivAtFilter f f' L
hf' : f' ≠ 0
⊢ IsBigO.{u, u, v} (E := 𝕜) (F := F) L (fun (p : 𝕜 × 𝕜) ↦ p.1 - p.2) fun (p : 𝕜 × 𝕜) ↦ f p.1 - f p.2

Tactic:
hf.isTheta_sub hf' |>.isBigO_symm

Premises used: Asymptotics.IsTheta.isBigO_symm, HasDerivAtFilter.isTheta_sub
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
⊢ HasDerivAt f f' x

Tactic:
h.hasStrictFDerivAt.hasFDerivAt

Premises used: HasDerivAt, HasStrictDerivAt.hasStrictFDerivAt, HasStrictFDerivAt.hasFDerivAt, HasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s t : Set 𝕜
y : 𝕜
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ HasDerivWithinAt f f' s x ↔ HasDerivWithinAt f f' t x

Tactic:
hasFDerivWithinAt_congr_set' y h

Premises used: HasDerivWithinAt, HasDerivAtFilter, hasFDerivWithinAt_congr_set'
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s t : Set 𝕜
h : s =ᶠ[𝓝 x] t
⊢ HasDerivWithinAt f f' s x ↔ HasDerivWithinAt f f' t x

Tactic:
hasFDerivWithinAt_congr_set h

Premises used: HasDerivWithinAt, HasDerivAtFilter, hasFDerivWithinAt_congr_set
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
⊢ HasDerivWithinAt f f' (s \ {x}) x ↔ HasDerivWithinAt f f' s x

Tactic:
hasFDerivWithinAt_diff_singleton _

Premises used: HasDerivWithinAt, HasDerivAtFilter, hasFDerivWithinAt_diff_singleton
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
inst_3 : PartialOrder 𝕜
rw : HasDerivWithinAt f f' (Ici x \ {x}) x ↔ HasDerivWithinAt f f' (Ici x) x
rw₁ rw₂ : HasDerivWithinAt f f' (Ici x) x ↔ HasDerivWithinAt f f' (Ici x) x
⊢ HasDerivWithinAt f f' (Ioi x) x ↔ HasDerivWithinAt f f' (Ici x) x

Tactic:
rw [← Ici_diff_left, hasDerivWithinAt_diff_singleton]

Premises used: hasDerivWithinAt_diff_singleton, Set.Ici_diff_left
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
inst_3 : PartialOrder 𝕜
rw : HasDerivWithinAt f f' (Iic x \ {x}) x ↔ HasDerivWithinAt f f' (Iic x) x
rw₁ rw₂ : HasDerivWithinAt f f' (Iic x) x ↔ HasDerivWithinAt f f' (Iic x) x
⊢ HasDerivWithinAt f f' (Iio x) x ↔ HasDerivWithinAt f f' (Iic x) x

Tactic:
rw [← Iic_diff_right, hasDerivWithinAt_diff_singleton]

Premises used: hasDerivWithinAt_diff_singleton, Set.Iic_diff_right
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
inst_3 : LinearOrder 𝕜
inst_4 : OrderClosedTopology 𝕜
x y : 𝕜
h : x < y
⊢ HasDerivWithinAt f f' (Ioo x y) x ↔ HasDerivWithinAt f f' (Ioi x) x

Tactic:
hasFDerivWithinAt_inter <| Iio_mem_nhds h

Premises used: Set.Ioi, Iio_mem_nhds, Set.Mem, setOf, HasDerivWithinAt, Set.inter, HasDerivAtFilter, hasFDerivWithinAt_inter, Set.Ioo
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
⊢ HasDerivAt f f' x ↔
    IsLittleO.{u, v, u} (E := F) (F := 𝕜) (𝓝 0) (fun (h : 𝕜) ↦ f (x + h) - f x - h • f') fun (h : 𝕜) ↦ h

Tactic:
hasFDerivAt_iff_isLittleO_nhds_zero

Premises used: Set.Mem, HasDerivAt, setOf, HasDerivAtFilter, hasFDerivAt_iff_isLittleO_nhds_zero
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
L₁ L₂ : Filter (𝕜 × 𝕜)
h : HasDerivAtFilter f f' L₂
hst : L₁ ≤ L₂
⊢ HasDerivAtFilter f f' L₁

Tactic:
HasFDerivAtFilter.mono h hst

Premises used: HasFDerivAtFilter.mono, HasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s t : Set 𝕜
h : HasDerivWithinAt f f' t x
hst : s ⊆ t
⊢ HasDerivWithinAt f f' s x

Tactic:
HasFDerivWithinAt.mono h hst

Premises used: HasDerivWithinAt, HasDerivAtFilter, HasFDerivWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s t : Set 𝕜
h : HasDerivWithinAt f f' t x
hst : t ∈ 𝓝[s] x
⊢ HasDerivWithinAt f f' s x

Tactic:
HasFDerivWithinAt.mono_of_mem_nhdsWithin h hst

Premises used: HasDerivWithinAt, HasFDerivWithinAt.mono_of_mem_nhdsWithin, HasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
L : Filter (𝕜 × 𝕜)
h : HasDerivAt f f' x
hL : L ≤ SProd.sprod (β := Filter 𝕜) (𝓝 x) (pure x)
⊢ HasDerivAtFilter f f' L

Tactic:
HasFDerivAt.hasFDerivAtFilter h hL

Premises used: HasFDerivAt.hasFDerivAtFilter, HasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
h : HasDerivAt f f' x
⊢ HasDerivWithinAt f f' s x

Tactic:
HasFDerivAt.hasFDerivWithinAt h

Premises used: HasFDerivAt.hasFDerivWithinAt, HasDerivWithinAt, HasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
HasFDerivWithinAt.differentiableWithinAt h

Premises used: HasFDerivWithinAt.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
f' : F
x : 𝕜
h : HasDerivAt f f' x
⊢ DifferentiableAt 𝕜 f x

Tactic:
HasFDerivAt.differentiableAt h

Premises used: HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
⊢ HasDerivWithinAt f f' univ x ↔ HasDerivAt f f' x

Tactic:
hasFDerivWithinAt_univ

Premises used: HasDerivAt, HasDerivWithinAt, HasDerivAtFilter, hasFDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f₀' f₁' : F
x : 𝕜
h₀ : HasDerivAt f f₀' x
h₁ : HasDerivAt f f₁' x
⊢ f₀' = f₁'

Tactic:
toSpanSingleton_inj.mp <| h₀.hasFDerivAt.unique h₁

Premises used: HasDerivAt.hasFDerivAt, Iff.mp, HasFDerivAt.unique, ContinuousLinearMap.toSpanSingleton_inj
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s t : Set 𝕜
h : t ∈ 𝓝[s] x
⊢ HasDerivWithinAt f f' (s ∩ t) x ↔ HasDerivWithinAt f f' s x

Tactic:
hasFDerivWithinAt_inter' h

Premises used: hasFDerivWithinAt_inter', HasDerivWithinAt, HasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s t : Set 𝕜
h : t ∈ 𝓝 x
⊢ HasDerivWithinAt f f' (s ∩ t) x ↔ HasDerivWithinAt f f' s x

Tactic:
hasFDerivWithinAt_inter h

Premises used: HasDerivWithinAt, HasDerivAtFilter, hasFDerivWithinAt_inter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s t : Set 𝕜
hs : HasDerivWithinAt f f' s x
ht : HasDerivWithinAt f f' t x
⊢ HasDerivWithinAt f f' (s ∪ t) x

Tactic:
hs.hasFDerivWithinAt.union ht.hasFDerivWithinAt

Premises used: HasDerivWithinAt.hasFDerivWithinAt, HasDerivWithinAt, HasDerivAtFilter, HasFDerivWithinAt.union
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
hs : s ∈ 𝓝 x
⊢ HasDerivAt f f' x

Tactic:
HasFDerivWithinAt.hasFDerivAt h hs

Premises used: HasDerivAt, HasDerivAtFilter, HasFDerivWithinAt.hasFDerivAt
-- 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 : DifferentiableWithinAt 𝕜 f s x
⊢ HasDerivWithinAt f (derivWithin f s x) s x

Tactic:
h.hasFDerivWithinAt.hasDerivWithinAt

Premises used: HasFDerivWithinAt.hasDerivWithinAt, derivWithin, DifferentiableWithinAt.hasFDerivWithinAt
-- 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 : 𝕜
h : DifferentiableAt 𝕜 f x
⊢ HasDerivAt f (deriv f x) x

Tactic:
h.hasFDerivAt.hasDerivAt

Premises used: deriv, DifferentiableAt.hasFDerivAt, HasFDerivAt.hasDerivAt
-- 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 : 𝕜
⊢ HasDerivAt f (deriv f x) x ↔ DifferentiableAt 𝕜 f x

Tactic:
⟨fun h => h.differentiableAt, fun h => h.hasDerivAt⟩

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.differentiableAt, Iff.intro
-- 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 𝕜
⊢ HasDerivWithinAt f (derivWithin f s x) s x ↔ DifferentiableWithinAt 𝕜 f s x

Tactic:
⟨fun h => h.differentiableWithinAt, fun h => h.hasDerivWithinAt⟩

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.differentiableWithinAt, Iff.intro
-- 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 : DifferentiableOn 𝕜 f s
hs : s ∈ 𝓝 x
⊢ HasDerivAt f (deriv f x) x

Tactic:
(h.hasFDerivAt hs).hasDerivAt

Premises used: DifferentiableOn.hasFDerivAt, deriv, HasFDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
⊢ _root_.deriv f x = f'

Tactic:
h.differentiableAt.hasDerivAt.unique h

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.differentiableAt, HasDerivAt.unique
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
f f' : 𝕜 → F
h : ∀ (x : 𝕜), HasDerivAt f (f' x) x
⊢ deriv f = f'

Tactic:
funext fun x => (h x).deriv

Premises used: HasDerivAt.deriv, funext
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
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
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ _root_.derivWithin f s x = f'

Tactic:
hxs.eq_deriv _ h.differentiableWithinAt.hasDerivWithinAt h

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.differentiableWithinAt, UniqueDiffWithinAt.eq_deriv
-- 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 𝕜
⊢ ((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 = derivWithin f s x

Tactic:
rfl

Premises used: derivWithin, rfl
-- 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 𝕜
⊢ Eq (α := 𝕜 →L[𝕜] F) (toSpanSingleton 𝕜 (derivWithin f s x)) (fderivWithin 𝕜 f s x)

Tactic:
simp [derivWithin]

Premises used: derivWithin
-- 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 𝕜
⊢ ‖derivWithin f s x‖ = norm (E := 𝕜 →L[𝕜] F) (fderivWithin 𝕜 f s x)

Tactic:
simp [← toSpanSingleton_derivWithin]

Premises used: toSpanSingleton_derivWithin
-- 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 : 𝕜
⊢ ((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 = deriv f x

Tactic:
rfl

Premises used: deriv, rfl
-- 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 y : 𝕜
rw :
  Eq.{v + 1} (α := F) (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) y : F)
    (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) (HSMul.hSMul (β := 𝕜) y 1) : F)
⊢ ((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) y = y • deriv f x

Tactic:
rw [← fderiv_apply_one_eq_deriv, ← map_smul]

Premises used: fderiv_apply_one_eq_deriv, map_smul
-- 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 y : 𝕜
⊢ Eq.{v + 1} (α := F) (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) y : F)
    (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) (HSMul.hSMul (β := 𝕜) y 1) : F)

Tactic:
simp only [smul_eq_mul, mul_one]

Premises used: smul_eq_mul, mul_one
-- 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 : 𝕜
⊢ Eq (α := 𝕜 →L[𝕜] F) (toSpanSingleton 𝕜 (deriv f x)) (fderiv 𝕜 f x)

Tactic:
simp only [deriv, ContinuousLinearMap.toSpanSingleton_apply_map_one]

Premises used: deriv, ContinuousLinearMap.toSpanSingleton_apply_map_one
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
f : 𝕜 → 𝕜
x y : 𝕜
⊢ ((fderiv 𝕜 f x : 𝕜 →L[𝕜] 𝕜) : (a : 𝕜) → 𝕜) y = deriv f x * y

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- 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 : 𝕜
⊢ ‖deriv f x‖ = norm (E := 𝕜 →L[𝕜] F) (fderiv 𝕜 f x)

Tactic:
simp [← toSpanSingleton_deriv]

Premises used: toSpanSingleton_deriv
-- 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 : DifferentiableAt 𝕜 f x
hxs : UniqueDiffWithinAt 𝕜 s x
unfold :
  Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
    (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
⊢ _root_.derivWithin f s x = deriv f x

Tactic:
unfold _root_.derivWithin deriv

Premises used: deriv, derivWithin
-- 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 : DifferentiableAt 𝕜 f x
hxs : UniqueDiffWithinAt 𝕜 s x
rw rw₁ :
  Eq.{v + 1} (α := F) (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
    (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
⊢ Eq.{v + 1} (α := F) (((fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
    (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)

Tactic:
rw [h.fderivWithin hxs]

Premises used: DifferentiableAt.fderivWithin