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₁ : 𝕜 → F
x : 𝕜
hL : f₁ =ᶠ[𝓝 x] f
rwa :
  Eq.{v + 1} (α := F) (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
    (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
rwa₁ : f₁ =ᶠ[𝓝 x] f
rwa₂ : 𝕜 → F
rwa₃ :
  Eq.{v + 1} (α := F) (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
    (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
rwa₄ : f₁ =ᶠ[𝓝 x] f
rwa₅ : 𝕜 → F
rwa₆ rwa₇ : f₁ =ᶠ[𝓝 x] f
⊢ Eq.{v + 1} (α := F) (((fderiv 𝕜 f₁ x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)
    (((fderiv 𝕜 f x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1 : F)

Tactic:
rwa [Filter.EventuallyEq.fderiv_eq]

Premises used: Filter.EventuallyEq.fderiv_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
x : 𝕜
s t : Set 𝕜
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
unfold :
  EventuallyEq.{u, v} (β := F) (𝓝[s] x) (fun (x : 𝕜) ↦ ((fderivWithin 𝕜 f₁ t x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1)
    fun (x : 𝕜) ↦ ((fderivWithin 𝕜 f t x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1
⊢ derivWithin f₁ t =ᶠ[𝓝[s] x] derivWithin f t

Tactic:
unfold 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₁ : 𝕜 → F
x : 𝕜
s t : Set 𝕜
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
⊢ EventuallyEq.{u, v} (β := F) (𝓝[s] x) (fun (x : 𝕜) ↦ ((fderivWithin 𝕜 f₁ t x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1)
    fun (x : 𝕜) ↦ ((fderivWithin 𝕜 f t x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1

Tactic:
h.fderivWithin' ht |>.fun_comp (fun a ↦ a 1)

Premises used: Filter.EventuallyEq.fderivWithin', OfNat.ofNat, Filter.EventuallyEq.fun_comp, DFunLike.coe
-- 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
x : 𝕜
s t : Set 𝕜
h : f₁ =ᶠ[𝓝[s] x] f
ht : t ⊆ s
⊢ EventuallyEq.{u, v} (β := F) (𝓝[s] x) (fun (x : 𝕜) ↦ ((fderivWithin 𝕜 f₁ t x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1)
    fun (x : 𝕜) ↦ ((fderivWithin 𝕜 f t x : 𝕜 →L[𝕜] F) : (a : 𝕜) → F) 1

Tactic:
exact h.fderivWithin' ht |>.fun_comp (fun a ↦ a 1)

Premises used: Filter.EventuallyEq.fderivWithin', OfNat.ofNat, Filter.EventuallyEq.fun_comp, DFunLike.coe
-- 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
x : 𝕜
s : Set 𝕜
h : f₁ =ᶠ[𝓝[s] x] f
⊢ derivWithin f₁ s =ᶠ[𝓝[s] x] derivWithin f s

Tactic:
h.derivWithin' Subset.rfl

Premises used: Set.Subset.rfl, Filter.EventuallyEq.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₁ : 𝕜 → F
x : 𝕜
h : f₁ =ᶠ[𝓝 x] f
⊢ deriv f₁ =ᶠ[𝓝 x] deriv f

Tactic:
h.eventuallyEq_nhds.mono fun _ h => h.deriv_eq

Premises used: Filter.EventuallyEq, Filter.EventuallyEq.eventuallyEq_nhds, Filter.Eventually.mono, Filter.EventuallyEq.deriv_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
x : 𝕜
h : f₁ =ᶠ[𝓝[≠] x] f
rw :
  ∀ (h : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ∀ᶠ (x : 𝕜) in 𝓝 y, f₁ x = f x),
    ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ∀ᶠ (x : 𝕜) in 𝓝 y, deriv f₁ x = deriv f x
⊢ deriv f₁ =ᶠ[𝓝[≠] x] deriv f

Tactic:
rw [Filter.EventuallyEq, ← eventually_nhdsNE_eventually_nhds_iff] at *

Premises used: Filter.EventuallyEq, eventually_nhdsNE_eventually_nhds_iff
-- 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
x : 𝕜
h : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ∀ᶠ (x : 𝕜) in 𝓝 y, f₁ x = f x
h₁ : ∀ (y : 𝕜) (hy : ∀ᶠ (x : 𝕜) in 𝓝 y, f₁ x = f x), ∀ᶠ (x : 𝕜) in 𝓝 y, deriv f₁ x = deriv f x
⊢ ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ∀ᶠ (x : 𝕜) in 𝓝 y, deriv f₁ x = deriv f x

Tactic:
filter_upwards [h] with y hy
-- 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
x : 𝕜
h : ∀ᶠ (y : 𝕜) in 𝓝[≠] x, ∀ᶠ (x : 𝕜) in 𝓝 y, f₁ x = f x
y : 𝕜
hy : ∀ᶠ (x : 𝕜) in 𝓝 y, f₁ x = f x
⊢ ∀ᶠ (x : 𝕜) in 𝓝 y, deriv f₁ x = deriv f x

Tactic:
apply Filter.EventuallyEq.deriv hy

Premises used: Filter.EventuallyEq.deriv
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
L : Filter (𝕜 × 𝕜)
⊢ HasDerivAtFilter id 1 L

Tactic:
(hasFDerivAtFilter_id L).hasDerivAtFilter

Premises used: hasFDerivAtFilter_id, HasFDerivAtFilter.hasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
⊢ HasDerivWithinAt id 1 s x

Tactic:
hasDerivAtFilter_id _

Premises used: HasDerivWithinAt, hasDerivAtFilter_id
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
⊢ HasDerivAt id 1 x

Tactic:
hasDerivAtFilter_id _

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

Tactic:
hasDerivAtFilter_id _

Premises used: HasDerivAt, hasDerivAtFilter_id
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
⊢ HasStrictDerivAt id 1 x

Tactic:
hasDerivAtFilter_id _

Premises used: hasDerivAtFilter_id, HasStrictDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
⊢ deriv id x = 1

Tactic:
HasDerivAt.deriv (hasDerivAt_id x)

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

Tactic:
funext deriv_id

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

Tactic:
deriv_id'

Premises used: deriv_id'
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin id s x = 1

Tactic:
(hasDerivWithinAt_id x s).derivWithin hxs

Premises used: HasDerivWithinAt.derivWithin, hasDerivWithinAt_id
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := 𝕜) (derivWithin (fun (x : 𝕜) ↦ x) s x) 1

Tactic:
derivWithin_id x s hxs

Premises used: derivWithin_id
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
L : Filter (𝕜 × 𝕜)
c : F
⊢ HasDerivAtFilter.{u, v} (F := F) (fun (x : 𝕜) ↦ c) 0 L

Tactic:
(hasFDerivAtFilter_const c L).hasDerivAtFilter

Premises used: hasFDerivAtFilter_const, HasFDerivAtFilter.hasDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
L : Filter (𝕜 × 𝕜)
⊢ HasDerivAtFilter.{u, v} (F := F) 0 0 L

Tactic:
hasDerivAtFilter_const _ _

Premises used: hasDerivAtFilter_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
L : Filter (𝕜 × 𝕜)
inst_3 : One F
⊢ HasDerivAtFilter.{u, v} (F := F) 1 0 L

Tactic:
hasDerivAtFilter_const _ _

Premises used: hasDerivAtFilter_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
L : Filter (𝕜 × 𝕜)
inst_3 : NatCast F
n : ℕ
⊢ HasDerivAtFilter.{u, v} (F := F) (↑n : 𝕜 → F) 0 L

Tactic:
hasDerivAtFilter_const _ _

Premises used: hasDerivAtFilter_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
L : Filter (𝕜 × 𝕜)
inst_3 : IntCast F
z : ℤ
⊢ HasDerivAtFilter.{u, v} (F := F) (↑z : 𝕜 → F) 0 L

Tactic:
hasDerivAtFilter_const _ _

Premises used: hasDerivAtFilter_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
L : Filter (𝕜 × 𝕜)
n : ℕ
inst_3 : OfNat F n
⊢ HasDerivAtFilter.{u, v} (F := F) (OfNat.ofNat n) 0 L

Tactic:
hasDerivAtFilter_const _ _

Premises used: hasDerivAtFilter_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
c : F
⊢ HasStrictDerivAt.{u, v} (F := F) (fun (x : 𝕜) ↦ c) 0 x

Tactic:
hasDerivAtFilter_const _ _

Premises used: hasDerivAtFilter_const, HasStrictDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
⊢ HasStrictDerivAt.{u, v} (F := F) 0 0 x

Tactic:
hasStrictDerivAt_const _ _

Premises used: hasStrictDerivAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
inst_3 : One F
⊢ HasStrictDerivAt.{u, v} (F := F) 1 0 x

Tactic:
hasStrictDerivAt_const _ _

Premises used: hasStrictDerivAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
inst_3 : NatCast F
n : ℕ
⊢ HasStrictDerivAt.{u, v} (F := F) (↑n : 𝕜 → F) 0 x

Tactic:
hasStrictDerivAt_const _ _

Premises used: hasStrictDerivAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
inst_3 : IntCast F
z : ℤ
⊢ HasStrictDerivAt.{u, v} (F := F) (↑z : 𝕜 → F) 0 x

Tactic:
hasStrictDerivAt_const _ _

Premises used: hasStrictDerivAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
n : ℕ
inst_3 : OfNat F n
⊢ HasStrictDerivAt.{u, v} (F := F) (OfNat.ofNat n) 0 x

Tactic:
hasStrictDerivAt_const _ _

Premises used: hasStrictDerivAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
c : F
⊢ HasDerivWithinAt.{u, v} (F := F) (fun (x : 𝕜) ↦ c) 0 s x

Tactic:
hasDerivAtFilter_const _ _

Premises used: HasDerivWithinAt, hasDerivAtFilter_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
⊢ HasDerivWithinAt.{u, v} (F := F) 0 0 s x

Tactic:
hasDerivAtFilter_zero _

Premises used: hasDerivAtFilter_zero, HasDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
inst_3 : One F
⊢ HasDerivWithinAt.{u, v} (F := F) 1 0 s x

Tactic:
hasDerivWithinAt_const _ _ _

Premises used: hasDerivWithinAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
inst_3 : NatCast F
n : ℕ
⊢ HasDerivWithinAt.{u, v} (F := F) (↑n : 𝕜 → F) 0 s x

Tactic:
hasDerivWithinAt_const _ _ _

Premises used: hasDerivWithinAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
inst_3 : IntCast F
z : ℤ
⊢ HasDerivWithinAt.{u, v} (F := F) (↑z : 𝕜 → F) 0 s x

Tactic:
hasDerivWithinAt_const _ _ _

Premises used: hasDerivWithinAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
s : Set 𝕜
n : ℕ
inst_3 : OfNat F n
⊢ HasDerivWithinAt.{u, v} (F := F) (OfNat.ofNat n) 0 s x

Tactic:
hasDerivWithinAt_const _ _ _

Premises used: hasDerivWithinAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
c : F
⊢ HasDerivAt.{u, v} (F := F) (fun (x : 𝕜) ↦ c) 0 x

Tactic:
hasDerivAtFilter_const _ _

Premises used: HasDerivAt, hasDerivAtFilter_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
⊢ HasDerivAt.{u, v} (F := F) 0 0 x

Tactic:
hasDerivAtFilter_zero _

Premises used: hasDerivAtFilter_zero, HasDerivAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
inst_3 : One F
⊢ HasDerivAt.{u, v} (F := F) 1 0 x

Tactic:
hasDerivAt_const _ _

Premises used: hasDerivAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
inst_3 : NatCast F
n : ℕ
⊢ HasDerivAt.{u, v} (F := F) (↑n : 𝕜 → F) 0 x

Tactic:
hasDerivAt_const _ _

Premises used: hasDerivAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
inst_3 : IntCast F
z : ℤ
⊢ HasDerivAt.{u, v} (F := F) (↑z : 𝕜 → F) 0 x

Tactic:
hasDerivAt_const _ _

Premises used: hasDerivAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
n : ℕ
inst_3 : OfNat F n
⊢ HasDerivAt.{u, v} (F := F) (OfNat.ofNat n) 0 x

Tactic:
hasDerivAt_const _ _

Premises used: hasDerivAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
x : 𝕜
c : F
⊢ Eq.{v + 1} (α := F) (deriv (fun (x : 𝕜) ↦ c) x) 0

Tactic:
HasDerivAt.deriv (hasDerivAt_const x c)

Premises used: HasDerivAt.deriv, hasDerivAt_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
c : F
⊢ Eq (α := (x : 𝕜) → F) (deriv fun (x : 𝕜) ↦ c) fun (x : 𝕜) ↦ 0

Tactic:
funext fun x => deriv_const x c

Premises used: funext, deriv_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
⊢ Eq (α := (x : 𝕜) → F) (deriv 0) 0

Tactic:
funext fun _ => deriv_const _ _

Premises used: Zero.zero, funext, deriv_const, NegZeroClass.toZero
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : One F
⊢ Eq (α := (x : 𝕜) → F) (deriv 1) 0

Tactic:
funext fun _ => deriv_const _ _

Premises used: One.one, funext, deriv_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NatCast F
n : ℕ
⊢ Eq (α := (x : 𝕜) → F) (deriv (↑n : 𝕜 → F)) 0

Tactic:
funext fun _ => deriv_const _ _

Premises used: NatCast.natCast, funext, deriv_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : IntCast F
z : ℤ
⊢ Eq (α := (x : 𝕜) → F) (deriv (↑z : 𝕜 → F)) 0

Tactic:
funext fun _ => deriv_const _ _

Premises used: IntCast.intCast, funext, deriv_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
n : ℕ
inst_3 : OfNat F n
⊢ Eq (α := (x : 𝕜) → F) (deriv (OfNat.ofNat n)) 0

Tactic:
funext fun _ => deriv_const _ _

Premises used: funext, deriv_const, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
c : F
h : ∀ (x : 𝕜), Eq.{v + 1} (α := F) (derivWithin (fun (x : 𝕜) ↦ c) s x) (0 x)
⊢ Eq (α := (x : 𝕜) → F) (derivWithin (fun (x : 𝕜) ↦ c) s) 0

Tactic:
ext
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
c : F
x : 𝕜
⊢ Eq.{v + 1} (α := F) (derivWithin (fun (x : 𝕜) ↦ c) s x) (0 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
s : Set 𝕜
c : F
⊢ derivWithin (Function.const 𝕜 c) s = 0

Tactic:
derivWithin_fun_const _ _

Premises used: derivWithin_fun_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
⊢ Eq (α := (x : 𝕜) → F) (derivWithin 0 s) 0

Tactic:
derivWithin_const _ _

Premises used: derivWithin_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
inst_3 : One F
⊢ Eq (α := (x : 𝕜) → F) (derivWithin 1 s) 0

Tactic:
derivWithin_const _ _

Premises used: derivWithin_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
inst_3 : NatCast F
n : ℕ
⊢ Eq (α := (x : 𝕜) → F) (derivWithin (↑n : 𝕜 → F) s) 0

Tactic:
derivWithin_const _ _

Premises used: derivWithin_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
inst_3 : IntCast F
z : ℤ
⊢ Eq (α := (x : 𝕜) → F) (derivWithin (↑z : 𝕜 → F) s) 0

Tactic:
derivWithin_const _ _

Premises used: derivWithin_const
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
n : ℕ
inst_3 : OfNat F n
⊢ Eq (α := (x : 𝕜) → F) (derivWithin (OfNat.ofNat n) s) 0

Tactic:
derivWithin_const _ _

Premises used: derivWithin_const
-- 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 𝕜
hL : L ≤ 𝓝 x
h : HasDerivAtFilter f f' (SProd.sprod (β := Filter 𝕜) L (pure x))
⊢ Tendsto f L (𝓝 (f x))

Tactic:
h.hasFDerivAtFilter.tendsto_nhds hL

Premises used: HasFDerivAtFilter.tendsto_nhds, HasDerivAtFilter.hasFDerivAtFilter
-- 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
⊢ ContinuousWithinAt f s x

Tactic:
HasDerivAtFilter.tendsto_nhds inf_le_left h

Premises used: ContinuousWithinAt, HasDerivAtFilter.tendsto_nhds, inf_le_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 : 𝕜
h : HasDerivAt f f' x
⊢ ContinuousAt f x

Tactic:
HasDerivAtFilter.tendsto_nhds le_rfl h

Premises used: le_rfl, ContinuousAt, HasDerivAtFilter.tendsto_nhds
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
f f' : 𝕜 → F
h : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
⊢ ContinuousOn f s

Tactic:
fun x hx => (h x hx).continuousWithinAt

Premises used: ContinuousOn, HasDerivWithinAt.continuousWithinAt
-- Module: Mathlib.Analysis.Calculus.Deriv.Basic
Goal:
𝕜 : Type u
inst : NontriviallyNormedField 𝕜
F : Type v
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
s : Set 𝕜
f f' : 𝕜 → F
hderiv : ∀ x ∈ s, HasDerivAt f (f' x) x
⊢ ContinuousOn f s

Tactic:
fun x hx => (hderiv x hx).continuousAt.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, HasDerivAt.continuousAt, ContinuousOn
-- 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₀ : 𝕜
hf : HasDerivAt f f' x₀
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : 𝕜) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
⊢ ‖f'‖ ≤ C

Tactic:
simpa using HasFDerivAt.le_of_lip' hf.hasFDerivAt hC₀ hlip

Premises used: HasDerivAt.hasFDerivAt, HasFDerivAt.le_of_lip'
-- 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₀ : 𝕜
hf : HasDerivAt f f' x₀
s : Set 𝕜
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ‖f'‖ ≤ (↑C : ℝ)

Tactic:
simpa using HasFDerivAt.le_of_lipschitzOn hf.hasFDerivAt hs hlip

Premises used: HasFDerivAt.le_of_lipschitzOn, HasDerivAt.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
f' : F
x₀ : 𝕜
hf : HasDerivAt f f' x₀
C : ℝ≥0
hlip : LipschitzWith C f
⊢ ‖f'‖ ≤ (↑C : ℝ)

Tactic:
simpa using HasFDerivAt.le_of_lipschitz hf.hasFDerivAt hlip

Premises used: HasDerivAt.hasFDerivAt, HasFDerivAt.le_of_lipschitz
-- 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₀ : 𝕜
C : ℝ
hC₀ : 0 ≤ C
hlip : ∀ᶠ (x : 𝕜) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖
⊢ ‖deriv f x₀‖ ≤ C

Tactic:
simpa [norm_deriv_eq_norm_fderiv] using norm_fderiv_le_of_lip' 𝕜 hC₀ hlip

Premises used: norm_deriv_eq_norm_fderiv, norm_fderiv_le_of_lip'
-- 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 𝕜
hs : s ∈ 𝓝 x₀
C : ℝ≥0
hlip : LipschitzOnWith C f s
⊢ ‖deriv f x₀‖ ≤ (↑C : ℝ)

Tactic:
simpa [norm_deriv_eq_norm_fderiv] using norm_fderiv_le_of_lipschitzOn 𝕜 hs hlip

Premises used: norm_deriv_eq_norm_fderiv, norm_fderiv_le_of_lipschitzOn
-- 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₀ : 𝕜
C : ℝ≥0
hlip : LipschitzWith C f
⊢ ‖deriv f x₀‖ ≤ (↑C : ℝ)

Tactic:
simpa [norm_deriv_eq_norm_fderiv] using norm_fderiv_le_of_lipschitz 𝕜 hlip

Premises used: norm_fderiv_le_of_lipschitz, norm_deriv_eq_norm_fderiv
-- 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 : RingHomIsometric σ
inst_4 : RingHomInvPair σ σ'
F' : Type u_1
inst_5 : NormedAddCommGroup F'
inst_6 : NormedSpace 𝕜 F'
L : F →SL[σ] F'
hf : HasDerivAt f f' x
⊢ RingHomIsometric σ'

Tactic:
have : RingHomIsometric σ' := .inv σ