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
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
s t : Set E
hf : DifferentiableOn 𝕜 f s
hf' : DifferentiableOn 𝕜 f t
hs : IsOpen[inst_3] s
ht : IsOpen[inst_3] t
x : E
hx : x ∈ s
⊢ DifferentiableWithinAt 𝕜 f (s ∪ t) x

Tactic:
exact (hf x hx).differentiableAt (hs.mem_nhds hx) |>.differentiableWithinAt

Premises used: DifferentiableWithinAt.differentiableAt, DifferentiableAt.differentiableWithinAt, 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
s t : Set E
hf : DifferentiableOn 𝕜 f s
hf' : DifferentiableOn 𝕜 f t
hs : IsOpen[inst_3] s
ht : IsOpen[inst_3] t
x : E
hx : x ∈ t
⊢ DifferentiableWithinAt 𝕜 f (s ∪ t) x

Tactic:
(hf' x hx).differentiableAt (ht.mem_nhds hx) |>.differentiableWithinAt

Premises used: DifferentiableWithinAt.differentiableAt, DifferentiableAt.differentiableWithinAt, 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
s t : Set E
hf : DifferentiableOn 𝕜 f s
hf' : DifferentiableOn 𝕜 f t
hs : IsOpen[inst_3] s
ht : IsOpen[inst_3] t
x : E
hx : x ∈ t
⊢ DifferentiableWithinAt 𝕜 f (s ∪ t) x

Tactic:
exact (hf' x hx).differentiableAt (ht.mem_nhds hx) |>.differentiableWithinAt

Premises used: DifferentiableWithinAt.differentiableAt, DifferentiableAt.differentiableWithinAt, 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
s t : Set E
hs : IsOpen[inst_3] s
ht : IsOpen[inst_3] t
⊢ DifferentiableOn 𝕜 f (s ∪ t) ↔ DifferentiableOn 𝕜 f s ∧ DifferentiableOn 𝕜 f t

Tactic:
⟨fun h ↦ ⟨h.mono subset_union_left, h.mono subset_union_right⟩,
    fun ⟨hfs, hft⟩ ↦ DifferentiableOn.union_of_isOpen hfs hft hs ht⟩

Premises used: Set.subset_union_right, _private.0.differentiableOn_union_iff_of_isOpen.match_1, Set.subset_union_left, And.intro, DifferentiableOn, Iff.intro, DifferentiableOn.mono, Union.union, DifferentiableOn.union_of_isOpen
-- 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
s t : Set E
hf : DifferentiableOn 𝕜 f s
hf' : DifferentiableOn 𝕜 f t
hst : s ∪ t = univ
hs : IsOpen[inst_3] s
ht : IsOpen[inst_3] t
rw : DifferentiableOn 𝕜 f (s ∪ t)
⊢ Differentiable 𝕜 f

Tactic:
rw [← differentiableOn_univ, ← hst]

Premises used: differentiableOn_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
s t : Set E
hf : DifferentiableOn 𝕜 f s
hf' : DifferentiableOn 𝕜 f t
hst : s ∪ t = univ
hs : IsOpen[inst_3] s
ht : IsOpen[inst_3] t
⊢ DifferentiableOn 𝕜 f (s ∪ t)

Tactic:
hf.union_of_isOpen hf' hs ht

Premises used: DifferentiableOn.union_of_isOpen
-- 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
s t : Set E
hf : DifferentiableOn 𝕜 f s
hf' : DifferentiableOn 𝕜 f t
hst : s ∪ t = univ
hs : IsOpen[inst_3] s
ht : IsOpen[inst_3] t
⊢ DifferentiableOn 𝕜 f (s ∪ t)

Tactic:
exact hf.union_of_isOpen hf' hs ht

Premises used: DifferentiableOn.union_of_isOpen
-- 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
ι : Type u_4
s : ι → Set E
hf : ∀ (i : ι), DifferentiableOn 𝕜 f (s i)
hs : ∀ (i : ι), IsOpen[inst_3] (s i)
x : E
i : ι
hxsi : Membership.mem (γ := Set E) ((fun (i : ι) ↦ s i) i) x
⊢ DifferentiableWithinAt 𝕜 f (⋃ (i : ι), s i) x

Tactic:
(hf i).differentiableAt ((hs i).mem_nhds hxsi) |>.differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, DifferentiableOn.differentiableAt, 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
ι : Type u_4
s : ι → Set E
hf : ∀ (i : ι), DifferentiableOn 𝕜 f (s i)
hs : ∀ (i : ι), IsOpen[inst_3] (s i)
x : E
i : ι
hxsi : Membership.mem (γ := Set E) ((fun (i : ι) ↦ s i) i) x
⊢ DifferentiableWithinAt 𝕜 f (⋃ (i : ι), s i) x

Tactic:
exact (hf i).differentiableAt ((hs i).mem_nhds hxsi) |>.differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, DifferentiableOn.differentiableAt, 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
ι : Type u_4
s : ι → Set E
hs : ∀ (i : ι), IsOpen[inst_3] (s i)
⊢ DifferentiableOn 𝕜 f (⋃ (i : ι), s i) ↔ ∀ (i : ι), DifferentiableOn 𝕜 f (s i)

Tactic:
⟨fun h i ↦ h.mono <| subset_iUnion_of_subset i fun _ a ↦ a,
   fun h ↦ DifferentiableOn.iUnion_of_isOpen h hs⟩

Premises used: Set.subset_iUnion_of_subset, DifferentiableOn.iUnion_of_isOpen, Iff.intro, DifferentiableOn.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
ι : Type u_4
s : ι → Set E
hf : ∀ (i : ι), DifferentiableOn 𝕜 f (s i)
hs : ∀ (i : ι), IsOpen[inst_3] (s i)
hs' : Eq.{u_2 + 1} (α := Set E) (⋃ (i : ι), s i) univ
rw : DifferentiableOn 𝕜 f (⋃ (i : ι), s i)
⊢ Differentiable 𝕜 f

Tactic:
rw [← differentiableOn_univ, ← hs']

Premises used: differentiableOn_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
ι : Type u_4
s : ι → Set E
hf : ∀ (i : ι), DifferentiableOn 𝕜 f (s i)
hs : ∀ (i : ι), IsOpen[inst_3] (s i)
hs' : Eq.{u_2 + 1} (α := Set E) (⋃ (i : ι), s i) univ
⊢ DifferentiableOn 𝕜 f (⋃ (i : ι), s i)

Tactic:
DifferentiableOn.iUnion_of_isOpen hf hs

Premises used: DifferentiableOn.iUnion_of_isOpen
-- 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
ι : Type u_4
s : ι → Set E
hf : ∀ (i : ι), DifferentiableOn 𝕜 f (s i)
hs : ∀ (i : ι), IsOpen[inst_3] (s i)
hs' : Eq.{u_2 + 1} (α := Set E) (⋃ (i : ι), s i) univ
⊢ DifferentiableOn 𝕜 f (⋃ (i : ι), s i)

Tactic:
exact DifferentiableOn.iUnion_of_isOpen hf hs

Premises used: DifferentiableOn.iUnion_of_isOpen
-- 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 : Filter (E × E)
inst_7 : ContinuousAdd F
inst_8 : ContinuousSMul 𝕜 F
hf : HasFDerivAtFilter f f' L
⊢ IsBigOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) L (fun (p : E × E) ↦ f p.1 - f p.2) fun (p : E × E) ↦ p.1 - p.2

Tactic:
simpa using hf.isLittleOTVS.isBigOTVS.fun_add f'.isBigOTVS_comp

Premises used: Asymptotics.IsBigOTVS.fun_add, ContinuousLinearMap.isBigOTVS_comp, Asymptotics.IsLittleOTVS.isBigOTVS, HasFDerivAtFilter.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
inst_7 : ContinuousAdd F
inst_8 : ContinuousSMul 𝕜 F
hf : HasStrictFDerivAt f f' x
⊢ IsBigOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝 (x, x)) (fun (p : E × E) ↦ f p.1 - f p.2) fun (p : E × E) ↦
    p.1 - p.2

Tactic:
HasFDerivAtFilter.isBigOTVS_sub hf

Premises used: HasFDerivAtFilter.isBigOTVS_sub
-- 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 : ContinuousAdd F
inst_8 : ContinuousSMul 𝕜 F
h : HasFDerivWithinAt f f' s x
⊢ IsBigOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝[s] x) (fun (x_1 : E) ↦ f x_1 - f x) fun (x_1 : E) ↦ x_1 - x

