Module: Mathlib.Analysis.Calculus.FDeriv.Extend

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
s : Set E
x : E
f' : E →L[ℝ] F
f_diff : DifferentiableOn ℝ f s
s_conv : Convex ℝ s
s_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
f_cont : ∀ y ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s, ContinuousWithinAt f s y
h : Tendsto (fun y ↦ fderiv ℝ f y) (𝓝[s] x) (𝓝 f')
⊢ HasFDerivWithinAt f f' (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) x

Tactic:
by
  -- one can assume without loss of generality that `x` belongs to the closure of `s`, as the
  -- statement is empty otherwise
  by_cases! hx : x ∉ closure s
  · rw [← closure_closure] at hx; exact HasFDerivWithinAt.of_notMem_closure hx
  rw [hasFDerivWithinAt_iff_isLittleO, Asymptotics.isLittleO_iff]
  /- One needs to show that `‖f y - f x - f' (y - x)‖ ≤ ε ‖y - x‖` for `y` close to `x` in
    `closure s`, where `ε` is an arbitrary positive constant. By continuity of the functions, it
    suffices to prove this for nearby points inside `s`. In a neighborhood of `x`, the derivative
    of `f` is arbitrarily close to `f'` by assumption. The mean value inequality completes the
    proof. -/
  intro ε ε_pos
  obtain ⟨δ, δ_pos, hδ⟩ : ∃ δ > 0, ∀ y ∈ s, dist y x < δ → ‖fderiv ℝ f y - f'‖ < ε := by
    simpa [dist_eq_norm] using tendsto_nhdsWithin_nhds.1 h ε ε_pos
  set B := ball x δ
  suffices ∀ y ∈ B ∩ closure s, ‖f y - f x - (f' y - f' x)‖ ≤ ε * ‖y - x‖ from
    mem_nhdsWithin_iff.2 ⟨δ, δ_pos, fun y hy => by simpa using this y hy⟩
  suffices
    ∀ p : E × E,
      p ∈ closure ((B ∩ s) ×ˢ (B ∩ s)) → ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖ by
    rw [closure_prod_eq] at this
    intro y y_in
    apply this ⟨x, y⟩
    have : B ∩ closure s ⊆ closure (B ∩ s) := isOpen_ball.inter_closure
    exact ⟨this ⟨mem_ball_self δ_pos, hx⟩, this y_in⟩
  have key : ∀ p : E × E, p ∈ (B ∩ s) ×ˢ (B ∩ s) →
        ‖f p.2 - f p.1 - (f' p.2 - f' p.1)‖ ≤ ε * ‖p.2 - p.1‖ := by
    rintro ⟨u, v⟩ ⟨u_in, v_in⟩
    have conv : Convex ℝ (B ∩ s) := (convex_ball _ _).inter s_conv
    have diff : DifferentiableOn ℝ f (B ∩ s) := f_diff.mono inter_subset_right
    have bound : ∀ z ∈ B ∩ s, ‖fderivWithin ℝ f (B ∩ s) z - f'‖ ≤ ε := by
      intro z z_in
      have h := hδ z
      have : fderivWithin ℝ f (B ∩ s) z = fderiv ℝ f z := by
        have op : IsOpen (B ∩ s) := isOpen_ball.inter s_open
        rw [DifferentiableAt.fderivWithin _ (op.uniqueDiffOn z z_in)]
        exact (diff z z_in).differentiableAt (IsOpen.mem_nhds op z_in)
      rw [← this] at h
      exact le_of_lt (h z_in.2 z_in.1)
    simpa using conv.norm_image_sub_le_of_norm_fderivWithin_le' diff bound u_in v_in
  rintro ⟨u, v⟩ uv_in
  have f_cont' : ∀ y ∈ closure s, ContinuousWithinAt (f - ⇑f') s y := by
    intro y y_in
    exact Tendsto.sub (f_cont y y_in) f'.cont.continuousWithinAt
  refine ContinuousWithinAt.closure_le uv_in ?_ ?_ key
  all_goals
    -- common start for both continuity proofs
    have : (B ∩ s) ×ˢ (B ∩ s) ⊆ s ×ˢ s := by grw [inter_subset_right]
    obtain ⟨u_in, v_in⟩ : u ∈ closure s ∧ v ∈ closure s := by
      simpa [closure_prod_eq] using closure_mono this uv_in
    apply ContinuousWithinAt.mono _ this
    simp only [ContinuousWithinAt]
  · rw [nhdsWithin_prod_eq]
    have : ∀ u v, f v - f u - (f' v - f' u) = f v - f' v - (f u - f' u) := by intros; abel
    simp only [this]
    exact
      Tendsto.comp continuous_norm.continuousAt
        ((Tendsto.comp (f_cont' v v_in) tendsto_snd).sub <|
          Tendsto.comp (f_cont' u u_in) tendsto_fst)
  · apply tendsto_nhdsWithin_of_tendsto_nhds
    rw [nhds_prod_eq]
    exact
      tendsto_const_nhds.mul
        (Tendsto.comp continuous_norm.continuousAt <| tendsto_snd.sub tendsto_fst)

Goal state after: