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 y : E
hy : y ∈ interior s
z : E
hz : z = (1 / 4) • (y - x)
A : ∀ (m : E), Tendsto (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m)) (𝓝 0) (𝓝 y)
B : ∀ (m : E), ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + HSMul.hSMul (α := ℝ) 4 (z + t • m) ∈ interior s
t : (m : E) → ℝ
ts : ∀ (m : E), x + HSMul.hSMul (α := ℝ) 4 (z + t m • m) ∈ interior s
tpos : ∀ (m : E), 0 < t m
⊢ ∀ (m : E),
    Eq.{u_2 + 1} (α := F) ((((f'' : (a : E) → E →L[ℝ] F) m : E →L[ℝ] F) : (a : E) → F) z : F)
      ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) m : F)

Tactic:
have C : ∀ m : E, f'' m z = f'' z m := by
    intro m
    have : f'' (z + t m • m) (z + t 0 • (0 : E)) = f'' (z + t 0 • (0 : E)) (z + t m • m) :=
      s_conv.second_derivative_within_at_symmetric_of_mem_interior hf xs hx (ts 0) (ts m)
    simp only [map_add, map_smul, add_right_inj, ContinuousLinearMap.add_apply, Pi.smul_apply,
      ContinuousLinearMap.coe_smul', add_zero, smul_zero] at this
    exact smul_right_injective F (tpos m).ne' this
-- 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 y : E
hy : y ∈ interior s
z : E
hz : z = (1 / 4) • (y - x)
A : ∀ (m : E), Tendsto (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m)) (𝓝 0) (𝓝 y)
B : ∀ (m : E), ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + HSMul.hSMul (α := ℝ) 4 (z + t • m) ∈ interior s
t : (m : E) → ℝ
ts : ∀ (m : E), x + HSMul.hSMul (α := ℝ) 4 (z + t m • m) ∈ interior s
tpos : ∀ (m : E), 0 < t m
C :
  ∀ (m : E),
    Eq.{u_2 + 1} (α := F) ((((f'' : (a : E) → E →L[ℝ] F) m : E →L[ℝ] F) : (a : E) → F) z : F)
      ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) m : F)
⊢ Eq.{u_2 + 1} (α := F) ((((f'' : (a : E) → E →L[ℝ] F) (z + t v • v) : E →L[ℝ] F) : (a : E) → F) (z + t w • w) : F)
    ((((f'' : (a : E) → E →L[ℝ] F) (z + t w • w) : E →L[ℝ] F) : (a : E) → F) (z + t v • v) : F)

Tactic:
have : f'' (z + t v • v) (z + t w • w) = f'' (z + t w • w) (z + t v • v) :=
    s_conv.second_derivative_within_at_symmetric_of_mem_interior hf xs hx (ts w) (ts v)
-- 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 y : E
hy : y ∈ interior s
z : E
hz : z = (1 / 4) • (y - x)
A : ∀ (m : E), Tendsto (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m)) (𝓝 0) (𝓝 y)
B : ∀ (m : E), ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + HSMul.hSMul (α := ℝ) 4 (z + t • m) ∈ interior s
t : (m : E) → ℝ
ts : ∀ (m : E), x + HSMul.hSMul (α := ℝ) 4 (z + t m • m) ∈ interior s
tpos : ∀ (m : E), 0 < t m
C :
  ∀ (m : E),
    Eq.{u_2 + 1} (α := F) ((((f'' : (a : E) → E →L[ℝ] F) m : E →L[ℝ] F) : (a : E) → F) z : F)
      ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) m : F)
this :
  Eq.{u_2 + 1} (α := F) ((((f'' : (a : E) → E →L[ℝ] F) (z + t v • v) : E →L[ℝ] F) : (a : E) → F) (z + t w • w) : F)
    ((((f'' : (a : E) → E →L[ℝ] F) (z + t w • w) : E →L[ℝ] F) : (a : E) → F) (z + t v • v) : F)