Tactic:
simpa using HasFDerivAtFilter.isBigOTVS_sub h

Premises used: HasFDerivAtFilter.isBigOTVS_sub
-- 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 : ContinuousAdd F
inst_8 : ContinuousSMul 𝕜 F
h : DifferentiableWithinAt 𝕜 f s x
⊢ IsBigOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝[s] x) (fun (x_1 : E) ↦ f x_1 - f x) fun (x_1 : E) ↦ x_1 - x

Tactic:
h.hasFDerivWithinAt.isBigOTVS_sub

Premises used: HasFDerivWithinAt.isBigOTVS_sub, DifferentiableWithinAt.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
f' : E →L[𝕜] F
x : E
inst_7 : ContinuousAdd F
inst_8 : ContinuousSMul 𝕜 F
h : HasFDerivAt f f' x
⊢ IsBigOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝 x) (fun (x_1 : E) ↦ f x_1 - f x) fun (x_1 : E) ↦ x_1 - x

Tactic:
simpa using HasFDerivAtFilter.isBigOTVS_sub h

Premises used: HasFDerivAtFilter.isBigOTVS_sub
-- 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 : ContinuousAdd F
inst_8 : ContinuousSMul 𝕜 F
h : DifferentiableAt 𝕜 f x
⊢ IsBigOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝 x) (fun (x_1 : E) ↦ f x_1 - f x) fun (x_1 : E) ↦ x_1 - x

