awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' f₁' : E →L[𝕜] F
x : E
s : Set E
inst_11 : T2Space F
H : UniqueDiffWithinAt 𝕜 s x
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt f f₁' s x
⊢ f' = f₁'

Tactic:
ContinuousLinearMap.ext_on H.1 (hf.unique_on hg)

Premises used: UniqueDiffWithinAt.dense_tangentConeAt, HasFDerivWithinAt.unique_on, ContinuousLinearMap.ext_on
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' f₁' : E →L[𝕜] F
x : E
s : Set E
inst_11 : T2Space F
H : UniqueDiffOn 𝕜 s
hx : x ∈ s
h : HasFDerivWithinAt f f' s x
h₁ : HasFDerivWithinAt f f₁' s x
⊢ f' = f₁'

Tactic:
(H x hx).eq h h₁

Premises used: UniqueDiffWithinAt.eq
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' f₁' : E →L[𝕜] F
x : E
inst_11 : T2Space F
h₀ : HasFDerivAt f f' x
h₁ : HasFDerivAt f f₁' x
⊢ HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) (𝓝[univ] x) (pure x))

Tactic:
rw [HasFDerivAt, ← nhdsWithin_univ] at *

Premises used: HasFDerivAt, nhdsWithin_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' f₁' : E →L[𝕜] F
x : E
inst_11 : T2Space F
h₀ : HasFDerivAt f f' x
h₁ : HasFDerivAt f f₁' x
h₂ : HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) (𝓝[univ] x) (pure x))
⊢ HasFDerivAtFilter f f₁' (SProd.sprod (β := Filter E) (𝓝[univ] x) (pure x))

Tactic:
rw [HasFDerivAt, ← nhdsWithin_univ] at *

Premises used: HasFDerivAt, nhdsWithin_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' f₁' : E →L[𝕜] F
x : E
inst_11 : T2Space F
h₀ : HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) (𝓝[univ] x) (pure x))
h₁ : HasFDerivAtFilter f f₁' (SProd.sprod (β := Filter E) (𝓝[univ] x) (pure x))
⊢ f' = f₁'

Tactic:
uniqueDiffWithinAt_univ.eq h₀ h₁

Premises used: uniqueDiffWithinAt_univ, UniqueDiffWithinAt.eq
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' f₁' : E →L[𝕜] F
x : E
inst_11 : T2Space F
h₀ : HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) (𝓝[univ] x) (pure x))
h₁ : HasFDerivAtFilter f f₁' (SProd.sprod (β := Filter E) (𝓝[univ] x) (pure x))
⊢ f' = f₁'

Tactic:
exact uniqueDiffWithinAt_univ.eq h₀ h₁

Premises used: uniqueDiffWithinAt_univ, UniqueDiffWithinAt.eq
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
L₁ L₂ : Filter (E × E)
h : HasFDerivAtFilter f f' L₂
hst : L₁ ≤ L₂
⊢ HasFDerivAtFilter f f' L₁

Tactic:
.of_isLittleOTVS <| h.isLittleOTVS.mono hst

Premises used: HasFDerivAtFilter.of_isLittleOTVS, HasFDerivAtFilter.isLittleOTVS, Asymptotics.IsLittleOTVS.mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s t : Set E
h : HasFDerivWithinAt f f' t x
hst : t ∈ 𝓝[s] x
⊢ HasFDerivWithinAt f f' s x

Tactic:
h.mono <| prod_mono_left _ (nhdsWithin_le_iff.mpr hst)

Premises used: Iff.mpr, HasFDerivAtFilter.mono, HasFDerivWithinAt, nhdsWithin_le_iff, Filter.prod_mono_left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s t : Set E
h : HasFDerivWithinAt f f' t x
hst : s ⊆ t
⊢ SProd.sprod (β := Filter E) (𝓝[s] x) (pure x) ≤ SProd.sprod (β := Filter E) (𝓝[t] x) (pure x)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
L : Filter (E × E)
h : HasFDerivAt f f' x
hL : L ≤ SProd.sprod (β := Filter E) (𝓝 x) (pure x)
⊢ HasFDerivAtFilter f f' L

Tactic:
h.mono hL

Premises used: HasFDerivAtFilter.mono
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivAt f f' x
⊢ HasFDerivWithinAt f f' s x

Tactic:
h.hasFDerivAtFilter <| prod_mono_left _ nhdsWithin_le_nhds

Premises used: HasFDerivAt.hasFDerivAtFilter, HasFDerivWithinAt, nhdsWithin_le_nhds, Filter.prod_mono_left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
⟨f', h⟩

Premises used: Exists.intro, DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
h : HasFDerivAt f f' x
⊢ DifferentiableAt 𝕜 f x

Tactic:
⟨f', h⟩

Premises used: DifferentiableAt, Exists.intro
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
⊢ HasFDerivWithinAt f f' univ x ↔ HasFDerivAt f f' x

