awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Analytic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
r : ℝ≥0∞
y : E
n : ℕ
ih :
  ∀ {F : Type (max u v)} [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F] [CompleteSpace F]
    {p : FormalMultilinearSeries 𝕜 E F} {f : E → F},
    HasFPowerSeriesOnBall f p x r →
      HSMul.hSMul (β := F) n ! ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
        (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
F : Type (max u v)
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
f : E → F
h : HasFPowerSeriesOnBall f p x r
⊢ Eq (α := F)
    (((iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x : Fin n) ↦ y : (a : E) → F) y : F)
    ((((iteratedFDeriv 𝕜 n (fun (y : E) ↦ fderiv 𝕜 f y) x : (a : (i : Fin n) → E) → E →L[𝕜] F)
              (Fin.init (α := fun (i : Fin (n + 1)) ↦ E) fun (x : Fin (n + 1)) ↦ y) :
            E →L[𝕜] F) :
          (a : E) → F)
        y :
      F)

Tactic:
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
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
y : E
inst_5 : CompleteSpace F
n : ℕ
zero :
  HSMul.hSMul (β := F) 0! ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F) =
    (iteratedFDeriv 𝕜 0 f x : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y
succ :
  ∀ (n : ℕ),
    HSMul.hSMul (β := F) (n + 1)! ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y : F) =
      (iteratedFDeriv 𝕜 (n + 1) f x : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y
⊢ HSMul.hSMul (β := F) n ! ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y

Tactic:
cases n
-- 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
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
y : E
inst_5 : CompleteSpace F
zero :
  HSMul.hSMul (α := ℕ) (β := F) 1 ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F) =
    (iteratedFDeriv 𝕜 0 f x : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y
zero₁ :
  Eq.{v + 1} (α := F) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F)
    ((iteratedFDeriv 𝕜 0 f x : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F)
zero₂ zero₃ :
  Eq.{v + 1} (α := F) ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F)
    ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F)