Tactic:
h.hasFDerivAt.isBigOTVS_sub

Premises used: HasFDerivAt.isBigOTVS_sub, DifferentiableAt.hasFDerivAt
-- 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 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
L : Filter E
hL : L ≤ 𝓝 x
h : HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) L (pure x))
⊢ IsLittleOTVS.{u_1, u_2, u_3, u_1} 𝕜 (E := F) (F := 𝕜) L (fun (x_1 : E) ↦ f x_1 - f x) 1

Tactic:
h.isBigOTVS_sub |>.comp_tendsto prod_pure.ge |>.trans_isLittleOTVS ?_

Premises used: Eq.ge, Asymptotics.IsBigOTVS.comp_tendsto, HasFDerivAtFilter.isBigOTVS_sub, Asymptotics.IsBigOTVS.trans_isLittleOTVS, Filter.prod_pure
-- 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 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
L : Filter E
hL : L ≤ 𝓝 x
h : HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) L (pure x))
refine : IsLittleOTVS 𝕜 (E := E) (F := 𝕜) L ((fun (p : E × E) ↦ p.1 - p.2) ∘ fun (a : E) ↦ (a, x)) 1
⊢ IsLittleOTVS.{u_1, u_2, u_3, u_1} 𝕜 (E := F) (F := 𝕜) L (fun (x_1 : E) ↦ f x_1 - f x) 1

Tactic:
refine h.isBigOTVS_sub |>.comp_tendsto prod_pure.ge |>.trans_isLittleOTVS ?_

Premises used: Eq.ge, Asymptotics.IsBigOTVS.comp_tendsto, HasFDerivAtFilter.isBigOTVS_sub, Asymptotics.IsBigOTVS.trans_isLittleOTVS, Filter.prod_pure
-- 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 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
L : Filter E
hL : L ≤ 𝓝 x
h : HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) L (pure x))
rw : Tendsto (β := E) ((fun (p : E × E) ↦ p.1 - p.2) ∘ fun (a : E) ↦ (a, x)) L (𝓝 0)
⊢ IsLittleOTVS 𝕜 (E := E) (F := 𝕜) L ((fun (p : E × E) ↦ p.1 - p.2) ∘ fun (a : E) ↦ (a, x)) 1

Tactic:
rw [isLittleOTVS_one]

Premises used: Asymptotics.isLittleOTVS_one
-- 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 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
L : Filter E
hL : L ≤ 𝓝 x
h : HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) L (pure x))
⊢ Tendsto (β := E) ((fun (p : E × E) ↦ p.1 - p.2) ∘ fun (a : E) ↦ (a, x)) L (𝓝 0)

Tactic:
simpa [sub_eq_add_neg] using (tendsto_id'.mpr hL).add_const (-x)

Premises used: Iff.mpr, sub_eq_add_neg, Filter.tendsto_id', Filter.Tendsto.add_const, Neg.neg
-- 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 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
L : Filter E
hL : L ≤ 𝓝 x
h : HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) L (pure x))
⊢ IsLittleOTVS.{u_1, u_2, u_3, u_1} 𝕜 (E := F) (F := 𝕜) L (fun (x_1 : E) ↦ f x_1 - f x) 1

Tactic:
have : (f · - f x) =o[𝕜; L] (1 : E → 𝕜) := by
    refine h.isBigOTVS_sub |>.comp_tendsto prod_pure.ge |>.trans_isLittleOTVS ?_
    rw [isLittleOTVS_one]
    simpa [sub_eq_add_neg] using (tendsto_id'.mpr hL).add_const (-x)
-- 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 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
L : Filter E
hL : L ≤ 𝓝 x
h : HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) L (pure x))
this : IsLittleOTVS.{u_1, u_2, u_3, u_1} 𝕜 (E := F) (F := 𝕜) L (fun (x_1 : E) ↦ f x_1 - f x) 1
⊢ Tendsto.{u_2, u_3} (β := F) (fun (x_1 : E) ↦ f x_1 - f x) L (𝓝 0)