⊢ HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
        (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)) +
      t w •
        HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)
          (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)) =
    HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
        (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)) +
      t v •
        HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)
          (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F))

Tactic:
simp only [map_add, map_smul, ContinuousLinearMap.add_apply, Pi.smul_apply,
    ContinuousLinearMap.coe_smul', C] at this

Premises used: ContinuousLinearMap.coe_smul', map_add, ContinuousLinearMap.add_apply, map_smul, Pi.smul_apply
-- 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 y : E
hy : y ∈ interior s
z : E
hz : z = (1 / 4) • (y - x)
A : ∀ (m : E), Tendsto (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m)) (𝓝 0) (𝓝 y)
B : ∀ (m : E), ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + HSMul.hSMul (α := ℝ) 4 (z + t • m) ∈ interior s
t : (m : E) → ℝ
ts : ∀ (m : E), x + HSMul.hSMul (α := ℝ) 4 (z + t m • m) ∈ interior s
tpos : ∀ (m : E), 0 < t m
C :
  ∀ (m : E),
    Eq.{u_2 + 1} (α := F) ((((f'' : (a : E) → E →L[ℝ] F) m : E →L[ℝ] F) : (a : E) → F) z : F)
      ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) m : F)
this :
  HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
        (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)) +
      t w •
        HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)
          (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)) =
    HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
        (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)) +
      t v •
        HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)
          (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F))
⊢ HSMul.hSMul (β := F) (t v * t w) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) +
        (HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
            (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)) +
          t v •
            HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)
              (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F))) -
      (HSMul.hSMul (β := F) (t v * t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F) +
        (HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
            (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)) +
          t w •
            HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)
              (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)))) =
    0

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 y : E
hy : y ∈ interior s
z : E
hz : z = (1 / 4) • (y - x)
A : ∀ (m : E), Tendsto (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m)) (𝓝 0) (𝓝 y)
B : ∀ (m : E), ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + HSMul.hSMul (α := ℝ) 4 (z + t • m) ∈ interior s
t : (m : E) → ℝ
ts : ∀ (m : E), x + HSMul.hSMul (α := ℝ) 4 (z + t m • m) ∈ interior s
tpos : ∀ (m : E), 0 < t m
C :
  ∀ (m : E),
    Eq.{u_2 + 1} (α := F) ((((f'' : (a : E) → E →L[ℝ] F) m : E →L[ℝ] F) : (a : E) → F) z : F)
      ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) m : F)
this :
  HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
        (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)) +
      t w •
        HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)
          (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)) =
    HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
        (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)) +
      t v •
        HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)
          (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F))
a :
  HSMul.hSMul (β := F) (t v * t w) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) +
        (HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
            (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)) +
          t v •
            HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)
              (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F))) -
      (HSMul.hSMul (β := F) (t v * t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F) +
        (HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
            (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)) +
          t w •
            HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)
              (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)))) =
    0
⊢ HSMul.hSMul (β := F) (t v * t w) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) =
    HSMul.hSMul (β := F) (t v * t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)

Tactic:
linear_combination (norm := module) this
-- 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 y : E
hy : y ∈ interior s
z : E
hz : z = (1 / 4) • (y - x)
A : ∀ (m : E), Tendsto (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m)) (𝓝 0) (𝓝 y)
B : ∀ (m : E), ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + HSMul.hSMul (α := ℝ) 4 (z + t • m) ∈ interior s
t : (m : E) → ℝ
ts : ∀ (m : E), x + HSMul.hSMul (α := ℝ) 4 (z + t m • m) ∈ interior s
tpos : ∀ (m : E), 0 < t m
C :
  ∀ (m : E),
    Eq.{u_2 + 1} (α := F) ((((f'' : (a : E) → E →L[ℝ] F) m : E →L[ℝ] F) : (a : E) → F) z : F)
      ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) m : F)
