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
f' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
⊢ IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝 x)
    (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) fun (x' : E) ↦ x' - x

Tactic:
simpa only using hf.isLittleOTVS.comp_tendsto (tendsto_id.prodMk_nhds tendsto_const_nhds)

Premises used: Filter.tendsto_id, tendsto_const_nhds, Asymptotics.IsLittleOTVS.comp_tendsto, HasFDerivAtFilter.isLittleOTVS, Filter.Tendsto.prodMk_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
hf : HasStrictFDerivAt f f' x
⊢ DifferentiableAt 𝕜 f x

Tactic:
hf.hasFDerivAt.differentiableAt

Premises used: HasStrictFDerivAt.hasFDerivAt, 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
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 : HasFDerivAt f f' x
v : E
α : Type u_4
c : α → 𝕜
l : Filter α
hc : Tendsto (β := ℝ) (fun (n : α) ↦ ‖c n‖) l atTop
⊢ Tendsto.{u_4, u_3} (β := F) (fun (n : α) ↦ c n • (f (x + (c n)⁻¹ • v) - f x)) l (𝓝 ((f' : (a : E) → F) v) : Filter F)

Tactic:
(hasFDerivWithinAt_univ.2 hf).lim ?_ (.of_forall fun _ ↦ mem_univ _) ?_

Premises used: Iff.mpr, HasFDerivWithinAt.lim, Filter.Eventually.of_forall, Inv.inv, HAdd.hAdd, Set.mem_univ, HSMul.hSMul, 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
f' : E →L[𝕜] F
x : E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
hf : HasFDerivAt f f' x
v : E
α : Type u_4
c : α → 𝕜
l : Filter α
hc : Tendsto (β := ℝ) (fun (n : α) ↦ ‖c n‖) l atTop
refine_1 : Tendsto.{u_4, u_2} (β := E) (fun (n : α) ↦ (c n)⁻¹ • v) l (𝓝 0)
refine_2 : Tendsto (fun (n : α) ↦ c n • (c n)⁻¹ • v) l (𝓝 v)
⊢ Tendsto.{u_4, u_3} (β := F) (fun (n : α) ↦ c n • (f (x + (c n)⁻¹ • v) - f x)) l (𝓝 ((f' : (a : E) → F) v) : Filter F)

Tactic:
refine (hasFDerivWithinAt_univ.2 hf).lim ?_ (.of_forall fun _ ↦ mem_univ _) ?_

Premises used: Iff.mpr, HasFDerivWithinAt.lim, Filter.Eventually.of_forall, HAdd.hAdd, Set.mem_univ, 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
f' : E →L[𝕜] F
x : E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
hf : HasFDerivAt f f' x
v : E
α : Type u_4
c : α → 𝕜
l : Filter α
hc : Tendsto (β := ℝ) (fun (n : α) ↦ ‖c n‖) l atTop
⊢ Tendsto c l (Bornology.cobounded 𝕜)

Tactic:
rw [tendsto_norm_atTop_iff_cobounded] at hc

Premises used: tendsto_norm_atTop_iff_cobounded
-- 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 : HasFDerivAt f f' x
v : E
α : Type u_4
c : α → 𝕜
l : Filter α
hc : Tendsto c l (Bornology.cobounded 𝕜)
⊢ Tendsto.{u_4, u_2} (β := E) (fun (n : α) ↦ (c n)⁻¹ • v) l (𝓝 0)

Tactic:
simpa using (tendsto_inv₀_cobounded.comp hc).smul (tendsto_const_nhds (x := v))

Premises used: tendsto_const_nhds, Filter.tendsto_inv₀_cobounded, Filter.Tendsto.smul, Filter.Tendsto.comp
-- 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 : HasFDerivAt f f' x
v : E
α : Type u_4
c : α → 𝕜
l : Filter α
hc : Tendsto (β := ℝ) (fun (n : α) ↦ ‖c n‖) l atTop
⊢ Tendsto (fun (n : α) ↦ c n • (c n)⁻¹ • v) l (𝓝 v)

Tactic:
tendsto_nhds_of_eventually_eq ?_

Premises used: tendsto_nhds_of_eventually_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
x : E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
hf : HasFDerivAt f f' x
v : E
α : Type u_4
c : α → 𝕜
l : Filter α
hc : Tendsto (β := ℝ) (fun (n : α) ↦ ‖c n‖) l atTop
refine_2 : ∀ᶠ (x' : α) in l, c x' • (c x')⁻¹ • v = v
⊢ Tendsto (fun (n : α) ↦ c n • (c n)⁻¹ • v) l (𝓝 v)

Tactic:
refine tendsto_nhds_of_eventually_eq ?_

Premises used: tendsto_nhds_of_eventually_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
x : E
inst_7 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
hf : HasFDerivAt f f' x
v : E
α : Type u_4
c : α → 𝕜
l : Filter α
hc : Tendsto (β := ℝ) (fun (n : α) ↦ ‖c n‖) l atTop
⊢ ∀ᶠ (x' : α) in l, c x' • (c x')⁻¹ • v = v

Tactic:
(eventually_ne_of_tendsto_norm_atTop hc (0 : 𝕜)).mono fun y hy => ?_

Premises used: Filter.Eventually.mono, eventually_ne_of_tendsto_norm_atTop, 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 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
hf : HasFDerivAt f f' x
v : E
α : Type u_4
c : α → 𝕜
l : Filter α
hc : Tendsto (β := ℝ) (fun (n : α) ↦ ‖c n‖) l atTop
refine_2 : ∀ (y : α) (hy : c y ≠ 0), c y • (c y)⁻¹ • v = v
⊢ ∀ᶠ (x' : α) in l, c x' • (c x')⁻¹ • v = v

Tactic:
refine (eventually_ne_of_tendsto_norm_atTop hc (0 : 𝕜)).mono fun y hy => ?_

Premises used: Filter.Eventually.mono, eventually_ne_of_tendsto_norm_atTop, 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 : ContinuousAdd E
inst_8 : ContinuousSMul 𝕜 E
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
hf : HasFDerivAt f f' x
v : E
α : Type u_4
c : α → 𝕜
l : Filter α
hc : Tendsto (β := ℝ) (fun (n : α) ↦ ‖c n‖) l atTop
y : α
hy : c y ≠ 0
⊢ c y • (c y)⁻¹ • v = v

Tactic:
simp [hy]
-- 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 : t ∈ 𝓝[s] x
⊢ HasFDerivWithinAt f f' (s ∩ t) x ↔ HasFDerivWithinAt f f' s x

Tactic:
simp [HasFDerivWithinAt, nhdsWithin_restrict'' s h]

Premises used: nhdsWithin_restrict'', 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
s t : Set E
h : t ∈ 𝓝 x
⊢ HasFDerivWithinAt f f' (s ∩ t) x ↔ HasFDerivWithinAt f f' s x

Tactic:
simp [HasFDerivWithinAt, nhdsWithin_restrict' s h]

Premises used: HasFDerivWithinAt, nhdsWithin_restrict'
-- 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
hs : HasFDerivWithinAt f f' s x
ht : HasFDerivWithinAt f f' t x
simp :
  ∀
    (hs :
      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)
    (ht :
      IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝[t] 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 ⊔ 𝓝[t] 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' (s ∪ t) x

Tactic:
simp only [hasFDerivWithinAt_iff_isLittleOTVS, nhdsWithin_union] at *

Premises used: nhdsWithin_union, 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 t : Set E
hs :
  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
ht :
  IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝[t] 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 ⊔ 𝓝[t] x)
    (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) fun (x' : E) ↦ x' - x

Tactic:
hs.sup ht

Premises used: Asymptotics.IsLittleOTVS.sup
-- 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
hs :
  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
ht :
  IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) (𝓝[t] 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 ⊔ 𝓝[t] x)
    (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) fun (x' : E) ↦ x' - x

Tactic:
exact hs.sup ht

Premises used: Asymptotics.IsLittleOTVS.sup
-- 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
hs : s ∈ 𝓝 x
rwa : ∀ (h : HasFDerivWithinAt f f' (univ ∩ s) x) (hs : s ∈ 𝓝 x), HasFDerivAt f f' x
rwa₁ : ∀ (h : HasFDerivWithinAt f f' univ x) (hs : s ∈ 𝓝 x), HasFDerivAt f f' x
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (h : HasFDerivAt f f' x) (hs : s ∈ 𝓝 x), HasFDerivAt f f' x
⊢ HasFDerivAt f f' x

Tactic:
rwa [← univ_inter s, hasFDerivWithinAt_inter hs, hasFDerivWithinAt_univ] at h

Premises used: Set.univ_inter, hasFDerivWithinAt_inter, 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
s : Set E
h : DifferentiableWithinAt 𝕜 f s x
hs : s ∈ 𝓝 x
⊢ DifferentiableAt 𝕜 f x

Tactic:
h.imp fun _ hf' => hf'.hasFDerivAt hs

Premises used: DifferentiableAt, Exists.imp
-- 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 : ¬AccPt x (𝓟 s)
⊢ 𝓝[s \ {x}] x = ⊥

Tactic:
rw [accPt_principal_iff_nhdsWithin, not_neBot] at h

Premises used: accPt_principal_iff_nhdsWithin, Filter.not_neBot
-- 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}] x = ⊥
rw :
  IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) ⊥
    (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' s x

Tactic:
rw [← hasFDerivWithinAt_diff_singleton_self, hasFDerivWithinAt_iff_isLittleOTVS, h]

Premises used: hasFDerivWithinAt_diff_singleton_self, 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 : 𝓝[s \ {x}] x = ⊥
⊢ IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) ⊥
    (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) fun (x' : E) ↦ x' - x

Tactic:
.bot

Premises used: Asymptotics.IsLittleOTVS.bot
-- 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}] x = ⊥
⊢ IsLittleOTVS.{u_1, u_2, u_3, u_2} 𝕜 (E := F) (F := E) ⊥
    (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) fun (x' : E) ↦ x' - x

Tactic:
exact .bot
-- 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 : x ∉ closure[inst_3] s
⊢ HasFDerivWithinAt f f' s x

Tactic:
.of_not_accPt (h ·.clusterPt.mem_closure)

Premises used: ClusterPt.mem_closure, AccPt.clusterPt, HasFDerivWithinAt.of_not_accPt
-- 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
h : ¬AccPt x (𝓟 s)
rw :
  Eq (α := E →L[𝕜] F)
    (if HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x then 0
    else
      if h : DifferentiableWithinAt 𝕜 f s x then
        Classical.choose (p := fun (x_1 : E →L[𝕜] F) ↦ HasFDerivWithinAt f x_1 s x) h
      else 0)
    0
rw₁ rw₂ : Eq (α := E →L[𝕜] F) 0 0
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) 0

Tactic:
rw [fderivWithin, if_pos (.of_not_accPt h)]

Premises used: if_pos, fderivWithin
-- 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
h : x ∉ closure[inst_3] s
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 f s x) 0

Tactic:
fderivWithin_zero_of_not_accPt (h ·.clusterPt.mem_closure)

Premises used: fderivWithin_zero_of_not_accPt, ClusterPt.mem_closure, AccPt.clusterPt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
F : Type u_3
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
inst_3 : TopologicalSpace F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : ¬UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := 𝕜 →L[𝕜] F) (fderivWithin 𝕜 f s x : 𝕜 →L[𝕜] F) (0 : 𝕜 →L[𝕜] F)

Tactic:
fderivWithin_zero_of_not_accPt <| mt AccPt.uniqueDiffWithinAt h

Premises used: fderivWithin_zero_of_not_accPt, mt, AccPt.uniqueDiffWithinAt
-- 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
h : DifferentiableWithinAt 𝕜 f s x
simp :
  HasFDerivWithinAt f
    (if HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x then 0
    else Classical.choose (p := fun (x_1 : E →L[𝕜] F) ↦ HasFDerivWithinAt f x_1 s x) h)
    s x
⊢ HasFDerivWithinAt f (fderivWithin 𝕜 f s x) s x

Tactic:
simp only [fderivWithin, dif_pos h]

Premises used: dif_pos, fderivWithin
-- 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
h : DifferentiableWithinAt 𝕜 f s x
pos : ∀ (h₀ : HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x), HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x
neg :
  ∀ (h₀ : ¬HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x),
    HasFDerivWithinAt f (Classical.choose (p := fun (x_1 : E →L[𝕜] F) ↦ HasFDerivWithinAt f x_1 s x) h) s x
⊢ HasFDerivWithinAt f
    (if HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x then 0
    else Classical.choose (p := fun (x_1 : E →L[𝕜] F) ↦ HasFDerivWithinAt f x_1 s x) h)
    s x

Tactic:
split_ifs with h₀
-- 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
h : DifferentiableWithinAt 𝕜 f s x
h₀ : HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x

Tactic:
h₀
-- 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
h : DifferentiableWithinAt 𝕜 f s x
h₀ : ¬HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x
⊢ HasFDerivWithinAt f (Classical.choose (p := fun (x_1 : E →L[𝕜] F) ↦ HasFDerivWithinAt f x_1 s x) h) s x

Tactic:
Classical.choose_spec h

Premises used: Classical.choose_spec
-- 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
h : DifferentiableWithinAt 𝕜 f s x
h₀ : HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x

Tactic:
exacts [h₀, Classical.choose_spec h]

Premises used: Classical.choose_spec
-- 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 : HasFDerivWithinAt f (fderivWithin 𝕜 f univ x) univ x
⊢ HasFDerivAt f (fderiv 𝕜 f x) x

Tactic:
rw [fderiv, ← hasFDerivWithinAt_univ]

Premises used: fderiv, 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
⊢ DifferentiableWithinAt 𝕜 f univ x

Tactic:
rw [← differentiableWithinAt_univ] at h

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
x : E
h : DifferentiableWithinAt 𝕜 f univ x
⊢ HasFDerivWithinAt f (fderivWithin 𝕜 f univ x) univ x

Tactic:
h.hasFDerivWithinAt

Premises used: 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
x : E
h : DifferentiableWithinAt 𝕜 f univ x
⊢ HasFDerivWithinAt f (fderivWithin 𝕜 f univ x) univ x

Tactic:
exact h.hasFDerivWithinAt

Premises used: 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
x : E
s : Set E
h : DifferentiableOn 𝕜 f s
hs : s ∈ 𝓝 x
⊢ HasFDerivAt f (fderiv 𝕜 f x) x

Tactic:
((h x (mem_of_mem_nhds hs)).differentiableAt hs).hasFDerivAt

Premises used: DifferentiableWithinAt.differentiableAt, mem_of_mem_nhds, 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
x : E
s : Set E
h : DifferentiableOn 𝕜 f s
hs : s ∈ 𝓝 x
⊢ DifferentiableAt 𝕜 f x

Tactic:
(h.hasFDerivAt hs).differentiableAt

Premises used: DifferentiableOn.hasFDerivAt, 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
F : Type u_3
inst_4 : AddCommGroup F
inst_5 : Module 𝕜 F
inst_6 : TopologicalSpace F
f : E → F
x : E
s : Set E
h : DifferentiableOn 𝕜 f s
hs : s ∈ 𝓝 x
⊢ ∀ᶠ (y : E) in 𝓝 x, DifferentiableAt 𝕜 f y

Tactic:
(eventually_eventually_nhds.2 hs).mono fun _ => h.differentiableAt

Premises used: Iff.mpr, DifferentiableOn.differentiableAt, Filter.Eventually.mono, eventually_eventually_nhds