Tactic:
simp only [HasFDerivWithinAt, nhdsWithin_univ, HasFDerivAt]

Premises used: HasFDerivAt, nhdsWithin_univ, HasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
⊢ DifferentiableWithinAt 𝕜 f univ x ↔ DifferentiableAt 𝕜 f x

Tactic:
simp only [DifferentiableWithinAt, hasFDerivWithinAt_univ, DifferentiableAt]

Premises used: DifferentiableAt, DifferentiableWithinAt, hasFDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
h : ¬DifferentiableAt 𝕜 f x
rw : ¬DifferentiableWithinAt 𝕜 f univ x
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 f x) 0

Tactic:
rw [fderiv, fderivWithin_zero_of_not_differentiableWithinAt]

Premises used: fderiv, fderivWithin_zero_of_not_differentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
h rwa rwa₁ rwa₂ rwa₃ : ¬DifferentiableAt 𝕜 f x
⊢ ¬DifferentiableWithinAt 𝕜 f univ x

Tactic:
rwa [differentiableWithinAt_univ]

Premises used: differentiableWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : s ∈ 𝓝 x
rw : HasFDerivWithinAt f f' s x ↔ HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) (𝓝 x) (pure x))
rw₁ :
  HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) (𝓝[s] x) (pure x)) ↔
    HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) (𝓝 x) (pure x))
rw₂ rw₃ :
  HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) (𝓝 x) (pure x)) ↔
    HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) (𝓝 x) (pure x))
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivAt f f' x

Tactic:
rw [HasFDerivAt, HasFDerivWithinAt, nhdsWithin_eq_nhds.mpr h]

Premises used: Iff.mpr, HasFDerivAt, HasFDerivWithinAt, nhdsWithin_eq_nhds
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : IsOpen[inst_3] s
hx : x ∈ s
⊢ HasFDerivWithinAt f f' s x ↔ HasFDerivAt f f' x

Tactic:
hasFDerivWithinAt_of_mem_nhds (h.mem_nhds hx)