⊢ HSMul.hSMul (β := F) 0! ((p 0 : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y : F) =
    (iteratedFDeriv 𝕜 0 f x : (a : (i : Fin 0) → E) → F) fun (x : Fin 0) ↦ y

Tactic:
rw [factorial_zero, one_smul, h.iteratedFDeriv_zero_apply_diag]

Premises used: one_smul, HasFPowerSeriesOnBall.iteratedFDeriv_zero_apply_diag, Nat.factorial_zero
-- 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
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
y : E
inst_5 : CompleteSpace F
n : ℕ
succ :
  Eq.{v + 1} (α := F)
    (((iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x : Fin n) ↦ y : (a : E) → F) y : F)
    ((((iteratedFDeriv 𝕜 n (fun (y : E) ↦ fderiv 𝕜 f y) x : (a : (i : Fin n) → E) → E →L[𝕜] F)
              (Fin.init (α := fun (i : Fin (n + 1)) ↦ E) fun (x : Fin (n + 1)) ↦ y) :
            E →L[𝕜] F) :
          (a : E) → F)
        y :
      F)
⊢ HSMul.hSMul (β := F) (n + 1)! ((p (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y : F) =
    (iteratedFDeriv 𝕜 (n + 1) f x : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y

Tactic:
rw [factorial_succ, mul_comm, mul_smul, ← derivSeries_apply_diag,
      ← ContinuousLinearMap.smul_apply, factorial_smul' _ h.fderiv, iteratedFDeriv_succ_apply_right]

Premises used: ContinuousLinearMap.smul_apply, Nat.factorial_succ, _private.0.HasFPowerSeriesOnBall.factorial_smul', HasFPowerSeriesOnBall.fderiv, iteratedFDeriv_succ_apply_right, mul_comm, FormalMultilinearSeries.derivSeries_apply_diag, SemigroupAction.mul_smul
-- 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
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
y : E
inst_5 : CompleteSpace F
n : ℕ
⊢ Eq.{v + 1} (α := F)
    (((iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x : (a : (i : Fin n) → E) → E →L[𝕜] F) fun (x : Fin n) ↦ y : (a : E) → F) y : F)
    ((((iteratedFDeriv 𝕜 n (fun (y : E) ↦ fderiv 𝕜 f y) x : (a : (i : Fin n) → E) → E →L[𝕜] F)
              (Fin.init (α := fun (i : Fin (n + 1)) ↦ E) fun (x : Fin (n + 1)) ↦ y) :
            E →L[𝕜] F) :
          (a : E) → F)
        y :
      F)

Tactic:
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
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
inst_5 : CompleteSpace F
inst_6 : CharZero 𝕜
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))

Tactic:
h.hasSum hy

Premises used: HasFPowerSeriesOnBall.hasSum
-- 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
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
inst_5 : CompleteSpace F
inst_6 : CharZero 𝕜
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h₁ :
  ∀ (n : ℕ),
    HSMul.hSMul.{u_1, v, v} (α := 𝕜) (β := F) (↑n ! : 𝕜)⁻¹
        ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
      (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
⊢ HasSum
    (fun (n : ℕ) ↦
      HSMul.hSMul.{u_1, v, v} (α := 𝕜) (β := F) (↑n ! : 𝕜)⁻¹
        ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F))
    (f (x + y))

Tactic:
convert! h.hasSum hy with n

Premises used: HasFPowerSeriesOnBall.hasSum
-- 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
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
inst_5 : CompleteSpace F
inst_6 : CharZero 𝕜
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
n : ℕ
h₁ :
  HSMul.hSMul.{u_1, v, v} (α := 𝕜) (↑n ! : 𝕜)⁻¹
      (HSMul.hSMul (β := F) n ! ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F)) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
h₂ :
  n ! •
      HSMul.hSMul.{u_1, v, v} (α := 𝕜) (β := F) (↑n ! : 𝕜)⁻¹
        ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
h₃ :
  HSMul.hSMul (β := F) (HSMul.hSMul (β := 𝕜) n ! (↑n ! : 𝕜)⁻¹)
      ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
h₄ :
  HSMul.hSMul (β := F) (HMul.hMul (α := 𝕜) (↑n ! : 𝕜) (↑n ! : 𝕜)⁻¹)
      ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
h₅ :
  HSMul.hSMul.{u_1, v, v} (α := 𝕜) (β := F) 1 ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y
h₆ h₇ :
  Eq.{v + 1} (α := F) ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F)
    ((p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F)
⊢ HSMul.hSMul.{u_1, v, v} (α := 𝕜) (β := F) (↑n ! : 𝕜)⁻¹
      ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y : F) =
    (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y

Tactic:
rw [← h.factorial_smul y n, smul_comm, ← smul_assoc, nsmul_eq_mul,
    mul_inv_cancel₀ <| cast_ne_zero.mpr n.factorial_ne_zero, one_smul]

Premises used: Iff.mpr, smul_assoc, mul_inv_cancel₀, one_smul, HasFPowerSeriesOnBall.factorial_smul, Nat.factorial_ne_zero, nsmul_eq_mul, SMulCommClass.smul_comm, Nat.cast_ne_zero
-- 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
ι : Type u_2
G : ι → Type u_3
inst_5 : (i : ι) → NormedAddCommGroup (G i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (G i)
inst_7 : Fintype ι
inst_8 : DecidableEq ι
f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F
v : E × ((i : ι) → G i)
⊢ HasFDerivAt (𝕜 := 𝕜) (F := F)
    (fun (p : E × ((i : ι) → G i)) ↦
      (((f : (a : E) → ContinuousMultilinearMap 𝕜 G F) p.1 : ContinuousMultilinearMap 𝕜 G F) : (a : (i : ι) → G i) → F)
        p.2)
    (HAdd.hAdd (α := E × ((i : ι) → G i) →L[𝕜] F)
      (comp (σ₂₃ := RingHom.id 𝕜) ((f.flipMultilinear (E := G) : (a : (i : ι) → G i) → E →L[𝕜] F) v.2)
        (fst 𝕜 E ((i : ι) → G i)))
      (∑ i : ι,
        comp (σ₁₂ := RingHom.id 𝕜)
          (ContinuousMultilinearMap.toContinuousLinearMap.{u_1, u_2, u_3, v} (R := 𝕜) (M₁ := G) (M₂ := F)
              ((f : (a : E) → ContinuousMultilinearMap 𝕜 G F) v.1) v.2 i :
            ContinuousLinearMap.{u_1, u_1, u_3, v} (RingHom.id 𝕜) (G i) F)
          (comp (σ₂₃ := RingHom.id 𝕜) (proj (φ := G) i) (snd 𝕜 E ((i : ι) → G i)) : E × ((i : ι) → G i) →L[𝕜] G i)))
    v

Tactic:
(f ∘L .fst 𝕜 E (∀ i, G i)).hasFDerivAt.continuousMultilinearMap_apply
    (hasFDerivAt_pi'.mp (hasFDerivAt_snd (E := E) (F := ∀ i, G i)))

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.hasFDerivAt, hasFDerivAt_snd, setOf, Iff.mp, ContinuousLinearMap.fst, hasFDerivAt_pi', HasFDerivAt.continuousMultilinearMap_apply
-- 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
ι : Type u_2
G : ι → Type u_3
inst_5 : (i : ι) → NormedAddCommGroup (G i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (G i)
inst_7 : Fintype ι
H : Type u_4
inst_8 : NormedAddCommGroup H
inst_9 : NormedSpace 𝕜 H
inst_10 : DecidableEq ι
a : H → E
a' : H →L[𝕜] E
b : (i : ι) → H → G i
b' : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_3} (RingHom.id 𝕜) H (G i)
s : Set H
x : H
ha : HasFDerivWithinAt a a' s x
hb : ∀ (i : ι), HasFDerivWithinAt (b i) (b' i) s x
f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F
⊢ HasFDerivWithinAt
    (fun (y : H) ↦
      (((f : (a : E) → ContinuousMultilinearMap 𝕜 G F) (a y) : ContinuousMultilinearMap 𝕜 G F) :
          (a : (i : ι) → G i) → F)
        fun (i : ι) ↦ b i y)
    (HAdd.hAdd (α := H →L[𝕜] F)
      (comp (σ₂₃ := RingHom.id 𝕜) ((f.flipMultilinear (E := G) : (a : (i : ι) → G i) → E →L[𝕜] F) fun (i : ι) ↦ b i x)
        a')
      (∑ i : ι,
        comp (σ₂₃ := RingHom.id 𝕜)
          (ContinuousMultilinearMap.toContinuousLinearMap.{u_1, u_2, u_3, v} (R := 𝕜) (M₁ := G) (M₂ := F)
            ((f : (a : E) → ContinuousMultilinearMap 𝕜 G F) (a x)) (fun (j : ι) ↦ b j x) i)
          (b' i)))
    s x

Tactic:
(f.hasFDerivAt.comp_hasFDerivWithinAt x ha).continuousMultilinearMap_apply hb

Premises used: HasFDerivWithinAt.continuousMultilinearMap_apply, ContinuousLinearMap.hasFDerivAt, HasFDerivAt.comp_hasFDerivWithinAt
-- 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
ι : Type u_2
G : ι → Type u_3
inst_5 : (i : ι) → NormedAddCommGroup (G i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_3} 𝕜 (G i)
inst_7 : Fintype ι
H : Type u_4
inst_8 : NormedAddCommGroup H
inst_9 : NormedSpace 𝕜 H
inst_10 : DecidableEq ι
a : H → E
a' : H →L[𝕜] E
b : (i : ι) → H → G i
b' : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_4, u_3} (RingHom.id 𝕜) H (G i)
x : H
ha : HasFDerivAt a a' x
hb : ∀ (i : ι), HasFDerivAt (b i) (b' i) x
f : E →L[𝕜] ContinuousMultilinearMap 𝕜 G F
⊢ HasFDerivAt
    (fun (y : H) ↦
      (((f : (a : E) → ContinuousMultilinearMap 𝕜 G F) (a y) : ContinuousMultilinearMap 𝕜 G F) :
          (a : (i : ι) → G i) → F)
        fun (i : ι) ↦ b i y)
    (HAdd.hAdd (α := H →L[𝕜] F)
      (comp (σ₂₃ := RingHom.id 𝕜) ((f.flipMultilinear (E := G) : (a : (i : ι) → G i) → E →L[𝕜] F) fun (i : ι) ↦ b i x)
        a')
      (∑ i : ι,
        comp (σ₂₃ := RingHom.id 𝕜)
          (ContinuousMultilinearMap.toContinuousLinearMap.{u_1, u_2, u_3, v} (R := 𝕜) (M₁ := G) (M₂ := F)
            ((f : (a : E) → ContinuousMultilinearMap 𝕜 G F) (a x)) (fun (j : ι) ↦ b j x) i)
          (b' i)))
    x

Tactic:
(f.hasFDerivAt.comp x ha).continuousMultilinearMap_apply hb

Premises used: ContinuousLinearMap.hasFDerivAt, HasFDerivAt.comp, HasFDerivAt.continuousMultilinearMap_apply
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
α : Type u_4
l : Filter α
c : α → 𝕜
d : α → E
v : E
dlim : Tendsto d l (𝓝 0)
dtop : ∀ᶠ (n : α) in l, x + d n ∈ s
cdlim : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 v)
rw : Tendsto (fun (n : α) ↦ x + d n) l (𝓝 x) ∧ ∀ᶠ (n : α) in l, x + d n ∈ s
⊢ Tendsto (fun (n : α) ↦ x + d n) l (𝓝[s] x)

Tactic:
rw [tendsto_nhdsWithin_iff]

Premises used: tendsto_nhdsWithin_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
α : Type u_4
l : Filter α
c : α → 𝕜
d : α → E
v : E
dlim : Tendsto d l (𝓝 0)
dtop : ∀ᶠ (n : α) in l, x + d n ∈ s
cdlim : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 v)
⊢ Tendsto (fun (n : α) ↦ x + d n) l (𝓝 x)

Tactic:
simpa using tendsto_const_nhds.add dlim

Premises used: tendsto_const_nhds, Filter.Tendsto.add
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
α : Type u_4
l : Filter α
c : α → 𝕜
d : α → E
v : E
dlim : Tendsto d l (𝓝 0)
dtop : ∀ᶠ (n : α) in l, x + d n ∈ s
cdlim : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 v)
⊢ Tendsto (fun (n : α) ↦ x + d n) l (𝓝 x) ∧ ∀ᶠ (n : α) in l, x + d n ∈ s

Tactic:
exact ⟨by simpa using tendsto_const_nhds.add dlim, dtop⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
α : Type u_4
l : Filter α
c : α → 𝕜
d : α → E
v : E
dlim : Tendsto d l (𝓝 0)
dtop : ∀ᶠ (n : α) in l, x + d n ∈ s
cdlim : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 v)
⊢ Tendsto (fun (n : α) ↦ x + d n) l (𝓝[s] x)

Tactic:
have tendsto_arg : Tendsto (fun n => x + d n) l (𝓝[s] x) := by
    rw [tendsto_nhdsWithin_iff]
    exact ⟨by simpa using tendsto_const_nhds.add dlim, dtop⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
α : Type u_4
l : Filter α
c : α → 𝕜
d : α → E
v : E
dlim : Tendsto d l (𝓝 0)
dtop : ∀ᶠ (n : α) in l, x + d n ∈ s
cdlim : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 v)
tendsto_arg : Tendsto (fun (n : α) ↦ x + d n) l (𝓝[s] x)
⊢ IsLittleOTVS.{u_1, u_4, u_3, u_2} 𝕜 (E := F) (F := E) l
    (fun (n : α) ↦ HSub.hSub (β := F) (c n • (f (x + d n) - f x)) ((f' : (a : E) → F) (c n • d n) : F)) fun (n : α) ↦
    c n • d n

Tactic:
simpa [smul_sub] using h.isLittleOTVS.comp_tendsto tendsto_arg |>.smul_left c

Premises used: Asymptotics.IsLittleOTVS.smul_left, Asymptotics.IsLittleOTVS.comp_tendsto, smul_sub, HasFDerivWithinAt.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
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
α : Type u_4
l : Filter α
c : α → 𝕜
d : α → E
v : E
dlim : Tendsto d l (𝓝 0)
dtop : ∀ᶠ (n : α) in l, x + d n ∈ s
cdlim : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 v)
tendsto_arg : Tendsto (fun (n : α) ↦ x + d n) l (𝓝[s] x)
⊢ IsLittleOTVS.{u_1, u_4, u_3, u_1} 𝕜 (E := F) (F := 𝕜) l
    (fun (n : α) ↦ HSub.hSub (β := F) (c n • (f (x + d n) - f x)) ((f' : (a : E) → F) (c n • d n) : F)) 1

Tactic:
have := calc
    (fun n ↦ c n • (f (x + d n) - f x) - f' (c n • d n)) =o[𝕜; l] fun n ↦ c n • d n := by
      simpa [smul_sub] using h.isLittleOTVS.comp_tendsto tendsto_arg |>.smul_left c
    _ =O[𝕜; l] (1 : α → 𝕜) := cdlim.isBigOTVS_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
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
α : Type u_4
l : Filter α
c : α → 𝕜
d : α → E
v : E
dlim : Tendsto d l (𝓝 0)
dtop : ∀ᶠ (n : α) in l, x + d n ∈ s
cdlim : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 v)
tendsto_arg : Tendsto (fun (n : α) ↦ x + d n) l (𝓝[s] x)
this :
  IsLittleOTVS.{u_1, u_4, u_3, u_1} 𝕜 (E := F) (F := 𝕜) l
    (fun (n : α) ↦ HSub.hSub (β := F) (c n • (f (x + d n) - f x)) ((f' : (a : E) → F) (c n • d n) : F)) 1
⊢ Tendsto.{u_4, u_3} (β := F)
    (fun (n : α) ↦ HSub.hSub (β := F) (c n • (f (x + d n) - f x)) ((f' : (a : E) → F) (c n • d n) : F)) 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
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' : E →L[𝕜] F
x : E
s : Set E
h : HasFDerivWithinAt f f' s x
α : Type u_4
l : Filter α
c : α → 𝕜
d : α → E
v : E
dlim : Tendsto d l (𝓝 0)
dtop : ∀ᶠ (n : α) in l, x + d n ∈ s
cdlim : Tendsto (fun (n : α) ↦ c n • d n) l (𝓝 v)
tendsto_arg : Tendsto (fun (n : α) ↦ x + d n) l (𝓝[s] x)
this :
  Tendsto.{u_4, u_3} (β := F)
    (fun (n : α) ↦ HSub.hSub (β := F) (c n • (f (x + d n) - f x)) ((f' : (a : E) → F) (c n • d n) : F)) l (𝓝 0)
⊢ Tendsto.{u_4, u_3} (β := F) (fun (n : α) ↦ c n • (f (x + d n) - f x)) l (𝓝 ((f' : (a : E) → F) v) : Filter F)

Tactic:
simpa using this.add <| ((map_continuous f').tendsto v).comp cdlim

Premises used: Continuous.tendsto, Filter.Tendsto.add, ContinuousMapClass.map_continuous, 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
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' f₁' : E →L[𝕜] F
x : E
s : Set E
inst_11 : T2Space F
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt f f₁' s x
y : E
hy : y ∈ tangentConeAt 𝕜 s x
rcases :
  ∀ (ι : Type (max u_1 u_2)) (l : Filter ι) (hl : l.NeBot) (c : ι → 𝕜) (d : ι → E) (hd₀ : Tendsto d l (𝓝 0))
    (hds : ∀ᶠ (n : ι) in l, x + d n ∈ s) (hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)),
    Eq.{u_3 + 1} (α := F) ((f' : (a : E) → F) y : F) ((f₁' : (a : E) → F) y : F)
⊢ Eq.{u_3 + 1} (α := F) ((f' : (a : E) → F) y : F) ((f₁' : (a : E) → F) y : F)

Tactic:
rcases exists_fun_of_mem_tangentConeAt hy with ⟨ι, l, hl, c, d, hd₀, hds, hcd⟩

Premises used: exists_fun_of_mem_tangentConeAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' f₁' : E →L[𝕜] F
x : E
s : Set E
inst_11 : T2Space F
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt f f₁' s x
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : Type (max u_1 u_2)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x + d n ∈ s
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
⊢ Eq.{u_3 + 1} (α := F) ((f' : (a : E) → F) y : F) ((f₁' : (a : E) → F) y : F)

Tactic:
tendsto_nhds_unique (hf.lim hd₀ hds hcd) (hg.lim hd₀ hds hcd)

Premises used: HasFDerivWithinAt.lim, tendsto_nhds_unique
-- Module: Mathlib.Analysis.Calculus.FDeriv.Basic
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : TopologicalSpace E
inst_4 : ContinuousAdd E
inst_5 : ContinuousSMul 𝕜 E
F : Type u_3
inst_6 : AddCommGroup F
inst_7 : Module 𝕜 F
inst_8 : TopologicalSpace F
inst_9 : ContinuousAdd F
inst_10 : ContinuousSMul 𝕜 F
f : E → F
f' f₁' : E →L[𝕜] F
x : E
s : Set E
inst_11 : T2Space F
hf : HasFDerivWithinAt f f' s x
hg : HasFDerivWithinAt f f₁' s x
y : E
hy : y ∈ tangentConeAt 𝕜 s x
ι : Type (max u_1 u_2)
l : Filter ι
hl : l.NeBot
c : ι → 𝕜
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hds : ∀ᶠ (n : ι) in l, x + d n ∈ s
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
⊢ Eq.{u_3 + 1} (α := F) ((f' : (a : E) → F) y : F) ((f₁' : (a : E) → F) y : F)

Tactic:
exact tendsto_nhds_unique (hf.lim hd₀ hds hcd) (hg.lim hd₀ hds hcd)

Premises used: HasFDerivWithinAt.lim, tendsto_nhds_unique