awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
a : E
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ f (a + x)) s x) (fderivWithin 𝕜 f (a +ᵥ s) (a + x))

Tactic:
simp only [fderivWithin, hasFDerivWithinAt_comp_add_left, differentiableWithinAt_comp_add_left]

Premises used: fderivWithin, differentiableWithinAt_comp_add_left, hasFDerivWithinAt_comp_add_left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
a : E
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ f (a + x)) s x) (fderivWithin 𝕜 f (a +ᵥ s) (a + x))

Tactic:
classical
  simp only [fderivWithin, hasFDerivWithinAt_comp_add_left, differentiableWithinAt_comp_add_left]

Premises used: fderivWithin, differentiableWithinAt_comp_add_left, hasFDerivWithinAt_comp_add_left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
a : E
⊢ HasFDerivWithinAt (fun (x : E) ↦ f (x + a)) f' s x ↔ HasFDerivWithinAt f f' (a +ᵥ s) (x + a)

Tactic:
simpa only [add_comm a] using hasFDerivWithinAt_comp_add_left a

Premises used: add_comm, hasFDerivWithinAt_comp_add_left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
a : E
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (x : E) ↦ f (x + a)) s x ↔
    DifferentiableWithinAt 𝕜 f (a +ᵥ s) (x + a)

Tactic:
simp [DifferentiableWithinAt, hasFDerivWithinAt_comp_add_right]

Premises used: hasFDerivWithinAt_comp_add_right, DifferentiableWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
a : E
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ f (x + a)) s x) (fderivWithin 𝕜 f (a +ᵥ s) (x + a))

Tactic:
simp only [add_comm _ a, fderivWithin_comp_add_left]

Premises used: fderivWithin_comp_add_left, add_comm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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 a : E
⊢ HasFDerivAt (fun (x : E) ↦ f (x + a)) f' x ↔ HasFDerivAt f f' (x + a)

Tactic:
simp [← hasFDerivWithinAt_univ, hasFDerivWithinAt_comp_add_right]

Premises used: hasFDerivWithinAt_comp_add_right, hasFDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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 a : E
⊢ DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (x : E) ↦ f (x + a)) x ↔ DifferentiableAt 𝕜 f (x + a)

Tactic:
simp [DifferentiableAt, hasFDerivAt_comp_add_right]

Premises used: hasFDerivAt_comp_add_right, DifferentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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 a : E
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (fun (x : E) ↦ f (x + a)) x) (fderiv 𝕜 f (x + a))

Tactic:
simp [← fderivWithin_univ, fderivWithin_comp_add_right]

Premises used: fderivWithin_univ, fderivWithin_comp_add_right
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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 a : E
⊢ HasFDerivAt (fun (x : E) ↦ f (a + x)) f' x ↔ HasFDerivAt f f' (a + x)

Tactic:
simpa [add_comm a] using hasFDerivAt_comp_add_right a

Premises used: hasFDerivAt_comp_add_right, add_comm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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 a : E
⊢ DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (x : E) ↦ f (a + x)) x ↔ DifferentiableAt 𝕜 f (a + x)

Tactic:
simp [DifferentiableAt, hasFDerivAt_comp_add_left]

Premises used: DifferentiableAt, hasFDerivAt_comp_add_left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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 a : E
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (fun (x : E) ↦ f (a + x)) x) (fderiv 𝕜 f (a + x))

Tactic:
simpa [add_comm a] using fderiv_comp_add_right a

Premises used: add_comm, fderiv_comp_add_right
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
a : E
⊢ HasFDerivWithinAt (fun (x : E) ↦ f (x - a)) f' s x ↔ HasFDerivWithinAt f f' (-a +ᵥ s) (x - a)

Tactic:
simpa [sub_eq_add_neg] using hasFDerivWithinAt_comp_add_right (-a)

Premises used: sub_eq_add_neg, hasFDerivWithinAt_comp_add_right, Neg.neg
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
a : E
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (x : E) ↦ f (x - a)) s x ↔
    DifferentiableWithinAt 𝕜 f (-a +ᵥ s) (x - a)

Tactic:
simp [DifferentiableWithinAt, hasFDerivWithinAt_comp_sub]

Premises used: DifferentiableWithinAt, hasFDerivWithinAt_comp_sub
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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
a : E
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (fun (x : E) ↦ f (x - a)) s x) (fderivWithin 𝕜 f (-a +ᵥ s) (x - a))

