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
x : E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
inst_6 : T2Space E
⊢ Eq (α := E →L[𝕜] E) (fderiv 𝕜 id x) (ContinuousLinearMap.id 𝕜 E)

Tactic:
HasFDerivAt.fderiv (hasFDerivAt_id x)

Premises used: hasFDerivAt_id, HasFDerivAt.fderiv
-- 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
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
inst_6 : T2Space E
hxs : UniqueDiffWithinAt 𝕜 s x
rw : Eq (α := E →L[𝕜] E) (fderiv 𝕜 id x) (ContinuousLinearMap.id 𝕜 E)
⊢ Eq (α := E →L[𝕜] E) (fderivWithin 𝕜 id s x) (ContinuousLinearMap.id 𝕜 E)

Tactic:
rw [DifferentiableAt.fderivWithin differentiableAt_id hxs]

Premises used: DifferentiableAt.fderivWithin, 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
x : E
s : Set E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
inst_6 : T2Space E
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := E →L[𝕜] E) (fderiv 𝕜 id x) (ContinuousLinearMap.id 𝕜 E)

Tactic:
fderiv_id

Premises used: fderiv_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
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
inst_6 : T2Space E
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := E →L[𝕜] E) (fderiv 𝕜 id x) (ContinuousLinearMap.id 𝕜 E)

Tactic:
exact fderiv_id