this :
  HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
        (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)) +
      t w •
        HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)
          (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)) =
    HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
        (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)) +
      t v •
        HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)
          (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F))
⊢ HSMul.hSMul (β := F) (t v * t w) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) =
    HSMul.hSMul (β := F) (t v * t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)

Tactic:
have : (t v * t w) • (f'' v) w = (t v * t w) • (f'' w) v := by
    linear_combination (norm := module) this
-- 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 y : E
hy : y ∈ interior s
z : E
hz : z = (1 / 4) • (y - x)
A : ∀ (m : E), Tendsto (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m)) (𝓝 0) (𝓝 y)
B : ∀ (m : E), ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + HSMul.hSMul (α := ℝ) 4 (z + t • m) ∈ interior s
t : (m : E) → ℝ
ts : ∀ (m : E), x + HSMul.hSMul (α := ℝ) 4 (z + t m • m) ∈ interior s
tpos : ∀ (m : E), 0 < t m
C :
  ∀ (m : E),
    Eq.{u_2 + 1} (α := F) ((((f'' : (a : E) → E →L[ℝ] F) m : E →L[ℝ] F) : (a : E) → F) z : F)
      ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) m : F)
this_1 :
  HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
        (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)) +
      t w •
        HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)
          (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)) =
    HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
        (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)) +
      t v •
        HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)
          (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F))
this :
  HSMul.hSMul (β := F) (t v * t w) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) =
    HSMul.hSMul (β := F) (t v * t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
apply : t v * t w ≠ 0
⊢ Eq.{u_2 + 1} (α := F) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)
    ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)

Tactic:
apply smul_right_injective F _ this

Premises used: smul_right_injective
-- 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 y : E
hy : y ∈ interior s
z : E
hz : z = (1 / 4) • (y - x)
A : ∀ (m : E), Tendsto (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m)) (𝓝 0) (𝓝 y)
B : ∀ (m : E), ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + HSMul.hSMul (α := ℝ) 4 (z + t • m) ∈ interior s
t : (m : E) → ℝ
ts : ∀ (m : E), x + HSMul.hSMul (α := ℝ) 4 (z + t m • m) ∈ interior s
tpos : ∀ (m : E), 0 < t m
C :
  ∀ (m : E),
    Eq.{u_2 + 1} (α := F) ((((f'' : (a : E) → E →L[ℝ] F) m : E →L[ℝ] F) : (a : E) → F) z : F)
      ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) m : F)
this_1 :
  HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
        (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)) +
      t w •
        HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)
          (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)) =
    HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
        (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)) +
      t v •
        HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)
          (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F))
