awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x v w : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hf :
  ∀ (x_1 : (i : Fin 2) → E),
    Eq.{u_3 + 1} (α := F)
      ((iteratedFDerivWithin 𝕜 2 f s x : (a : (i : Fin 2) → E) → F) fun (i : Fin 2) ↦
          x_1 ((Fin.revPerm : (a : Fin 2) → Fin 2) i) :
        F)
      ((iteratedFDerivWithin 𝕜 2 f s x : (a : (i : Fin 2) → E) → F) x_1 : F)
i : Fin (Nat.succ 1)
h :
  ![v, w] ((fun (i : Fin (Nat.succ 1)) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 1))) =
    ![w, v] ((Fin.revPerm : (a : Fin 2) → Fin 2) ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨0, ⋯⟩))
h₁ :
  ![v, w] ((fun (i : Fin (Nat.succ 1)) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 1))) =
    ![w, v] ((Fin.revPerm : (a : Fin 2) → Fin 2) ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨1, ⋯⟩))
⊢ ![v, w] i = ![w, v] ((Fin.revPerm : (a : Fin 2) → Fin 2) i)

Tactic:
fin_cases i
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x v w : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hf :
  ∀ (x_1 : (i : Fin 2) → E),
    Eq.{u_3 + 1} (α := F)
      ((iteratedFDerivWithin 𝕜 2 f s x : (a : (i : Fin 2) → E) → F) fun (i : Fin 2) ↦
          x_1 ((Fin.revPerm : (a : Fin 2) → Fin 2) i) :
        F)
      ((iteratedFDerivWithin 𝕜 2 f s x : (a : (i : Fin 2) → E) → F) x_1 : F)
⊢ ![v, w] ((fun (i : Fin (Nat.succ 1)) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 1))) =
    ![w, v] ((Fin.revPerm : (a : Fin 2) → Fin 2) ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨0, ⋯⟩))

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x v w : E
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hf :
  ∀ (x_1 : (i : Fin 2) → E),
    Eq.{u_3 + 1} (α := F)
      ((iteratedFDerivWithin 𝕜 2 f s x : (a : (i : Fin 2) → E) → F) fun (i : Fin 2) ↦
          x_1 ((Fin.revPerm : (a : Fin 2) → Fin 2) i) :
        F)
      ((iteratedFDerivWithin 𝕜 2 f s x : (a : (i : Fin 2) → E) → F) x_1 : F)
⊢ ![v, w] ((fun (i : Fin (Nat.succ 1)) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 1))) =
    ![w, v] ((Fin.revPerm : (a : Fin 2) → Fin 2) ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨1, ⋯⟩))

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x v w : E
hf : IsSymmSndFDerivAt 𝕜 f x
simp :
  ∀ (hf : IsSymmSndFDerivWithinAt 𝕜 f univ x),
    Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 2 f univ x : (a : (i : Fin 2) → E) → F) ![v, w] : F)
      ((iteratedFDerivWithin 𝕜 2 f univ x : (a : (i : Fin 2) → E) → F) ![w, v] : F)
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDeriv 𝕜 2 f x : (a : (i : Fin 2) → E) → F) ![v, w] : F)
    ((iteratedFDeriv 𝕜 2 f x : (a : (i : Fin 2) → E) → F) ![w, v] : F)

Tactic:
simp only [← isSymmSndFDerivWithinAt_univ, ← iteratedFDerivWithin_univ] at *

Premises used: isSymmSndFDerivWithinAt_univ, iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x v w : E
hf : IsSymmSndFDerivWithinAt 𝕜 f univ x
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 2 f univ x : (a : (i : Fin 2) → E) → F) ![v, w] : F)
    ((iteratedFDerivWithin 𝕜 2 f univ x : (a : (i : Fin 2) → E) → F) ![w, v] : F)

Tactic:
hf.iteratedFDerivWithin_cons uniqueDiffOn_univ (mem_univ _)