Premises used: fderiv_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
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
hf : HasFDerivAtFilter f f' L
hf' : IsInducing.{u_2, u_3} (X := E) (Y := F) (⇑f' : (a : E) → F)
rw :
  IsLittleOTVS 𝕜 (F := F) L
    (HSub.hSub (α := E × E → F) (fun (p : E × E) ↦ f p.1 - f p.2) fun (p : E × E) ↦ (f' : (a : E) → F) (p.1 - p.2))
    fun (p : E × E) ↦ (f' : (a : E) → F) (p.1 - p.2)
⊢ IsEquivalent.{u_2, u_3} (E' := F) L (fun (p : E × E) ↦ f p.1 - f p.2) fun (p : E × E) ↦ (f' : (a : E) → F) (p.1 - p.2)

Tactic:
rw [IsEquivalent, ← isLittleOTVS_iff_isLittleO (𝕜 := 𝕜)]

Premises used: Asymptotics.isLittleOTVS_iff_isLittleO, Asymptotics.IsEquivalent
-- 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 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
hf : HasFDerivAtFilter f f' L
hf' : IsInducing.{u_2, u_3} (X := E) (Y := F) (⇑f' : (a : E) → F)
⊢ IsLittleOTVS 𝕜 (F := F) L
    (HSub.hSub (α := E × E → F) (fun (p : E × E) ↦ f p.1 - f p.2) fun (p : E × E) ↦ (f' : (a : E) → F) (p.1 - p.2))
    fun (p : E × E) ↦ (f' : (a : E) → F) (p.1 - p.2)

Tactic:
hf.isLittleOTVS.trans_isBigOTVS <| f'.isThetaTVS_comp hf' |>.symm.isBigOTVS

Premises used: Asymptotics.IsLittleOTVS.trans_isBigOTVS, Asymptotics.IsThetaTVS.isBigOTVS, Asymptotics.IsThetaTVS.symm, ContinuousLinearMap.isThetaTVS_comp, 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 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
hf : HasFDerivAtFilter f f' L
hf' : IsInducing.{u_2, u_3} (X := E) (Y := F) (⇑f' : (a : E) → F)
⊢ IsLittleOTVS 𝕜 (F := F) L
    (HSub.hSub (α := E × E → F) (fun (p : E × E) ↦ f p.1 - f p.2) fun (p : E × E) ↦ (f' : (a : E) → F) (p.1 - p.2))
    fun (p : E × E) ↦ (f' : (a : E) → F) (p.1 - p.2)

Tactic:
exact hf.isLittleOTVS.trans_isBigOTVS <| f'.isThetaTVS_comp hf' |>.symm.isBigOTVS

Premises used: Asymptotics.IsLittleOTVS.trans_isBigOTVS, Asymptotics.IsThetaTVS.isBigOTVS, Asymptotics.IsThetaTVS.symm, ContinuousLinearMap.isThetaTVS_comp, 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 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
hf : HasFDerivAtFilter f f' L
hf' : IsInducing.{u_2, u_3} (X := E) (Y := F) (⇑f' : (a : E) → F)
⊢ IsThetaTVS.{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:
hf.isEquivalent_sub hf' |>.isTheta.isThetaTVS.trans <| f'.isThetaTVS_comp hf'

Premises used: Asymptotics.IsTheta.isThetaTVS, ContinuousLinearMap.isThetaTVS_comp, Asymptotics.IsThetaTVS.trans, Asymptotics.IsEquivalent.isTheta, HasFDerivAtFilter.isEquivalent_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 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
hf : HasFDerivAt f f' x
hf' : IsInducing.{u_2, u_3} (X := E) (Y := F) (⇑f' : (a : E) → F)
⊢ IsEquivalent.{u_2, u_3} (E' := F) (𝓝 x) (fun (x_1 : E) ↦ f x_1 - f x) fun (x_1 : E) ↦ (f' : (a : E) → F) (x_1 - x)

Tactic:
simpa using HasFDerivAtFilter.isEquivalent_sub hf hf'

Premises used: HasFDerivAtFilter.isEquivalent_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 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
hf : HasFDerivAt f f' x
hf' : IsInducing.{u_2, u_3} (X := E) (Y := F) (⇑f' : (a : E) → F)
⊢ IsThetaTVS.{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 [IsThetaTVS] using HasFDerivAtFilter.isThetaTVS_sub hf hf'

Premises used: HasFDerivAtFilter.isThetaTVS_sub, Asymptotics.IsThetaTVS
-- 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 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
hf : HasFDerivWithinAt f f' s x
hf' : IsInducing.{u_2, u_3} (X := E) (Y := F) (⇑f' : (a : E) → F)
⊢ IsEquivalent.{u_2, u_3} (E' := F) (𝓝[s] x) (fun (x_1 : E) ↦ f x_1 - f x) fun (x_1 : E) ↦ (f' : (a : E) → F) (x_1 - x)

Tactic:
simpa using HasFDerivAtFilter.isEquivalent_sub hf hf'

Premises used: HasFDerivAtFilter.isEquivalent_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 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
hf : HasFDerivWithinAt f f' s x
hf' : IsInducing.{u_2, u_3} (X := E) (Y := F) (⇑f' : (a : E) → F)
⊢ IsThetaTVS.{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 [IsThetaTVS] using HasFDerivAtFilter.isThetaTVS_sub hf hf'

Premises used: HasFDerivAtFilter.isThetaTVS_sub, Asymptotics.IsThetaTVS
-- 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 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
hf' : IsInducing.{u_2, u_3} (X := E) (Y := F) (⇑f' : (a : E) → F)
⊢ IsEquivalent.{u_2, u_3} (E' := F) (𝓝 (x, x)) (fun (p : E × E) ↦ f p.1 - f p.2) fun (p : E × E) ↦
    (f' : (a : E) → F) (p.1 - p.2)

Tactic:
HasFDerivAtFilter.isEquivalent_sub hf hf'

Premises used: HasFDerivAtFilter.isEquivalent_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 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
hf' : IsInducing.{u_2, u_3} (X := E) (Y := F) (⇑f' : (a : E) → F)
⊢ IsThetaTVS.{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.isThetaTVS_sub hf hf'

Premises used: HasFDerivAtFilter.isThetaTVS_sub
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
rw :
  Tendsto (β := ℝ)
      (fun (x : E × E) ↦ ‖HSub.hSub (β := F) (f x.1 - f x.2) ((f' : (a : E) → F) (x.1 - x.2) : F)‖ / ‖x.1 - x.2‖) L
      (𝓝 0) ↔
    Tendsto (β := ℝ)
      (fun (p : E × E) ↦ ‖p.1 - p.2‖⁻¹ * ‖HSub.hSub (β := F) (f p.1 - f p.2) ((f' : (a : E) → F) (p.1 - p.2) : F)‖) L
      (𝓝 0)
rw₁ : ∀ (x : E × E), ‖x.1 - x.2‖ = 0 → ‖HSub.hSub (β := F) (f x.1 - f x.2) ((f' : (a : E) → F) (x.1 - x.2) : F)‖ = 0
⊢ HasFDerivAtFilter f f' L ↔
    Tendsto (β := ℝ)
      (fun (p : E × E) ↦ ‖p.1 - p.2‖⁻¹ * ‖HSub.hSub (β := F) (f p.1 - f p.2) ((f' : (a : E) → F) (p.1 - p.2) : F)‖) L
      (𝓝 0)

Tactic:
rw [hasFDerivAtFilter_iff_isLittleO, ← isLittleO_norm_left, ← isLittleO_norm_right,
    isLittleO_iff_tendsto]

Premises used: hasFDerivAtFilter_iff_isLittleO, Asymptotics.isLittleO_norm_right, Asymptotics.isLittleO_norm_left, Asymptotics.isLittleO_iff_tendsto
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
⊢ Tendsto (β := ℝ)
      (fun (x : E × E) ↦ ‖HSub.hSub (β := F) (f x.1 - f x.2) ((f' : (a : E) → F) (x.1 - x.2) : F)‖ / ‖x.1 - x.2‖) L
      (𝓝 0) ↔
    Tendsto (β := ℝ)
      (fun (p : E × E) ↦ ‖p.1 - p.2‖⁻¹ * ‖HSub.hSub (β := F) (f p.1 - f p.2) ((f' : (a : E) → F) (p.1 - p.2) : F)‖) L
      (𝓝 0)

Tactic:
simp [div_eq_inv_mul]

Premises used: div_eq_inv_mul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
⊢ ∀ (x : E × E), ‖x.1 - x.2‖ = 0 → ‖HSub.hSub (β := F) (f x.1 - f x.2) ((f' : (a : E) → F) (x.1 - x.2) : F)‖ = 0

Tactic:
simp +contextual [sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
⊢ HasFDerivWithinAt f f' s x ↔
    Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖)
      (𝓝[s] x) (𝓝 0)

Tactic:
simp [HasFDerivWithinAt, hasFDerivAtFilter_iff_tendsto, Function.comp_def]

Premises used: HasFDerivWithinAt, Function.comp_def, hasFDerivAtFilter_iff_tendsto
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
rw :
  HasFDerivWithinAt f f' univ x ↔
    Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖)
      (𝓝 x) (𝓝 0)
rw₁ :
  Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖)
      (𝓝[univ] x) (𝓝 0) ↔
    Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖)
      (𝓝 x) (𝓝 0)
rw₂ rw₃ :
  Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖)
      (𝓝 x) (𝓝 0) ↔
    Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖)
      (𝓝 x) (𝓝 0)
⊢ HasFDerivAt f f' x ↔
    Tendsto (β := ℝ) (fun (x' : E) ↦ ‖x' - x‖⁻¹ * ‖HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)‖)
      (𝓝 x) (𝓝 0)

Tactic:
rw [← hasFDerivWithinAt_univ, hasFDerivWithinAt_iff_tendsto, nhdsWithin_univ]

Premises used: nhdsWithin_univ, hasFDerivWithinAt_iff_tendsto, hasFDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
rw :
  IsLittleO.{u_2, u_3, u_2} (α := E) (E := F) (F := E) (𝓝 0)
      ((fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) ∘ fun (x_1 : E) ↦ x + x_1)
      ((fun (x' : E) ↦ x' - x) ∘ fun (x_1 : E) ↦ x + x_1) ↔
    IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝 0)
      (fun (h : E) ↦ HSub.hSub (β := F) (f (x + h) - f x) ((f' : (a : E) → F) h : F)) fun (h : E) ↦ h
⊢ HasFDerivAt f f' x ↔
    IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝 0)
      (fun (h : E) ↦ HSub.hSub (β := F) (f (x + h) - f x) ((f' : (a : E) → F) h : F)) fun (h : E) ↦ h

Tactic:
rw [hasFDerivAt_iff_isLittleO, ← map_add_left_nhds_zero x, isLittleO_map]

Premises used: hasFDerivAt_iff_isLittleO, Asymptotics.isLittleO_map, map_add_left_nhds_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
⊢ IsLittleO.{u_2, u_3, u_2} (α := E) (E := F) (F := E) (𝓝 0)
      ((fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x) ((f' : (a : E) → F) (x' - x) : F)) ∘ fun (x_1 : E) ↦ x + x_1)
      ((fun (x' : E) ↦ x' - x) ∘ fun (x_1 : E) ↦ x + x_1) ↔
    IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝 0)
      (fun (h : E) ↦ HSub.hSub (β := F) (f (x + h) - f x) ((f' : (a : E) → F) h : F)) fun (h : E) ↦ h

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
⊢ IsBigO.{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:
hf.isBigOTVS_sub.isBigO

Premises used: Asymptotics.IsBigOTVS.isBigO, HasStrictFDerivAt.isBigOTVS_sub
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
h : HasFDerivAtFilter f f' L
⊢ IsBigO.{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:
h.isBigOTVS_sub.isBigO

Premises used: Asymptotics.IsBigOTVS.isBigO, HasFDerivAtFilter.isBigOTVS_sub
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
s : Set E
h : HasFDerivWithinAt f f' s x₀
⊢ IsBigO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝[s] x₀) (fun (x : E) ↦ f x - f x₀) fun (x : E) ↦ x - x₀

Tactic:
h.isBigOTVS_sub.isBigO

Premises used: Asymptotics.IsBigOTVS.isBigO, HasFDerivWithinAt.isBigOTVS_sub
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
s : Set E
h : DifferentiableWithinAt 𝕜 f s x₀
⊢ IsBigO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝[s] x₀) (fun (x : E) ↦ f x - f x₀) fun (x : E) ↦ x - x₀

Tactic:
h.hasFDerivWithinAt.isBigO_sub

Premises used: HasFDerivWithinAt.isBigO_sub, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x₀ : E
h : HasFDerivAt f f' x₀
⊢ IsBigO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝 x₀) (fun (x : E) ↦ f x - f x₀) fun (x : E) ↦ x - x₀

Tactic:
h.isBigOTVS_sub.isBigO

Premises used: Asymptotics.IsBigOTVS.isBigO, HasFDerivAt.isBigOTVS_sub
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
h : DifferentiableAt 𝕜 f x₀
⊢ IsBigO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝 x₀) (fun (x : E) ↦ f x - f x₀) fun (x : E) ↦ x - x₀

Tactic:
h.hasFDerivAt.isBigO_sub

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.isBigO_sub
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
s : Set E
n : ℕ
h : IsBigO (F := ℝ) (𝓝[s] x₀) f fun (x : E) ↦ ‖x - x₀‖ ^ n
hx₀ : x₀ ∈ s
hn : 1 < n
simp_rw :
  IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝[s] x₀)
    (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - f x₀) ((0 : (a : E) → F) (x' - x₀) : F)) fun (x' : E) ↦ x' - x₀
simp_rw₁ :
  IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝[s] x₀)
    (fun (x' : E) ↦ HSub.hSub (β := F) (f x' - 0) ((0 : (a : E) → F) (x' - x₀) : F)) fun (x' : E) ↦ x' - x₀
simp_rw₂ : IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝[s] x₀) (fun (x' : E) ↦ f x' - 0 - 0) fun (x' : E) ↦ x' - x₀
simp_rw₃ : IsLittleO.{u_2, u_3, u_2} (E := F) (F := E) (𝓝[s] x₀) (fun (x' : E) ↦ f x') fun (x' : E) ↦ x' - x₀
⊢ HasFDerivWithinAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 s x₀

Tactic:
simp_rw [hasFDerivWithinAt_iff_isLittleO,
    h.eq_zero_of_norm_pow_within hx₀ hn.ne_bot, zero_apply, sub_zero,
    h.trans_isLittleO ((isLittleO_pow_sub_sub x₀ hn).mono nhdsWithin_le_nhds)]

Premises used: sub_zero, Asymptotics.IsBigO.eq_zero_of_norm_pow_within, hasFDerivWithinAt_iff_isLittleO, nhdsWithin_le_nhds, Asymptotics.IsBigO.trans_isLittleO, Asymptotics.isLittleO_pow_sub_sub, Asymptotics.IsLittleO.mono, ContinuousLinearMap.zero_apply, LT.lt.ne_bot
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
n : ℕ
h : IsBigO (F := ℝ) (𝓝 x₀) f fun (x : E) ↦ ‖x - x₀‖ ^ n
hn : 1 < n
⊢ IsBigO (F := ℝ) (𝓝[univ] x₀) f fun (x : E) ↦ ‖x - x₀‖ ^ n

Tactic:
rw [← nhdsWithin_univ] at h

Premises used: nhdsWithin_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
n : ℕ
h : IsBigO (F := ℝ) (𝓝 x₀) f fun (x : E) ↦ ‖x - x₀‖ ^ n
hn : 1 < n
h₁ : IsBigO (F := ℝ) (𝓝[univ] x₀) f fun (x : E) ↦ ‖x - x₀‖ ^ n
⊢ 1 < n

Tactic:
rw [← nhdsWithin_univ] at h

Premises used: nhdsWithin_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
n : ℕ
h : IsBigO (F := ℝ) (𝓝[univ] x₀) f fun (x : E) ↦ ‖x - x₀‖ ^ n
hn : 1 < n
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 x₀

Tactic:
(h.hasFDerivWithinAt (mem_univ _) hn).hasFDerivAt_of_univ

Premises used: HasFDerivWithinAt.hasFDerivAt_of_univ, Asymptotics.IsBigO.hasFDerivWithinAt, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x₀ : E
n : ℕ
h : IsBigO (F := ℝ) (𝓝[univ] x₀) f fun (x : E) ↦ ‖x - x₀‖ ^ n
hn : 1 < n
⊢ HasFDerivAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 x₀

Tactic:
exact (h.hasFDerivWithinAt (mem_univ _) hn).hasFDerivAt_of_univ

Premises used: HasFDerivWithinAt.hasFDerivAt_of_univ, Asymptotics.IsBigO.hasFDerivWithinAt, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
hf' : IsInducing.{u_2, u_3} (X := E) (Y := F) (⇑f' : (a : E) → F)
⊢ IsTheta.{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:
hf.isThetaTVS_sub hf' |>.isTheta

Premises used: HasStrictFDerivAt.isThetaTVS_sub, Asymptotics.IsThetaTVS.isTheta
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
L : Filter (E × E)
hf : HasFDerivAtFilter f f' L
hf' : IsInducing.{u_2, u_3} (X := E) (Y := F) (⇑f' : (a : E) → F)
⊢ IsTheta.{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:
hf.isThetaTVS_sub hf' |>.isTheta

Premises used: HasFDerivAtFilter.isThetaTVS_sub, Asymptotics.IsThetaTVS.isTheta
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
hf : HasFDerivWithinAt f f' s x
hf' : IsInducing.{u_2, u_3} (X := E) (Y := F) (⇑f' : (a : E) → F)
⊢ IsTheta.{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:
hf.isThetaTVS_sub hf' |>.isTheta

Premises used: HasFDerivWithinAt.isThetaTVS_sub, Asymptotics.IsThetaTVS.isTheta
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
hf : HasFDerivAt f f' x
hf' : IsInducing.{u_2, u_3} (X := E) (Y := F) (⇑f' : (a : E) → F)
⊢ IsTheta.{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:
hf.isThetaTVS_sub hf' |>.isTheta

Premises used: HasFDerivAt.isThetaTVS_sub, Asymptotics.IsThetaTVS.isTheta