Tactic:
rw [isLittleOTVS_one] at this

Premises used: Asymptotics.isLittleOTVS_one
-- 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 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
L : Filter E
hL : L ≤ 𝓝 x
h : HasFDerivAtFilter f f' (SProd.sprod (β := Filter E) L (pure x))
this : Tendsto.{u_2, u_3} (β := F) (fun (x_1 : E) ↦ f x_1 - f x) L (𝓝 0)
⊢ Tendsto f L (𝓝 (f x))

Tactic:
simpa using this.add_const (f x)

Premises used: Filter.Tendsto.add_const
-- 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 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
h : HasFDerivWithinAt f f' s x
⊢ ContinuousWithinAt f s x

Tactic:
HasFDerivAtFilter.tendsto_nhds inf_le_left h

Premises used: HasFDerivAtFilter.tendsto_nhds, ContinuousWithinAt, inf_le_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
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
h : HasFDerivAt f f' x
⊢ ContinuousAt f x

Tactic:
HasFDerivAtFilter.tendsto_nhds le_rfl h

Premises used: HasFDerivAtFilter.tendsto_nhds, le_rfl, ContinuousAt
-- 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 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
h : DifferentiableWithinAt 𝕜 f s x
⊢ ContinuousWithinAt f s x

Tactic:
let ⟨_, hf'⟩ := h
  hf'.continuousWithinAt

Premises used: ContinuousWithinAt, _private.0.DifferentiableWithinAt.continuousWithinAt.match_1, HasFDerivWithinAt.continuousWithinAt
-- 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 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
h : DifferentiableAt 𝕜 f x
⊢ ContinuousAt f x

Tactic:
let ⟨_, hf'⟩ := h
  hf'.continuousAt

Premises used: ContinuousAt, _private.0.DifferentiableAt.continuousAt.match_1, HasFDerivAt.continuousAt
-- 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
s : Set E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
h : DifferentiableOn 𝕜 f s
⊢ ContinuousOn f s

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

Premises used: DifferentiableWithinAt.continuousWithinAt, ContinuousOn
-- 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
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
h : Differentiable 𝕜 f
⊢ Continuous[inst_3, inst_6] f

Tactic:
continuous_iff_continuousAt.2 fun x => (h x).continuousAt

Premises used: Iff.mpr, DifferentiableAt.continuousAt, continuous_iff_continuousAt
-- 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 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
hf : HasStrictFDerivAt f f' x
⊢ ContinuousAt f x

Tactic:
hf.hasFDerivAt.continuousAt

Premises used: HasStrictFDerivAt.hasFDerivAt, HasFDerivAt.continuousAt
-- 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
L : Filter (E × E)
⊢ ∀ (x : E × E), 0 x = HSub.hSub (β := E) (id x.1 - id x.2) ((ContinuousLinearMap.id 𝕜 E : (a : E) → E) (x.1 - x.2) : E)

Tactic:
simp
-- 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
x : E
⊢ HasStrictFDerivAt id (ContinuousLinearMap.id 𝕜 E) x

Tactic:
hasFDerivAtFilter_id _

Premises used: HasStrictFDerivAt, hasFDerivAtFilter_id
-- 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
x : E
s : Set E
⊢ HasFDerivWithinAt id (ContinuousLinearMap.id 𝕜 E) s x

Tactic:
hasFDerivAtFilter_id _

Premises used: HasFDerivWithinAt, hasFDerivAtFilter_id
-- 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
x : E
⊢ HasFDerivAt id (ContinuousLinearMap.id 𝕜 E) x

Tactic:
hasFDerivAtFilter_id _

Premises used: HasFDerivAt, hasFDerivAtFilter_id
-- 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
x : E
⊢ DifferentiableAt 𝕜 id x

Tactic:
(hasFDerivAt_id x).differentiableAt

Premises used: hasFDerivAt_id, HasFDerivAt.differentiableAt
-- 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
x : E
s : Set E
⊢ DifferentiableWithinAt 𝕜 id s x

Tactic:
differentiableAt_id.differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, differentiableAt_id
-- 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
⊢ Differentiable.{u_1, u_2, u_2} 𝕜 (E := E) id

Tactic:
fun _ => differentiableAt_id

Premises used: Differentiable, differentiableAt_id
-- 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
s : Set E
⊢ DifferentiableOn 𝕜 id s

Tactic:
differentiable_id.differentiableOn

Premises used: Differentiable.differentiableOn, differentiable_id