Premises used: uniqueDiffOn_univ, Set.mem_univ, IsSymmSndFDerivWithinAt.iteratedFDerivWithin_cons
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x v w : E
hf : IsSymmSndFDerivWithinAt 𝕜 f univ x
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDerivWithin 𝕜 2 f univ x : (a : (i : Fin 2) → E) → F) ![v, w] : F)
    ((iteratedFDerivWithin 𝕜 2 f univ x : (a : (i : Fin 2) → E) → F) ![w, v] : F)

Tactic:
exact hf.iteratedFDerivWithin_cons uniqueDiffOn_univ (mem_univ _)

Premises used: uniqueDiffOn_univ, Set.mem_univ, IsSymmSndFDerivWithinAt.iteratedFDerivWithin_cons
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
rw :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin 2) ↦ E) F)
    (ContinuousMultilinearMap.domDomCongr Fin.revPerm (iteratedFDerivWithin 𝕜 2 f s x)) (iteratedFDerivWithin 𝕜 2 f s x)
⊢ IsSymmSndFDerivWithinAt 𝕜 f s x

Tactic:
rw [isSymmSndFDerivWithinAt_iff_iteratedFDerivWithin hs hx]

Premises used: isSymmSndFDerivWithinAt_iff_iteratedFDerivWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin 2) ↦ E) F)
    (ContinuousMultilinearMap.domDomCongr Fin.revPerm (iteratedFDerivWithin 𝕜 2 f s x)) (iteratedFDerivWithin 𝕜 2 f s x)

Tactic:
hf.domDomCongr_iteratedFDerivWithin hs hx _

Premises used: ContDiffWithinAt.domDomCongr_iteratedFDerivWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
s : Set E
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin 2) ↦ E) F)
    (ContinuousMultilinearMap.domDomCongr Fin.revPerm (iteratedFDerivWithin 𝕜 2 f s x)) (iteratedFDerivWithin 𝕜 2 f s x)

Tactic:
exact hf.domDomCongr_iteratedFDerivWithin hs hx _

Premises used: ContDiffWithinAt.domDomCongr_iteratedFDerivWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
hf : ContDiffAt 𝕜 ω f x
simp : ∀ (hf : ContDiffWithinAt 𝕜 ω f univ x), IsSymmSndFDerivWithinAt 𝕜 f univ x
⊢ IsSymmSndFDerivAt 𝕜 f x

Tactic:
simp only [← isSymmSndFDerivWithinAt_univ, ← contDiffWithinAt_univ] at hf ⊢

Premises used: isSymmSndFDerivWithinAt_univ, contDiffWithinAt_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 ω f univ x
⊢ IsSymmSndFDerivWithinAt 𝕜 f univ x

Tactic:
hf.isSymmSndFDerivWithinAt_of_omega uniqueDiffOn_univ (mem_univ _)

Premises used: uniqueDiffOn_univ, ContDiffWithinAt.isSymmSndFDerivWithinAt_of_omega, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 ω f univ x
⊢ IsSymmSndFDerivWithinAt 𝕜 f univ x

Tactic:
exact hf.isSymmSndFDerivWithinAt_of_omega uniqueDiffOn_univ (mem_univ _)

Premises used: uniqueDiffOn_univ, ContDiffWithinAt.isSymmSndFDerivWithinAt_of_omega, Set.mem_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
⊢ IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      f (x + h • v + h • w) - f (x + h • v) - HSMul.hSMul (β := F) h ((f' x : (a : E) → F) w : F) -
          HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
            ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2 / 2)
          ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2

Tactic:
IsLittleO.trans_isBigO
    (isLittleO_iff.2 fun ε εpos => ?_) (isBigO_const_mul_self ((‖v‖ + ‖w‖) * ‖w‖) _ _)

Premises used: Iff.mpr, Norm.norm, HMul.hMul, HAdd.hAdd, Asymptotics.isBigO_const_mul_self, Asymptotics.isLittleO_iff, Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
refine :
  ∀ (ε : ℝ) (εpos : 0 < ε),
    ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
      ‖f (x + x_1 • v + x_1 • w) - f (x + x_1 • v) - HSMul.hSMul (β := F) x_1 ((f' x : (a : E) → F) w : F) -
              HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2)
                ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
            HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2 / 2)
              ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F)‖ ≤
        ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * HPow.hPow (β := ℕ) x_1 2‖
