awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  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
this :
  IsBigO (E := ℝ) (F := ℝ) (𝓝[>] 0) (fun (h : ℝ) ↦ 1 / HPow.hPow (β := ℕ) h 2) fun (h : ℝ) ↦ 1 / HPow.hPow (β := ℕ) h 2
C :
  IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
    (fun (x : ℝ) ↦
      (1 / HPow.hPow (β := ℕ) x 2) •
        HPow.hPow (β := ℕ) x 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 / HPow.hPow (β := ℕ) x 2) • HPow.hPow (β := ℕ) x 2
⊢ EventuallyEq (β := ℝ) (𝓝[>] 0) (fun (x : ℝ) ↦ (1 / HPow.hPow (β := ℕ) x 2) • HPow.hPow (β := ℕ) x 2) fun (x : ℝ) ↦ 1
have h : ∀ (h : ℝ) (hpos : 0 < h), (1 / HPow.hPow (β := ℕ) h 2) • HPow.hPow (β := ℕ) h 2 = 1
Tactic: filter_upwards [self_mem_nhdsWithin] with h (hpos : 0 < h)
-- 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 :
  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
⊢ Eq.{u_2 + 1} (α := 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)
have B : IsLittleO.{0, u_2, 0} (E := F) (F := ℝ) (𝓝[>] 0)
  (fun (x : ℝ) ↦
    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
Tactic: have B : (fun _ : ℝ => f'' w v - f'' v w) =o[𝓝[>] 0] fun _ => (1 : ℝ) := by
    have : (fun h : ℝ => 1 / h ^ 2) =O[𝓝[>] 0] fun h => 1 / h ^ 2 := isBigO_refl _ _
    have C := this.smul_isLittleO A
    apply C.congr' _ _
    · filter_upwards [self_mem_nhdsWithin]
      intro h (hpos : 0 < h)
      match_scalars <;> field
    · filter_upwards [self_mem_nhdsWithin] with h (hpos : 0 < h)
      simp [field]
-- 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
hne : (interior s).Nonempty
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
⊢ 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)
have rcases : ∀ (y : E) (hy : y ∈ interior s),
  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 hne with ⟨y, hy⟩
Cleared hypotheses: hne
-- 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 y : E
hy : y ∈ interior s
⊢ 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)
have obtain : ∀ (z : E) (hz : z = (1 / 4) • (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)
Tactic: obtain ⟨z, hz⟩ : ∃ z, z = ((1 : ℝ) / 4) • (y - x) := ⟨((1 : ℝ) / 4) • (y - x), rfl⟩
-- 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 y : E
hy : y ∈ interior s
z : E
hz : z = (1 / 4) • (y - x)
m : E
⊢ Tendsto (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m)) (𝓝 0) (𝓝 y)
have this : x + HSMul.hSMul (α := ℝ) 4 (z + HSMul.hSMul (α := ℝ) 0 m) = y
Tactic: have : x + (4 : ℝ) • (z + (0 : ℝ) • m) = y := by simp [hz]
-- 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 y : E
hy : y ∈ interior s
z : E
hz : z = (1 / 4) • (y - x)
m : E
this : x + HSMul.hSMul (α := ℝ) 4 (z + HSMul.hSMul (α := ℝ) 0 m) = y
⊢ Tendsto (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m)) (𝓝 0) (𝓝 y)
have rw : Tendsto (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m)) (𝓝 0)
  (𝓝 (x + HSMul.hSMul (α := ℝ) 4 (z + HSMul.hSMul (α := ℝ) 0 m)))
Tactic: rw [← this]
-- 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 y : E
hy : y ∈ interior s
z : E
hz : z = (1 / 4) • (y - x)
m : E
this : x + HSMul.hSMul (α := ℝ) 4 (z + HSMul.hSMul (α := ℝ) 0 m) = y
⊢ Tendsto (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m)) (𝓝 0)
    (𝓝 (x + HSMul.hSMul (α := ℝ) 4 (z + HSMul.hSMul (α := ℝ) 0 m)))