Tactic:
simpa [sub_eq_add_neg] using fderivWithin_comp_add_right (-a)

Premises used: sub_eq_add_neg, fderivWithin_comp_add_right, Neg.neg
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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 a : E
⊢ HasFDerivAt (fun (x : E) ↦ f (x - a)) f' x ↔ HasFDerivAt f f' (x - a)

Tactic:
simp [← hasFDerivWithinAt_univ, hasFDerivWithinAt_comp_sub]

Premises used: hasFDerivWithinAt_comp_sub, hasFDerivWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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 a : E
⊢ DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (x : E) ↦ f (x - a)) x ↔ DifferentiableAt 𝕜 f (x - a)

Tactic:
simp [DifferentiableAt, hasFDerivAt_comp_sub]

Premises used: DifferentiableAt, hasFDerivAt_comp_sub
-- Module: Mathlib.Analysis.Calculus.FDeriv.Add
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 a : E
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (fun (x : E) ↦ f (x - a)) x) (fderiv 𝕜 f (x - a))

Tactic:
simp [← fderivWithin_univ, fderivWithin_comp_sub]

Premises used: fderivWithin_univ, fderivWithin_comp_sub
-- Module: Mathlib.Analysis.Calculus.FDeriv.Affine
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
L : Filter (E × E)
⊢ HasFDerivAtFilter (⇑f : (a : E) → F) f.contLinear L

Tactic:
.of_isLittleOTVS <| .congr_left (.zero _ _) ?_

Premises used: Asymptotics.IsLittleOTVS.zero, Asymptotics.IsLittleOTVS.congr_left, HasFDerivAtFilter.of_isLittleOTVS
-- Module: Mathlib.Analysis.Calculus.FDeriv.Affine
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
L : Filter (E × E)
refine :
  ∀ (x : E × E),
    0 x =
      HSub.hSub (β := F) (HSub.hSub (α := F) (β := F) ((f : (a : E) → F) x.1 : F) ((f : (a : E) → F) x.2 : F))
        ((f.contLinear : (a : E) → F) (x.1 - x.2) : F)
⊢ HasFDerivAtFilter (⇑f : (a : E) → F) f.contLinear L

Tactic:
refine .of_isLittleOTVS <| .congr_left (.zero _ _) ?_
-- Module: Mathlib.Analysis.Calculus.FDeriv.Affine
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
L : Filter (E × E)
⊢ ∀ (x : E × E),
    0 x =
      HSub.hSub (β := F) (HSub.hSub (α := F) (β := F) ((f : (a : E) → F) x.1 : F) ((f : (a : E) → F) x.2 : F))
        ((f.contLinear : (a : E) → F) (x.1 - x.2) : F)

Tactic:
simp [(vsub_eq_sub _ _).symm.trans (f.contLinear_map_vsub _ _).symm]

Premises used: ContinuousAffineMap.contLinear_map_vsub, Eq.symm, vsub_eq_sub, Eq.trans
-- Module: Mathlib.Analysis.Calculus.FDeriv.Affine
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
⊢ HasStrictFDerivAt (⇑f : (a : E) → F) f.contLinear x

Tactic:
f.hasFDerivAtFilter

Premises used: ContinuousAffineMap.hasFDerivAtFilter, HasStrictFDerivAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Affine
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
⊢ HasFDerivWithinAt (⇑f : (a : E) → F) f.contLinear s x

Tactic:
f.hasFDerivAtFilter

Premises used: HasFDerivWithinAt, ContinuousAffineMap.hasFDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Affine
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
⊢ HasFDerivAt (⇑f : (a : E) → F) f.contLinear x

Tactic:
f.hasFDerivAtFilter

Premises used: HasFDerivAt, ContinuousAffineMap.hasFDerivAtFilter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Affine
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
⊢ DifferentiableAt.{u_1, u_2, u_3} 𝕜 (F := F) (⇑f : (a : E) → F) x

Tactic:
f.hasFDerivAt.differentiableAt

Premises used: ContinuousAffineMap.hasFDerivAt, HasFDerivAt.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Affine
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
⊢ DifferentiableWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (⇑f : (a : E) → F) s x

Tactic:
f.differentiableAt.differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, ContinuousAffineMap.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Affine
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
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (⇑f : (a : E) → F) x) f.contLinear

Tactic:
f.hasFDerivAt.fderiv