Premises used: hasFDerivWithinAt_of_mem_nhds, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
simp_rw :
  (IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝[insert x s] x)
      (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) fun (x' : E) ↦ x' - x) ↔
    IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝[s] x)
      (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) fun (x' : E) ↦ x' - x
⊢ HasFDerivWithinAt f f' (insert x s) x ↔ HasFDerivWithinAt f f' s x

Tactic:
simp_rw [hasFDerivWithinAt_iff_isLittleOTVS]

Premises used: hasFDerivWithinAt_iff_isLittleOTVS
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HSub.hSub (β := F) (f x - f x) ((f' : (a : E) → F) (x - x) : F) = 0
⊢ (IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝[insert x s] x)
      (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) fun (x' : E) ↦ x' - x) ↔
    IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝[s] x)
      (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) fun (x' : E) ↦ x' - x

Tactic:
apply isLittleOTVS_insert

Premises used: Asymptotics.isLittleOTVS_insert
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
⊢ HSub.hSub (β := F) (f x - f x) ((f' : (a : E) → F) (x - x) : F) = 0

Tactic:
simp only [sub_self, map_zero]

Premises used: sub_self, map_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
y : E
h : HasFDerivWithinAt f f' (insert y s) x
⊢ HasFDerivWithinAt f f' s x

Tactic:
h.mono <| subset_insert y s

Premises used: HasFDerivWithinAt.mono, Set.subset_insert
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : T1Space E
y : E
inl : HasFDerivWithinAt f f' (insert x s) x ↔ HasFDerivWithinAt f f' s x
inr : ∀ (h : x ≠ y), HasFDerivWithinAt f f' (insert y s) x ↔ HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt f f' (insert y s) x ↔ HasFDerivWithinAt f f' s x

Tactic:
rcases eq_or_ne x y with (rfl | h)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : T1Space E
⊢ HasFDerivWithinAt f f' (insert x s) x ↔ HasFDerivWithinAt f f' s x

Tactic:
apply hasFDerivWithinAt_insert_self

Premises used: hasFDerivWithinAt_insert_self
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : T1Space E
y : E
h : x ≠ y
⊢ HasFDerivWithinAt f f' (insert y s) x ↔ HasFDerivWithinAt f f' s x

Tactic:
⟨.of_insert, fun hf => hf.mono_of_mem_nhdsWithin ?_⟩

Premises used: HasFDerivWithinAt.mono_of_mem_nhdsWithin, Iff.intro, HasFDerivWithinAt.of_insert
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : T1Space E
y : E
h : x ≠ y
inr : ∀ (hf : HasFDerivWithinAt f f' s x), s ∈ 𝓝[insert y s] x
⊢ HasFDerivWithinAt f f' (insert y s) x ↔ HasFDerivWithinAt f f' s x

Tactic:
refine ⟨.of_insert, fun hf => hf.mono_of_mem_nhdsWithin ?_⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : T1Space E
y : E
h : x ≠ y
hf : HasFDerivWithinAt f f' s x
inr : s ∈ 𝓝[s] x
⊢ s ∈ 𝓝[insert y s] x

Tactic:
simp_rw [nhdsWithin_insert_of_ne h, self_mem_nhdsWithin]

Premises used: self_mem_nhdsWithin, nhdsWithin_insert_of_ne
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
rw : HasFDerivWithinAt f f' (insert x (s \ {x})) x ↔ HasFDerivWithinAt f f' s x
rw₁ : HasFDerivWithinAt f f' (insert x s) x ↔ HasFDerivWithinAt f f' s x
rw₂ rw₃ : HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt f f' (s \ {x}) x ↔ HasFDerivWithinAt f f' s x

Tactic:
rw [← hasFDerivWithinAt_insert_self, insert_diff_singleton, hasFDerivWithinAt_insert_self]

Premises used: hasFDerivWithinAt_insert_self, Set.insert_diff_singleton
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : T1Space E
y : E
rw : HasFDerivWithinAt f f' (insert y (s \ {y})) x ↔ HasFDerivWithinAt f f' s x
rw₁ : E
rw₂ : HasFDerivWithinAt f f' (insert y s) x ↔ HasFDerivWithinAt f f' s x
rw₃ rw₄ : HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' s x
⊢ HasFDerivWithinAt f f' (s \ {y}) x ↔ HasFDerivWithinAt f f' s x

Tactic:
rw [← hasFDerivWithinAt_insert, insert_diff_singleton, hasFDerivWithinAt_insert]

Premises used: Set.insert_diff_singleton, hasFDerivWithinAt_insert
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
⊢ HasFDerivWithinAt f f' ∅ x

Tactic:
simp [HasFDerivWithinAt, hasFDerivAtFilter_iff_isLittleOTVS]

Premises used: HasFDerivWithinAt, hasFDerivAtFilter_iff_isLittleOTVS
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
⊢ DifferentiableWithinAt 𝕜 f ∅ x

Tactic:
⟨0, .empty⟩

Premises used: HasFDerivWithinAt.empty, Exists.intro, DifferentiableWithinAt, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
⊢ DifferentiableOn 𝕜 f ∅

Tactic:
fun _ => False.elim

Premises used: Set.Mem, False.elim, DifferentiableOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : T1Space E
⊢ HasFDerivWithinAt f f' ∅ x

Tactic:
.empty

Premises used: HasFDerivWithinAt.empty
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : T1Space E
⊢ HasFDerivWithinAt f f' ∅ x

Tactic:
exact .empty
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : T1Space E
a : E
s_1 : Set E
h : a ∉ s_1
hs : s_1.Finite
ih : HasFDerivWithinAt f f' s_1 x
⊢ HasFDerivWithinAt f f' (insert a s_1) x

Tactic:
ih.insert'

Premises used: HasFDerivWithinAt.insert'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : T1Space E
a : E
s_1 : Set E
h : a ∉ s_1
hs : s_1.Finite
ih : HasFDerivWithinAt f f' s_1 x
⊢ HasFDerivWithinAt f f' (insert a s_1) x

Tactic:
exact ih.insert'

Premises used: HasFDerivWithinAt.insert'
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : T1Space E
h : s.Finite
empty : HasFDerivWithinAt f f' ∅ x
insert :
  ∀ {a : E} {s : Set E},
    a ∉ s → s.Finite → ∀ (ih : HasFDerivWithinAt f f' s x), HasFDerivWithinAt f f' (Insert.insert a s) x
⊢ HasFDerivWithinAt f f' s x

Tactic:
induction s, h using Set.Finite.induction_on with
  | empty => exact .empty
  | insert _ _ ih => exact ih.insert'

Premises used: Insert.insert
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s : Set E
inst_7 : T1Space E
h : s.Finite
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
⟨0, .of_finite h⟩

Premises used: HasFDerivWithinAt.of_finite, Exists.intro, DifferentiableWithinAt, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
inst_7 : T1Space E
y : E
⊢ HasFDerivWithinAt f f' {x} y

Tactic:
.of_finite <| finite_singleton _

Premises used: HasFDerivWithinAt.of_finite, Set.finite_singleton
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
inst_7 : T1Space E
y : E
⊢ DifferentiableWithinAt 𝕜 f {x} y

Tactic:
⟨0, .singleton⟩

Premises used: HasFDerivWithinAt.singleton, Exists.intro, DifferentiableWithinAt, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
inst_7 : T1Space E
h : s.Subsingleton
⊢ HasFDerivWithinAt f f' s x

Tactic:
.of_finite h.finite

Premises used: HasFDerivWithinAt.of_finite, Set.Subsingleton.finite
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s : Set E
inst_7 : T1Space E
h : s.Subsingleton
⊢ DifferentiableWithinAt 𝕜 f s x

Tactic:
.of_finite h.finite

Premises used: DifferentiableWithinAt.of_finite, Set.Subsingleton.finite