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 :
  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
h : ℝ
hpos : 0 < h
⊢ (1 / HPow.hPow (β := ℕ) h 2) • HPow.hPow (β := ℕ) h 2 = 1

Tactic:
simp [field]
-- 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 :
  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
⊢ 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]
-- 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 :
  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
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
⊢ 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)

Tactic:
simpa only [sub_eq_zero] using isLittleO_const_const_iff.1 B

Premises used: sub_eq_zero, Iff.mp, Asymptotics.isLittleO_const_const_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
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
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)
⊢ 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⟩
-- 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), z = (1 / 4) • (y - x)

Tactic:
⟨((1 : ℝ) / 4) • (y - x), rfl⟩

Premises used: HSub.hSub, HDiv.hDiv, Exists.intro, HSMul.hSMul, OfNat.ofNat, rfl
-- 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
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)
⊢ 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⟩

Premises used: HSub.hSub, HDiv.hDiv, OfNat.ofNat
-- 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)
m : E
⊢ x + HSMul.hSMul (α := ℝ) 4 (z + HSMul.hSMul (α := ℝ) 0 m) = y

Tactic:
simp [hz]
-- 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)
m : E
⊢ x + HSMul.hSMul (α := ℝ) 4 (z + HSMul.hSMul (α := ℝ) 0 m) = y

Tactic:
have : x + (4 : ℝ) • (z + (0 : ℝ) • m) = y := by simp [hz]
-- 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)
m : E
this : x + HSMul.hSMul (α := ℝ) 4 (z + HSMul.hSMul (α := ℝ) 0 m) = y
rw :
  Tendsto (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m)) (𝓝 0)
    (𝓝 (x + HSMul.hSMul (α := ℝ) 4 (z + HSMul.hSMul (α := ℝ) 0 m)))
⊢ Tendsto (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m)) (𝓝 0) (𝓝 y)

Tactic:
rw [← 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)
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)))

Tactic:
tendsto_const_nhds.add <| tendsto_const_nhds.smul <| tendsto_const_nhds.add ?_

Premises used: tendsto_const_nhds, Filter.Tendsto.smul, Filter.Tendsto.add
-- 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)
m : E
this : x + HSMul.hSMul (α := ℝ) 4 (z + HSMul.hSMul (α := ℝ) 0 m) = y
refine : Tendsto (fun (t : ℝ) ↦ t • m) (𝓝 0) (𝓝 (HSMul.hSMul (α := ℝ) 0 m))
⊢ Tendsto (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m)) (𝓝 0)
    (𝓝 (x + HSMul.hSMul (α := ℝ) 4 (z + HSMul.hSMul (α := ℝ) 0 m)))

Tactic:
refine tendsto_const_nhds.add <| tendsto_const_nhds.smul <| tendsto_const_nhds.add ?_

Premises used: tendsto_const_nhds, Filter.Tendsto.smul, Filter.Tendsto.add
-- 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)
m : E
this : x + HSMul.hSMul (α := ℝ) 4 (z + HSMul.hSMul (α := ℝ) 0 m) = y
⊢ Tendsto (fun (t : ℝ) ↦ t • m) (𝓝 0) (𝓝 (HSMul.hSMul (α := ℝ) 0 m))

Tactic:
continuousAt_id.smul continuousAt_const

Premises used: ContinuousAt, ContinuousAt.smul, continuousAt_const, continuousAt_id
-- 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)
m : E
this : x + HSMul.hSMul (α := ℝ) 4 (z + HSMul.hSMul (α := ℝ) 0 m) = y
⊢ Tendsto (fun (t : ℝ) ↦ t • m) (𝓝 0) (𝓝 (HSMul.hSMul (α := ℝ) 0 m))

Tactic:
exact continuousAt_id.smul continuousAt_const

Premises used: ContinuousAt.smul, continuousAt_const, continuousAt_id
-- 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)
⊢ ∀ (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
-- 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)
m : E
a :
  Membership.mem (γ := Filter ℝ) (𝓝 0)
    {x_1 : ℝ | (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m) ∈ interior s) x_1}
⊢ ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + HSMul.hSMul (α := ℝ) 4 (z + t • m) ∈ interior s

Tactic:
apply nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds
-- 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)
m : E
a : interior s ∈ 𝓝 y
⊢ Membership.mem (γ := Filter ℝ) (𝓝 0)
    {x_1 : ℝ | (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m) ∈ interior s) x_1}

Tactic:
apply A m
-- 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)
m : E
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
⊢ interior s ∈ 𝓝 y

Tactic:
rw [mem_interior_iff_mem_nhds] at hy

Premises used: mem_interior_iff_mem_nhds
-- 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 : 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:
interior_mem_nhds.2 hy

Premises used: Iff.mpr, interior_mem_nhds
-- 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 : 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:
exact interior_mem_nhds.2 hy

Premises used: Iff.mpr, interior_mem_nhds
-- 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)
⊢ ∀ (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
-- 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
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)
⊢ 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

Premises used: Filter.Eventually.and, Filter.Eventually.exists, 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 : 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) (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)
-- 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
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)
⊢ 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

Premises used: ContinuousLinearMap.coe_smul', smul_zero, map_add, ContinuousLinearMap.add_apply, add_zero, add_right_inj, 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
m : E
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)
⊢ 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:
smul_right_injective F (tpos m).ne' this

Premises used: smul_right_injective, 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
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 :
  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)
⊢ 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:
exact smul_right_injective F (tpos m).ne' this

Premises used: smul_right_injective, LT.lt.ne'