Premises used: ContinuousAffineMap.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Affine
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
hxs : UniqueDiffWithinAt 𝕜 s x
rw : Eq (α := E →L[𝕜] F) (fderiv 𝕜 (⇑f : (a : E) → F) x) f.contLinear
⊢ Eq (α := E →L[𝕜] F) (fderivWithin 𝕜 (⇑f : (a : E) → F) s x) f.contLinear

Tactic:
rw [DifferentiableAt.fderivWithin f.differentiableAt hxs]

Premises used: DifferentiableAt.fderivWithin, ContinuousAffineMap.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Affine
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
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (⇑f : (a : E) → F) x) f.contLinear

Tactic:
f.fderiv

Premises used: ContinuousAffineMap.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Affine
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
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ Eq (α := E →L[𝕜] F) (fderiv 𝕜 (⇑f : (a : E) → F) x) f.contLinear

Tactic:
exact f.fderiv

Premises used: ContinuousAffineMap.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Affine
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
⊢ Differentiable.{u_1, u_2, u_3} 𝕜 (E := E) (F := F) (⇑f : (a : E) → F)

Tactic:
fun _ =>
  f.differentiableAt

Premises used: Differentiable, ContinuousAffineMap.differentiableAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Affine
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
s : Set E
⊢ DifferentiableOn.{u_1, u_2, u_3} 𝕜 (F := F) (⇑f : (a : E) → F) s

Tactic:
f.differentiable.differentiableOn

Premises used: ContinuousAffineMap.differentiable, Differentiable.differentiableOn
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
⊢ IsLittleO.{u, v, u} (E := F) (F := E) (𝓝[insert x s ×ˢ insert x s] (x, x))
    (fun (y : E × E) ↦
      HSub.hSub (β := F) (f y.1 - f y.2)
        ((((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
                  (p 1) :
                E →L[𝕜] F) :
              (a : E) → F)
            (y.1 - y.2) :
          F))
    fun (y : E × E) ↦ y.1 - y.2

Tactic:
h.isBigO_image_sub_norm_mul_norm_sub.trans_isLittleO (IsLittleO.of_norm_right ?_)

Premises used: cast, Fin.snoc, dite, HasFPowerSeriesWithinAt.isBigO_image_sub_norm_mul_norm_sub, Asymptotics.IsBigO.trans_isLittleO, Asymptotics.IsLittleO.of_norm_right
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
refine :
  IsLittleO (E := ℝ) (F := ℝ) (𝓝[insert x s ×ˢ insert x s] (x, x)) (fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖)
    fun (x : E × E) ↦ ‖x.1 - x.2‖
⊢ IsLittleO.{u, v, u} (E := F) (F := E) (𝓝[insert x s ×ˢ insert x s] (x, x))
    (fun (y : E × E) ↦
      HSub.hSub (β := F) (f y.1 - f y.2)
        ((((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
                  (p 1) :
                E →L[𝕜] F) :
              (a : E) → F)
            (y.1 - y.2) :
          F))
    fun (y : E × E) ↦ y.1 - y.2

Tactic:
refine h.isBigO_image_sub_norm_mul_norm_sub.trans_isLittleO (IsLittleO.of_norm_right ?_)

Premises used: HasFPowerSeriesWithinAt.isBigO_image_sub_norm_mul_norm_sub, Asymptotics.IsBigO.trans_isLittleO, Asymptotics.IsLittleO.of_norm_right
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
⊢ IsLittleO (E := ℝ) (F := ℝ) (𝓝[insert x s ×ˢ insert x s] (x, x)) (fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖)
    fun (x : E × E) ↦ ‖x.1 - x.2‖

Tactic:
isLittleO_iff_exists_eq_mul.2 ⟨fun y => ‖y - (x, x)‖, ?_, EventuallyEq.rfl⟩

Premises used: Iff.mpr, Norm.norm, HSub.hSub, Prod.mk, Asymptotics.isLittleO_iff_exists_eq_mul, And.intro, Exists.intro, Filter.EventuallyEq.rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
refine : Tendsto (β := ℝ) (fun (y : E × E) ↦ ‖y - (x, x)‖) (𝓝[insert x s ×ˢ insert x s] (x, x)) (𝓝 0)
⊢ IsLittleO (E := ℝ) (F := ℝ) (𝓝[insert x s ×ˢ insert x s] (x, x)) (fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖)
    fun (x : E × E) ↦ ‖x.1 - x.2‖

Tactic:
refine isLittleO_iff_exists_eq_mul.2 ⟨fun y => ‖y - (x, x)‖, ?_, EventuallyEq.rfl⟩

Premises used: Iff.mpr, Norm.norm, HSub.hSub, Prod.mk, Asymptotics.isLittleO_iff_exists_eq_mul, And.intro, Exists.intro, Filter.EventuallyEq.rfl
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
apply : Tendsto (β := ℝ) (fun (y : E × E) ↦ ‖y - (x, x)‖) (𝓝 (x, x)) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (y : E × E) ↦ ‖y - (x, x)‖) (𝓝[insert x s ×ˢ insert x s] (x, x)) (𝓝 0)

Tactic:
apply Tendsto.mono_left _ nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds, Filter.Tendsto.mono_left
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
⊢ Tendsto (β := ℝ) (fun (y : E × E) ↦ ‖y - (x, x)‖) (𝓝 (x, x)) (𝓝 0)

Tactic:
(continuous_id.sub continuous_const).norm.tendsto' _ _ ?_

Premises used: continuous_const, setOf, Continuous.norm, continuous_id, Continuous.tendsto', Continuous.sub
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
refine : ‖id (x, x) - (x, x)‖ = 0
⊢ Tendsto (β := ℝ) (fun (y : E × E) ↦ ‖y - (x, x)‖) (𝓝 (x, x)) (𝓝 0)

Tactic:
refine (continuous_id.sub continuous_const).norm.tendsto' _ _ ?_

Premises used: continuous_const, Continuous.norm, continuous_id, Continuous.tendsto', Continuous.sub
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
rw : ‖(x, x) - (x, x)‖ = 0
rw₁ : norm.{u} (E := E × E) 0 = 0
rw₂ rw₃ : Eq (α := ℝ) 0 0
⊢ ‖id (x, x) - (x, x)‖ = 0

Tactic:
rw [_root_.id, sub_self, norm_zero]

Premises used: sub_self, norm_zero, id
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
h : HasFPowerSeriesAt f p x
⊢ HasStrictFDerivAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p 1))
    x

