awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
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)
⊢ IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      f (x + h • (HSMul.hSMul (α := ℕ) 2 v + HSMul.hSMul (α := ℕ) 2 w)) + f (x + h • (v + w)) -
            f (x + h • (HSMul.hSMul (α := ℕ) 2 v + w)) -
          f (x + h • (v + HSMul.hSMul (α := ℕ) 2 w)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
have B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
Tactic: have B : (1 : ℝ) / 2 ∈ Icc (0 : ℝ) 1 := ⟨by simp, by norm_num⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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)
⊢ x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
have h : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w =
  x + HSMul.hSMul (α := ℝ) 4 v + (1 / 2) • (x + HSMul.hSMul (α := ℝ) 4 w - (x + HSMul.hSMul (α := ℝ) 4 v))
Tactic: convert! s_conv.interior.add_smul_sub_mem h4v h4w B using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
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)
⊢ IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      f (x + h • (HSMul.hSMul (α := ℕ) 2 v + HSMul.hSMul (α := ℕ) 2 w)) + f (x + h • (v + w)) -
            f (x + h • (HSMul.hSMul (α := ℕ) 2 v + w)) -
          f (x + h • (v + HSMul.hSMul (α := ℕ) 2 w)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
have h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
Tactic: have h2v2w : x + (2 : ℝ) • v + (2 : ℝ) • w ∈ interior s := by
    convert! s_conv.interior.add_smul_sub_mem h4v h4w B using 1
    module
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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
⊢ x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
have h : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w = x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w
Tactic: convert! h2v2w using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
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
⊢ IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      f (x + h • (HSMul.hSMul (α := ℕ) 2 v + HSMul.hSMul (α := ℕ) 2 w)) + f (x + h • (v + w)) -
            f (x + h • (HSMul.hSMul (α := ℕ) 2 v + w)) -
          f (x + h • (v + HSMul.hSMul (α := ℕ) 2 w)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
have h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
Tactic: have h2vww : x + (2 • v + w) + w ∈ interior s := by
    convert! h2v2w using 1
    module
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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
⊢ x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
have h : x + HSMul.hSMul (α := ℝ) 2 v = x + (1 / 2) • (x + HSMul.hSMul (α := ℝ) 4 v - x)
Tactic: convert! s_conv.add_smul_sub_mem_interior xs h4v A using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
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
⊢ IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      f (x + h • (HSMul.hSMul (α := ℕ) 2 v + HSMul.hSMul (α := ℕ) 2 w)) + f (x + h • (v + w)) -
            f (x + h • (HSMul.hSMul (α := ℕ) 2 v + w)) -
          f (x + h • (v + HSMul.hSMul (α := ℕ) 2 w)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
have h2v : x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
Tactic: have h2v : x + (2 : ℝ) • v ∈ interior s := by
    convert! s_conv.add_smul_sub_mem_interior xs h4v A using 1
    module
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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
⊢ x + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
have h : x + HSMul.hSMul (α := ℝ) 2 w = x + (1 / 2) • (x + HSMul.hSMul (α := ℝ) 4 w - x)
Tactic: convert! s_conv.add_smul_sub_mem_interior xs h4w A using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
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
⊢ IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      f (x + h • (HSMul.hSMul (α := ℕ) 2 v + HSMul.hSMul (α := ℕ) 2 w)) + f (x + h • (v + w)) -
            f (x + h • (HSMul.hSMul (α := ℕ) 2 v + w)) -
          f (x + h • (v + HSMul.hSMul (α := ℕ) 2 w)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
have h2w : x + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
Tactic: have h2w : x + (2 : ℝ) • w ∈ interior s := by
    convert! s_conv.add_smul_sub_mem_interior xs h4w A using 1
    module
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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
have h : x + (v + w) = x + (1 / 2) • (x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w - x)
Tactic: convert! s_conv.add_smul_sub_mem_interior xs h2v2w A using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
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
⊢ IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      f (x + h • (HSMul.hSMul (α := ℕ) 2 v + HSMul.hSMul (α := ℕ) 2 w)) + f (x + h • (v + w)) -
            f (x + h • (HSMul.hSMul (α := ℕ) 2 v + w)) -
          f (x + h • (v + HSMul.hSMul (α := ℕ) 2 w)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
have hvw : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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
have 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))
Tactic: convert! s_conv.interior.add_smul_sub_mem h2v h2v2w B using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
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
⊢ IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      f (x + h • (HSMul.hSMul (α := ℕ) 2 v + HSMul.hSMul (α := ℕ) 2 w)) + f (x + h • (v + w)) -
            f (x + h • (HSMul.hSMul (α := ℕ) 2 v + w)) -
          f (x + h • (v + HSMul.hSMul (α := ℕ) 2 w)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
have h2vw : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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
have 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))
Tactic: convert! s_conv.interior.add_smul_sub_mem h2w h2v2w B using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
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
⊢ IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (h : ℝ) ↦
      f (x + h • (HSMul.hSMul (α := ℕ) 2 v + HSMul.hSMul (α := ℕ) 2 w)) + f (x + h • (v + w)) -
            f (x + h • (HSMul.hSMul (α := ℕ) 2 v + w)) -
          f (x + h • (v + HSMul.hSMul (α := ℕ) 2 w)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
have hvww : 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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
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 + HSMul.hSMul (α := ℕ) 2 w)) + f (x + h • (v + w)) -
            f (x + h • (HSMul.hSMul (α := ℕ) 2 v + w)) -
          f (x + h • (v + HSMul.hSMul (α := ℕ) 2 w)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
have 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
Tactic: have TA1 := s_conv.taylor_approx_two_segment hf xs hx h2vw h2vww
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
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 • (HSMul.hSMul (α := ℕ) 2 v + HSMul.hSMul (α := ℕ) 2 w)) + f (x + h • (v + w)) -
            f (x + h • (HSMul.hSMul (α := ℕ) 2 v + w)) -
          f (x + h • (v + HSMul.hSMul (α := ℕ) 2 w)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F))
    fun (h : ℝ) ↦ HPow.hPow (β := ℕ) h 2
have 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
Tactic: have TA2 := s_conv.taylor_approx_two_segment hf xs hx hvw hvww