⊢ IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      f (x + h • v + h • w) - f (x + h • v) - HSMul.hSMul (β := F) h ((f' x : (a : E) → F) w : F) -
          HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
            ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2 / 2)
          ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2

Tactic:
refine IsLittleO.trans_isBigO
    (isLittleO_iff.2 fun ε εpos => ?_) (isBigO_const_mul_self ((‖v‖ + ‖w‖) * ‖w‖) _ _)

Premises used: Iff.mpr, Norm.norm, HMul.hMul, HAdd.hAdd, Asymptotics.isBigO_const_mul_self, Asymptotics.isLittleO_iff, Asymptotics.IsLittleO.trans_isBigO
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
rw :
  ∀
    (hx :
      ∀ ⦃c : ℝ⦄,
        0 < c →
          ∀ᶠ (x_1 : E) in 𝓝[interior s] x,
            ‖HSub.hSub (β := E →L[ℝ] F) (f' x_1 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_1 - x) : E →L[ℝ] F)‖ ≤
              c * ‖x_1 - x‖)
    {v w : E} (hv : x + v ∈ interior s) (hw : x + v + w ∈ interior s) (ε : ℝ) (εpos : 0 < ε),
    ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
      ‖f (x + x_1 • v + x_1 • w) - f (x + x_1 • v) - HSMul.hSMul (β := F) x_1 ((f' x : (a : E) → F) w : F) -
              HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2)
                ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
            HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2 / 2)
              ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F)‖ ≤
        ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * HPow.hPow (β := ℕ) x_1 2‖
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    ‖f (x + x_1 • v + x_1 • w) - f (x + x_1 • v) - HSMul.hSMul (β := F) x_1 ((f' x : (a : E) → F) w : F) -
            HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2)
              ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
          HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2 / 2)
            ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F)‖ ≤
      ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * HPow.hPow (β := ℕ) x_1 2‖

Tactic:
rw [hasFDerivWithinAt_iff_isLittleO, isLittleO_iff] at hx

Premises used: hasFDerivWithinAt_iff_isLittleO, Asymptotics.isLittleO_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx :
  ∀ ⦃c : ℝ⦄,
    0 < c →
      ∀ᶠ (x_1 : E) in 𝓝[interior s] x,
        ‖HSub.hSub (β := E →L[ℝ] F) (f' x_1 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_1 - x) : E →L[ℝ] F)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
rcases :
  ∀ (δ : ℝ) (δpos : δ > 0)
    (sδ :
      Metric.ball x δ ∩ interior s ⊆
        {x_1 : E |
          (fun (x_2 : E) ↦
              ‖HSub.hSub (β := E →L[ℝ] F) (f' x_2 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_2 - x) : E →L[ℝ] F)‖ ≤
                ε * ‖x_2 - x‖)
            x_1}),
    ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
      ‖f (x + x_1 • v + x_1 • w) - f (x + x_1 • v) - HSMul.hSMul (β := F) x_1 ((f' x : (a : E) → F) w : F) -
              HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2)
                ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
            HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2 / 2)
              ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F)‖ ≤
        ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * HPow.hPow (β := ℕ) x_1 2‖
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    ‖f (x + x_1 • v + x_1 • w) - f (x + x_1 • v) - HSMul.hSMul (β := F) x_1 ((f' x : (a : E) → F) w : F) -
            HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2)
              ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
          HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2 / 2)
            ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F)‖ ≤
      ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * HPow.hPow (β := ℕ) x_1 2‖

