awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
h2v : x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
h2w : x + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h : x + (v + w) = x + (1 / 2) • (x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w - x)
⊢ x + (v + w) ∈ interior s

Tactic:
convert! s_conv.add_smul_sub_mem_interior xs h2v2w A using 1

Premises used: Convex.add_smul_sub_mem_interior
-- 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
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
h2v : x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
h2w : x + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
⊢ x + (v + w) = x + (1 / 2) • (x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w - x)

Tactic:
module
-- 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
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
h2v : x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
h2w : x + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
⊢ x + (v + w) ∈ interior s

Tactic:
have hvw : x + (v + w) ∈ interior s := by
    convert! s_conv.add_smul_sub_mem_interior xs h2v2w A using 1
    module
-- 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
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
h2v : x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
h2w : x + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
hvw : x + (v + w) ∈ interior s
⊢ x + HSMul.hSMul (α := ℝ) 2 v +
      (1 / 2) • (x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w - (x + HSMul.hSMul (α := ℝ) 2 v)) ∈
    interior s

Tactic:
s_conv.interior.add_smul_sub_mem h2v h2v2w B

Premises used: Convex.interior, Convex.add_smul_sub_mem
-- 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
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
h2v : x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
h2w : x + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
hvw : x + (v + w) ∈ interior s
h :
  x + (HSMul.hSMul (α := ℕ) 2 v + w) =
    x + HSMul.hSMul (α := ℝ) 2 v +
      (1 / 2) • (x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w - (x + HSMul.hSMul (α := ℝ) 2 v))
⊢ x + (HSMul.hSMul (α := ℕ) 2 v + w) ∈ interior s

Tactic:
convert! s_conv.interior.add_smul_sub_mem h2v h2v2w B using 1

Premises used: Convex.interior, Convex.add_smul_sub_mem
-- 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
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
h2v : x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
h2w : x + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
hvw : x + (v + w) ∈ interior s
⊢ x + (HSMul.hSMul (α := ℕ) 2 v + w) =
    x + HSMul.hSMul (α := ℝ) 2 v +
      (1 / 2) • (x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w - (x + HSMul.hSMul (α := ℝ) 2 v))

Tactic:
module
-- 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
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
h2v : x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
h2w : x + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
hvw : x + (v + w) ∈ interior s
⊢ x + (HSMul.hSMul (α := ℕ) 2 v + w) ∈ interior s

Tactic:
have h2vw : x + (2 • v + w) ∈ interior s := by
    convert! s_conv.interior.add_smul_sub_mem h2v h2v2w B using 1
    module
-- 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
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
h2v : x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
h2w : x + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
hvw : x + (v + w) ∈ interior s
h2vw : x + (HSMul.hSMul (α := ℕ) 2 v + w) ∈ interior s
⊢ x + HSMul.hSMul (α := ℝ) 2 w +
      (1 / 2) • (x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w - (x + HSMul.hSMul (α := ℝ) 2 w)) ∈
    interior s

Tactic:
s_conv.interior.add_smul_sub_mem h2w h2v2w B

Premises used: Convex.interior, Convex.add_smul_sub_mem
-- 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
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
h2v : x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
h2w : x + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
hvw : x + (v + w) ∈ interior s
h2vw : x + (HSMul.hSMul (α := ℕ) 2 v + w) ∈ interior s
h :
  x + (v + w) + w =
    x + HSMul.hSMul (α := ℝ) 2 w +
      (1 / 2) • (x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w - (x + HSMul.hSMul (α := ℝ) 2 w))
⊢ x + (v + w) + w ∈ interior s

Tactic:
convert! s_conv.interior.add_smul_sub_mem h2w h2v2w B using 1

Premises used: Convex.interior, Convex.add_smul_sub_mem
-- 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
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
h2v : x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
h2w : x + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
hvw : x + (v + w) ∈ interior s
h2vw : x + (HSMul.hSMul (α := ℕ) 2 v + w) ∈ interior s
⊢ x + (v + w) + w =
    x + HSMul.hSMul (α := ℝ) 2 w +
      (1 / 2) • (x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w - (x + HSMul.hSMul (α := ℝ) 2 w))

Tactic:
module
-- 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
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
h2v : x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
h2w : x + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
hvw : x + (v + w) ∈ interior s
h2vw : x + (HSMul.hSMul (α := ℕ) 2 v + w) ∈ interior s
⊢ x + (v + w) + w ∈ interior s

Tactic:
have hvww : x + (v + w) + w ∈ interior s := by
    convert! s_conv.interior.add_smul_sub_mem h2w h2v2w B using 1
    module
