-- 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 :
  ∀ ⦃c : ℝ⦄,
    0 < c →
      ∀ᶠ (x_1 : E) in 𝓝[interior s] x,
        ‖HSub.hSub (β := E →L[ℝ] F) (f' x_1 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_1 - x) : E →L[ℝ] F)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ :
  Metric.ball x δ ∩ interior s ⊆
    {x_1 : E |
      (fun (x_2 : E) ↦
          ‖HSub.hSub (β := E →L[ℝ] F) (f' x_2 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_2 - x) : E →L[ℝ] F)‖ ≤
            ε * ‖x_2 - x‖)
        x_1}
E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ
E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1
h : ℝ
hδ : h * (‖v‖ + ‖w‖) < δ
h_lt_1 : h < 1
hpos : 0 < h
xt_mem : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Icc 0 1) t → x + h • v + (t * h) • w ∈ interior s
g : (t : ℝ) → F :=
  fun (t : ℝ) ↦
    f (x + h • v + (t * h) • w) - HSMul.hSMul (β := F) (t * h) ((f' x : (a : E) → F) w : F) -
        HSMul.hSMul (β := F) (t * HPow.hPow (β := ℕ) h 2)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
      HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) (t * h) 2 / 2)
        ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F)
g' : (t : ℝ) → F :=
  fun (t : ℝ) ↦
    HSub.hSub (α := F) ((f' (x + h • v + (t * h) • w) : (a : E) → F) (h • w) : F)
          (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 : E →L[ℝ] F) : (a : E) → F) w : F) -
      HSMul.hSMul (β := F) (t * HPow.hPow (β := ℕ) h 2)
        ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F)
hg' :
  g' = fun (t : ℝ) ↦
    HSub.hSub (α := F) ((f' (x + h • v + (t * h) • w) : (a : E) → F) (h • w) : F)
          (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 : E →L[ℝ] F) : (a : E) → F) w : F) -
      HSMul.hSMul (β := F) (t * HPow.hPow (β := ℕ) h 2)
        ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F)
g_deriv : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Icc 0 1) t → HasDerivWithinAt g (g' t) (Icc 0 1) t
⊢ ‖f (x + h • v + h • w) - f (x + h • v) - 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 : 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)‖ ≤
    ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * HPow.hPow (β := ℕ) h 2‖
have g'_bound : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ico 0 1) t → ‖g' t‖ ≤ ε * ((‖v‖ + ‖w‖) * ‖w‖) * HPow.hPow (β := ℕ) h 2
Tactic: have g'_bound : ∀ t ∈ Ico (0 : ℝ) 1, ‖g' t‖ ≤ ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2 := by
    intro t ht
    have I : ‖h • v + (t * h) • w‖ ≤ h * (‖v‖ + ‖w‖) :=
      calc
        ‖h • v + (t * h) • w‖ ≤ ‖h • v‖ + ‖(t * h) • w‖ := norm_add_le _ _
        _ = h * ‖v‖ + t * (h * ‖w‖) := by
          simp only [norm_smul, Real.norm_eq_abs, hpos.le, abs_of_nonneg, abs_mul, ht.left,
            mul_assoc]
        _ ≤ h * ‖v‖ + 1 * (h * ‖w‖) := by gcongr; exact ht.2.le
        _ = h * (‖v‖ + ‖w‖) := by ring
    calc
      ‖g' t‖ = ‖(f' (x + h • v + (t * h) • w) - f' x - f'' (h • v + (t * h) • w)) (h • w)‖ := by
        rw [hg']
        congrm ‖?_‖
        simp only [ContinuousLinearMap.sub_apply, ContinuousLinearMap.add_apply,
          ContinuousLinearMap.smul_apply, map_add, map_smul]
        module
      _ ≤ ‖f' (x + h • v + (t * h) • w) - f' x - f'' (h • v + (t * h) • w)‖ * ‖h • w‖ :=
        (ContinuousLinearMap.le_opNorm _ _)
      _ ≤ ε * ‖h • v + (t * h) • w‖ * ‖h • w‖ := by
        gcongr
        have H : x + h • v + (t * h) • w ∈ Metric.ball x δ ∩ interior s := by
          refine ⟨?_, xt_mem t ⟨ht.1, ht.2.le⟩⟩
          rw [add_assoc, add_mem_ball_iff_norm]
          exact I.trans_lt hδ
        simpa only [mem_setOf_eq, add_assoc x, add_sub_cancel_left] using sδ H
      _ ≤ ε * (‖h • v‖ + ‖h • w‖) * ‖h • w‖ := by
        gcongr
        apply (norm_add_le _ _).trans
        gcongr
        simp only [norm_smul, Real.norm_eq_abs, abs_mul, abs_of_nonneg, ht.1, hpos.le, mul_assoc]
        exact mul_le_of_le_one_left (by positivity) ht.2.le
      _ = ε * ((‖v‖ + ‖w‖) * ‖w‖) * h ^ 2 := by
        simp only [norm_smul, Real.norm_eq_abs, abs_of_nonneg, hpos.le]; ring