Tactic:
rcases Metric.mem_nhdsWithin_iff.1 (hx εpos) with ⟨δ, δpos, sδ⟩

Premises used: Metric.mem_nhdsWithin_iff, Iff.mp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx :
  ∀ ⦃c : ℝ⦄,
    0 < c →
      ∀ᶠ (x_1 : E) in 𝓝[interior s] x,
        ‖HSub.hSub (β := E →L[ℝ] F) (f' x_1 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_1 - x) : E →L[ℝ] F)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ :
  Metric.ball x δ ∩ interior s ⊆
    {x_1 : E |
      (fun (x_2 : E) ↦
          ‖HSub.hSub (β := E →L[ℝ] F) (f' x_2 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_2 - x) : E →L[ℝ] F)‖ ≤
            ε * ‖x_2 - x‖)
        x_1}
⊢ Tendsto (fun (h : ℝ) ↦ h * (‖v‖ + ‖w‖)) (𝓝[>] 0) (𝓝 (0 * (‖v‖ + ‖w‖)))

Tactic:
have : Filter.Tendsto (fun h => h * (‖v‖ + ‖w‖)) (𝓝[>] (0 : ℝ)) (𝓝 (0 * (‖v‖ + ‖w‖))) :=
      (continuous_id.mul continuous_const).continuousWithinAt
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx :
  ∀ ⦃c : ℝ⦄,
    0 < c →
      ∀ᶠ (x_1 : E) in 𝓝[interior s] x,
        ‖HSub.hSub (β := E →L[ℝ] F) (f' x_1 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_1 - x) : E →L[ℝ] F)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ :
  Metric.ball x δ ∩ interior s ⊆
    {x_1 : E |
      (fun (x_2 : E) ↦
          ‖HSub.hSub (β := E →L[ℝ] F) (f' x_2 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_2 - x) : E →L[ℝ] F)‖ ≤
            ε * ‖x_2 - x‖)
        x_1}
this : Tendsto (fun (h : ℝ) ↦ h * (‖v‖ + ‖w‖)) (𝓝[>] 0) (𝓝 (0 * (‖v‖ + ‖w‖)))
apply : δ > 0 * (‖v‖ + ‖w‖)
⊢ ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ

Tactic:
apply (tendsto_order.1 this).2 δ

Premises used: tendsto_order, And.right, Iff.mp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx :
  ∀ ⦃c : ℝ⦄,
    0 < c →
      ∀ᶠ (x_1 : E) in 𝓝[interior s] x,
        ‖HSub.hSub (β := E →L[ℝ] F) (f' x_1 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_1 - x) : E →L[ℝ] F)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ :
  Metric.ball x δ ∩ interior s ⊆
    {x_1 : E |
      (fun (x_2 : E) ↦
          ‖HSub.hSub (β := E →L[ℝ] F) (f' x_2 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_2 - x) : E →L[ℝ] F)‖ ≤
            ε * ‖x_2 - x‖)
        x_1}
this : Tendsto (fun (h : ℝ) ↦ h * (‖v‖ + ‖w‖)) (𝓝[>] 0) (𝓝 (0 * (‖v‖ + ‖w‖)))
⊢ δ > 0 * (‖v‖ + ‖w‖)

Tactic:
simpa only [zero_mul] using δpos

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx :
  ∀ ⦃c : ℝ⦄,
    0 < c →
      ∀ᶠ (x_1 : E) in 𝓝[interior s] x,
        ‖HSub.hSub (β := E →L[ℝ] F) (f' x_1 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_1 - x) : E →L[ℝ] F)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ :
  Metric.ball x δ ∩ interior s ⊆
    {x_1 : E |
      (fun (x_2 : E) ↦
          ‖HSub.hSub (β := E →L[ℝ] F) (f' x_2 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_2 - x) : E →L[ℝ] F)‖ ≤
            ε * ‖x_2 - x‖)
        x_1}
⊢ ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ

Tactic:
have E1 : ∀ᶠ h in 𝓝[>] (0 : ℝ), h * (‖v‖ + ‖w‖) < δ := by
    have : Filter.Tendsto (fun h => h * (‖v‖ + ‖w‖)) (𝓝[>] (0 : ℝ)) (𝓝 (0 * (‖v‖ + ‖w‖))) :=
      (continuous_id.mul continuous_const).continuousWithinAt
    apply (tendsto_order.1 this).2 δ
    simpa only [zero_mul] using δpos
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx :
  ∀ ⦃c : ℝ⦄,
    0 < c →
      ∀ᶠ (x_1 : E) in 𝓝[interior s] x,
        ‖HSub.hSub (β := E →L[ℝ] F) (f' x_1 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_1 - x) : E →L[ℝ] F)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ :
  Metric.ball x δ ∩ interior s ⊆
    {x_1 : E |
      (fun (x_2 : E) ↦
          ‖HSub.hSub (β := E →L[ℝ] F) (f' x_2 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_2 - x) : E →L[ℝ] F)‖ ≤
            ε * ‖x_2 - x‖)
        x_1}
E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ
⊢ ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1

Tactic:
have E2 : ∀ᶠ h in 𝓝[>] (0 : ℝ), (h : ℝ) < 1 :=
    mem_nhdsWithin_of_mem_nhds <| Iio_mem_nhds zero_lt_one
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx :
  ∀ ⦃c : ℝ⦄,
    0 < c →
      ∀ᶠ (x_1 : E) in 𝓝[interior s] x,
        ‖HSub.hSub (β := E →L[ℝ] F) (f' x_1 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_1 - x) : E →L[ℝ] F)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ :
  Metric.ball x δ ∩ interior s ⊆
    {x_1 : E |
      (fun (x_2 : E) ↦
          ‖HSub.hSub (β := E →L[ℝ] F) (f' x_2 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_2 - x) : E →L[ℝ] F)‖ ≤
            ε * ‖x_2 - x‖)
        x_1}
E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ
E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1
h :
  ∀ (h : ℝ) (hδ : h * (‖v‖ + ‖w‖) < δ) (h_lt_1 : h < 1) (hpos : Membership.mem (γ := Set ℝ) (Ioi 0) h),
    ‖f (x + h • v + h • w) - f (x + h • v) - HSMul.hSMul (β := F) h ((f' x : (a : E) → F) w : F) -
            HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
              ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
          HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2 / 2)
            ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F)‖ ≤
      ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * HPow.hPow (β := ℕ) h 2‖
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[>] 0,
    ‖f (x + x_1 • v + x_1 • w) - f (x + x_1 • v) - HSMul.hSMul (β := F) x_1 ((f' x : (a : E) → F) w : F) -
            HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2)
              ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
          HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2 / 2)
            ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F)‖ ≤
      ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * HPow.hPow (β := ℕ) x_1 2‖

Tactic:
filter_upwards [E1, E2, self_mem_nhdsWithin] with h hδ h_lt_1 hpos

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx :
  ∀ ⦃c : ℝ⦄,
    0 < c →
      ∀ᶠ (x_1 : E) in 𝓝[interior s] x,
        ‖HSub.hSub (β := E →L[ℝ] F) (f' x_1 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_1 - x) : E →L[ℝ] F)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ :
  Metric.ball x δ ∩ interior s ⊆
    {x_1 : E |
      (fun (x_2 : E) ↦
          ‖HSub.hSub (β := E →L[ℝ] F) (f' x_2 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_2 - x) : E →L[ℝ] F)‖ ≤
            ε * ‖x_2 - x‖)
        x_1}
E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ
E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1
h : ℝ
hδ : h * (‖v‖ + ‖w‖) < δ
h_lt_1 : h < 1
hpos : Membership.mem (γ := Set ℝ) (Ioi 0) h
⊢ 0 < h

Tactic:
replace hpos : 0 < h := hpos