-- 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
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
h2v : x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
h2w : x + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
hvw : x + (v + w) ∈ interior s
h2vw : x + (HSMul.hSMul (α := ℕ) 2 v + w) ∈ interior s
hvww : x + (v + w) + w ∈ interior s
⊢ IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      f (x + h • (HSMul.hSMul (α := ℕ) 2 v + w) + h • w) - f (x + h • (HSMul.hSMul (α := ℕ) 2 v + w)) -
            HSMul.hSMul (β := F) h ((f' x : (a : E) → F) w : F) -
          HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
            ((((f'' : (a : E) → E →L[ℝ] F) (HSMul.hSMul (α := ℕ) 2 v + w) : 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:
have TA1 := s_conv.taylor_approx_two_segment hf xs hx h2vw h2vww
-- 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
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
h2v : x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
h2w : x + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
hvw : x + (v + w) ∈ interior s
h2vw : x + (HSMul.hSMul (α := ℕ) 2 v + w) ∈ interior s
hvww : x + (v + w) + w ∈ interior s
TA1 :
  IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      f (x + h • (HSMul.hSMul (α := ℕ) 2 v + w) + h • w) - f (x + h • (HSMul.hSMul (α := ℕ) 2 v + w)) -
            HSMul.hSMul (β := F) h ((f' x : (a : E) → F) w : F) -
          HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
            ((((f'' : (a : E) → E →L[ℝ] F) (HSMul.hSMul (α := ℕ) 2 v + w) : 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
⊢ IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      f (x + h • (v + w) + h • w) - f (x + h • (v + w)) - 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 + w) : 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:
have TA2 := s_conv.taylor_approx_two_segment hf xs hx hvw hvww
-- 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
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
h2v : x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
h2w : x + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
hvw : x + (v + w) ∈ interior s
h2vw : x + (HSMul.hSMul (α := ℕ) 2 v + w) ∈ interior s
hvww : x + (v + w) + w ∈ interior s
TA1 :
  IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      f (x + h • (HSMul.hSMul (α := ℕ) 2 v + w) + h • w) - f (x + h • (HSMul.hSMul (α := ℕ) 2 v + w)) -
            HSMul.hSMul (β := F) h ((f' x : (a : E) → F) w : F) -
          HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
            ((((f'' : (a : E) → E →L[ℝ] F) (HSMul.hSMul (α := ℕ) 2 v + w) : 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
TA2 :
  IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      f (x + h • (v + w) + h • w) - f (x + h • (v + w)) - 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 + w) : 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
⊢ IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (x_1 : ℝ) ↦
      f (x + x_1 • (HSMul.hSMul (α := ℕ) 2 v + w) + x_1 • w) - f (x + x_1 • (HSMul.hSMul (α := ℕ) 2 v + w)) -
              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) (HSMul.hSMul (α := ℕ) 2 v + w) : 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) -
        (f (x + x_1 • (v + w) + x_1 • w) - f (x + x_1 • (v + w)) -
              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 + w) : 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)))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2

Tactic:
TA1.sub TA2

Premises used: Asymptotics.IsLittleO.sub
-- 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
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
⊢ IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (x_1 : ℝ) ↦
      f (x + x_1 • (HSMul.hSMul (α := ℕ) 2 v + HSMul.hSMul (α := ℕ) 2 w)) + f (x + x_1 • (v + w)) -
              f (x + x_1 • (HSMul.hSMul (α := ℕ) 2 v + w)) -
            f (x + x_1 • (v + HSMul.hSMul (α := ℕ) 2 w)) -
          HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2)
            ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
        (f (x + x_1 • (HSMul.hSMul (α := ℕ) 2 w + HSMul.hSMul (α := ℕ) 2 v)) + f (x + x_1 • (w + v)) -
              f (x + x_1 • (HSMul.hSMul (α := ℕ) 2 w + v)) -
            f (x + x_1 • (w + HSMul.hSMul (α := ℕ) 2 v)) -
          HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2)
            ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2

Tactic:
(s_conv.isLittleO_alternate_sum_square hf xs hx h4v h4w).sub
        (s_conv.isLittleO_alternate_sum_square hf xs hx h4w h4v)

Premises used: Convex.isLittleO_alternate_sum_square, Asymptotics.IsLittleO.sub
-- 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
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
h :
  Eq.{u_2 + 1} (α := ℝ → F)
    (fun (h : ℝ) ↦
      HPow.hPow (β := ℕ) h 2 •
        HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (x_1 : ℝ) ↦
    f (x + x_1 • (HSMul.hSMul (α := ℕ) 2 v + HSMul.hSMul (α := ℕ) 2 w)) + f (x + x_1 • (v + w)) -
            f (x + x_1 • (HSMul.hSMul (α := ℕ) 2 v + w)) -
          f (x + x_1 • (v + HSMul.hSMul (α := ℕ) 2 w)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
      (f (x + x_1 • (HSMul.hSMul (α := ℕ) 2 w + HSMul.hSMul (α := ℕ) 2 v)) + f (x + x_1 • (w + v)) -
            f (x + x_1 • (HSMul.hSMul (α := ℕ) 2 w + v)) -
          f (x + x_1 • (w + HSMul.hSMul (α := ℕ) 2 v)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) x_1 2)
          ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F))
⊢ IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      HPow.hPow (β := ℕ) h 2 •
        HSub.hSub (α := F) (β := F) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2

Tactic:
convert!
      (s_conv.isLittleO_alternate_sum_square hf xs hx h4v h4w).sub
        (s_conv.isLittleO_alternate_sum_square hf xs hx h4w h4v) using 1

Premises used: Convex.isLittleO_alternate_sum_square, Asymptotics.IsLittleO.sub