Tactic:
simpa only [hasStrictFDerivAt_iff_isLittleO, Set.insert_eq_of_mem, Set.mem_univ,
      Set.univ_prod_univ, nhdsWithin_univ]
    using (h.hasFPowerSeriesWithinAt (s := Set.univ)).hasStrictFDerivWithinAt

Premises used: HasFPowerSeriesWithinAt.hasStrictFDerivWithinAt, nhdsWithin_univ, hasStrictFDerivAt_iff_isLittleO, HasFPowerSeriesAt.hasFPowerSeriesWithinAt, Set.insert_eq_of_mem, Set.univ_prod_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
rw :
  ∀ ⦃c : ℝ⦄,
    0 < c →
      ∀ᶠ (x_1 : E) in 𝓝[insert x s] x,
        ‖HSub.hSub (β := F) (f x_1 - f x)
              ((((continuousMultilinearCurryFin1 𝕜 E F :
                          (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
                        (p 1) :
                      E →L[𝕜] F) :
                    (a : E) → F)
                  (x_1 - x) :
                F)‖ ≤
          c * ‖x_1 - x‖
⊢ HasFDerivWithinAt.{u_1, u, v} (𝕜 := 𝕜) f
    ((continuousMultilinearCurryFin1 𝕜 E F : (a : ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E) F) → E →L[𝕜] F)
      (p 1))
    (insert x s) x

Tactic:
rw [hasFDerivWithinAt_iff_isLittleO, isLittleO_iff]

Premises used: hasFDerivWithinAt_iff_isLittleO, Asymptotics.isLittleO_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
c : ℝ
hc : 0 < c
rw : Tendsto (fun (y : E) ↦ (y, x)) (𝓝[insert x s] x) (𝓝[insert x s] x ×ˢ 𝓝[insert x s] x)
⊢ Tendsto (fun (y : E) ↦ (y, x)) (𝓝[insert x s] x) (𝓝[insert x s ×ˢ insert x s] (x, x))

Tactic:
rw [nhdsWithin_prod_eq]

Premises used: nhdsWithin_prod_eq
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type v
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
x : E
s : Set E
h : HasFPowerSeriesWithinAt f p s x
c : ℝ
hc : 0 < c
⊢ x ∈ insert x s

Tactic:
simp