this :
  HSMul.hSMul (β := F) (t v * t w) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) =
    HSMul.hSMul (β := F) (t v * t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
⊢ t v * t w ≠ 0

Tactic:
simp [(tpos v).ne', (tpos w).ne']

Premises used: LT.lt.ne'
-- 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
x : E
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
rcases :
  ∀ (ε : ℝ) (εpos : ε > 0) (hε : Metric.ball x ε ⊆ {x : E | (fun (y : E) ↦ HasFDerivAt f (f' y) y) x}),
    Eq.{u_2 + 1} (α := F) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)
      ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
⊢ Eq.{u_2 + 1} (α := F) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)
    ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)

Tactic:
rcases Metric.mem_nhds_iff.1 hf with ⟨ε, εpos, hε⟩

Premises used: Metric.mem_nhds_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
x : E
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ {x : E | (fun (y : E) ↦ HasFDerivAt f (f' y) y) x}
rwa : (Metric.ball x ε).Nonempty
rwa₁ rwa₂ rwa₃ rwa₄ : 0 < ε
⊢ (interior (Metric.ball x ε)).Nonempty

Tactic:
rwa [Metric.isOpen_ball.interior_eq, Metric.nonempty_ball]

Premises used: Metric.nonempty_ball, Metric.isOpen_ball, IsOpen.interior_eq
-- 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
x : E
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ {x : E | (fun (y : E) ↦ HasFDerivAt f (f' y) y) x}
⊢ (interior (Metric.ball x ε)).Nonempty

Tactic:
have A : (interior (Metric.ball x ε)).Nonempty := by
    rwa [Metric.isOpen_ball.interior_eq, Metric.nonempty_ball]
-- 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
x : E
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ {x : E | (fun (y : E) ↦ HasFDerivAt f (f' y) y) x}
A : (interior (Metric.ball x ε)).Nonempty
⊢ Eq.{u_2 + 1} (α := F) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)
    ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)

Tactic:
Convex.second_derivative_within_at_symmetric (convex_ball x ε) A
      (fun y hy => hε (interior_subset hy)) (Metric.mem_ball_self εpos) hx.hasFDerivWithinAt v w

Premises used: interior_subset, HasFDerivAt.hasFDerivWithinAt, Convex.second_derivative_within_at_symmetric, Metric.mem_ball_self, convex_ball
-- 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
x : E
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ {x : E | (fun (y : E) ↦ HasFDerivAt f (f' y) y) x}
A : (interior (Metric.ball x ε)).Nonempty
⊢ Eq.{u_2 + 1} (α := F) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)
    ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)

Tactic:
exact
    Convex.second_derivative_within_at_symmetric (convex_ball x ε) A
      (fun y hy => hε (interior_subset hy)) (Metric.mem_ball_self εpos) hx.hasFDerivWithinAt v w

Premises used: interior_subset, HasFDerivAt.hasFDerivWithinAt, Convex.second_derivative_within_at_symmetric, Metric.mem_ball_self, convex_ball
-- 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
inst_5 : IsRCLikeNormedField 𝕜
f' : E → E →L[𝕜] F
x : E
f'' : E →L[𝕜] E →L[𝕜] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
h : LinearMap.CompatibleSMul E F ℝ 𝕜 := ⋯
h_1 : LinearMap.CompatibleSMul E (E →L[𝕜] F) ℝ 𝕜 := ⋯
f'R : E → E →L[ℝ] F := fun (x : E) ↦ ContinuousLinearMap.restrictScalars ℝ (f' x)
f''R : E →L[ℝ] E →L[ℝ] F := ContinuousLinearMap.bilinearRestrictScalars ℝ f''
y : E
hy : HasFDerivAt f (f' y) y
⊢ HasFDerivAt f (f'R y) y

Tactic:
HasFDerivAt.restrictScalars ℝ hy

Premises used: Real, HasFDerivAt.restrictScalars
-- 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
inst_5 : IsRCLikeNormedField 𝕜
f' : E → E →L[𝕜] F
x : E
f'' : E →L[𝕜] E →L[𝕜] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
h_1 : LinearMap.CompatibleSMul E F ℝ 𝕜 := ⋯
h_2 : LinearMap.CompatibleSMul E (E →L[𝕜] F) ℝ 𝕜 := ⋯
f'R : E → E →L[ℝ] F := fun (x : E) ↦ ContinuousLinearMap.restrictScalars ℝ (f' x)
f''R : E →L[ℝ] E →L[ℝ] F := ContinuousLinearMap.bilinearRestrictScalars ℝ f''
h :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x : E |
        Membership.mem (γ := Set E) {x : E | (fun (y : E) ↦ HasFDerivAt f (f' y) y) x} x →
          Membership.mem (γ := Set E) {x : E | (fun (y : E) ↦ HasFDerivAt f (f'R y) y) x} x}
      a
h₁ h₂ : ∀ (y : E) (hy : HasFDerivAt f (f' y) y), HasFDerivAt f (f'R y) y
⊢ ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f'R y) y

Tactic:
filter_upwards [hf] with y hy using HasFDerivAt.restrictScalars ℝ hy