have refine : Tendsto (fun (t : ℝ) ↦ t • m) (𝓝 0) (𝓝 (HSMul.hSMul (α := ℝ) 0 m))
Tactic: refine tendsto_const_nhds.add <| tendsto_const_nhds.smul <| tendsto_const_nhds.add ?_
-- 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 y : E
hy : y ∈ interior s
z : E
hz : z = (1 / 4) • (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)
have A : ∀ (m : E), Tendsto (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m)) (𝓝 0) (𝓝 y)
Tactic: have A : ∀ m : E, Filter.Tendsto (fun t : ℝ => x + (4 : ℝ) • (z + t • m)) (𝓝 0) (𝓝 y) := by
    intro m
    have : x + (4 : ℝ) • (z + (0 : ℝ) • m) = y := by simp [hz]
    rw [← this]
    refine tendsto_const_nhds.add <| tendsto_const_nhds.smul <| tendsto_const_nhds.add ?_
    exact continuousAt_id.smul continuousAt_const
-- 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 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)
m : E
⊢ ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + HSMul.hSMul (α := ℝ) 4 (z + t • m) ∈ interior s
have a : Membership.mem (γ := Filter ℝ) (𝓝 0) {x_1 : ℝ | (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m) ∈ interior s) x_1}
Tactic: apply nhdsWithin_le_nhds
-- 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 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)
m : E
⊢ Membership.mem (γ := Filter ℝ) (𝓝 0)
    {x_1 : ℝ | (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m) ∈ interior s) x_1}
have a : interior s ∈ 𝓝 y
Tactic: apply A m
-- 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 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)
m : E
⊢ interior s ∈ 𝓝 y
have a : ∀ (hy : s ∈ 𝓝 y) (z : E) (hz : z = (1 / 4) • (y - x))
  (A : ∀ (m : E), Tendsto (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m)) (𝓝 0) (𝓝 y)) (m : E), interior s ∈ 𝓝 y
Tactic: rw [mem_interior_iff_mem_nhds] at hy
Cleared hypotheses: hy, z, hz, A, m
-- 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 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)
⊢ 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)
have B : ∀ (m : E), ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + HSMul.hSMul (α := ℝ) 4 (z + t • m) ∈ interior s
Tactic: have B : ∀ m : E, ∀ᶠ t in 𝓝[>] (0 : ℝ), x + (4 : ℝ) • (z + t • m) ∈ interior s := by
    intro m
    apply nhdsWithin_le_nhds
    apply A m
    rw [mem_interior_iff_mem_nhds] at hy
    exact interior_mem_nhds.2 hy
-- 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 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
⊢ 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)
have choose : ∀ (t : (m : E) → ℝ) (ts : ∀ (m : E), x + HSMul.hSMul (α := ℝ) 4 (z + t m • m) ∈ interior s) (tpos : ∀ (m : E), 0 < t m),
  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: choose t ts tpos using fun m => ((B m).and self_mem_nhdsWithin).exists
-- 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 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)
have this : Eq.{u_2 + 1} (α := F)
  ((((f'' : (a : E) → E →L[ℝ] F) (z + t m • m) : E →L[ℝ] F) : (a : E) → F) (z + HSMul.hSMul (β := E) (t 0) 0) : F)
  ((((f'' : (a : E) → E →L[ℝ] F) (z + HSMul.hSMul (β := E) (t 0) 0) : E →L[ℝ] F) : (a : E) → F) (z + t m • m) : F)
Tactic: 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)
-- 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 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
this :
  Eq.{u_2 + 1} (α := F)
    ((((f'' : (a : E) → E →L[ℝ] F) (z + t m • m) : E →L[ℝ] F) : (a : E) → F) (z + HSMul.hSMul (β := E) (t 0) 0) : F)
    ((((f'' : (a : E) → E →L[ℝ] F) (z + HSMul.hSMul (β := E) (t 0) 0) : E →L[ℝ] F) : (a : E) → F) (z + t m • m) : F)
⊢ 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)
have this₁ : HSMul.hSMul (β := F) (t m) ((((f'' : (a : E) → E →L[ℝ] F) m : E →L[ℝ] F) : (a : E) → F) z : F) =
  HSMul.hSMul (β := F) (t m) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) m : F)
Tactic: simp only [map_add, map_smul, add_right_inj, ContinuousLinearMap.add_apply, Pi.smul_apply,
      ContinuousLinearMap.coe_smul', add_zero, smul_zero] at this
Cleared hypotheses: this
-- 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 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
⊢ 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)
have 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)
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
-- 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 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) v : E →L[ℝ] F) : (a : E) → F) w : F)
    ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
have 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)
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)
-- 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 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)
⊢ 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)
have 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))
Tactic: simp only [map_add, map_smul, ContinuousLinearMap.add_apply, Pi.smul_apply,
    ContinuousLinearMap.coe_smul', C] at this
Cleared hypotheses: this