-- Module: Mathlib.Analysis.Calculus.Rademacher
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
F : Type u_2
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
C : ℝ≥0
inst_4 : FiniteDimensional ℝ E
f : E → F
hf : LipschitzWith C f
s : Set E
hs : sphere 0 1 ⊆ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
L : E →L[ℝ] F
x : E
hL : ∀ v ∈ s, HasLineDerivAt ℝ f ((L : (a : E) → F) v) x v
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : ((↑C : ℝ) + ‖L‖ + 1) * δ = ε
q : Set E
hqs : q ⊆ s
q_fin : q.Finite
hq : Subset.{u_1} (α := Set E) (sphere 0 1) (⋃ y ∈ q, ball y δ)
I : ∀ᶠ (t : ℝ) in 𝓝 0, ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
r : ℝ
r_pos : 0 < r
hr : ∀ (t : ℝ), ‖t‖ < r → ∀ v ∈ q, ‖f (x + t • v) - f x - HSMul.hSMul (β := F) t ((L : (a : E) → F) v : F)‖ ≤ δ * ‖t‖
v : E
hv : Membership.mem (γ := Set E) (ball 0 r) v
v_ne : v ≠ 0
w : E
ρ : ℝ
w_mem : Membership.mem (γ := Set E) (sphere 0 1) w
hvw : v = ρ • w
hρ : ρ = ‖v‖
norm_rho : ‖ρ‖ = ρ
rho_pos : 0 ≤ ρ
y : E
yq : y ∈ q
hy : ‖w - y‖ < δ
this : ‖y - w‖ < δ
calc :
  ‖HSub.hSub (β := F) (f (x + v) - f x) ((L : (a : E) → F) v : F)‖ =
    ‖f (x + ρ • w) - f x - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) w : F)‖
calc₁ :
  ‖f (x + ρ • w) - f x - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) w : F)‖ =
    ‖f (x + ρ • w) - f (x + ρ • y) +
          (HSMul.hSMul (β := F) ρ ((L : (a : E) → F) y : F) - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) w : F)) +
        (f (x + ρ • y) - f x - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) y : F))‖
calc₂ :
  ‖f (x + ρ • w) - f (x + ρ • y)‖ +
        ‖HSMul.hSMul (β := F) ρ ((L : (a : E) → F) y : F) - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) w : F)‖ +
      ‖f (x + ρ • y) - f x - HSMul.hSMul (β := F) ρ ((L : (a : E) → F) y : F)‖ ≤
    (↑C : ℝ) * ‖x + ρ • w - (x + ρ • y)‖ + ρ * (‖L‖ * ‖y - w‖) + δ * ρ
calc₃ : (↑C : ℝ) * ‖x + ρ • w - (x + ρ • y)‖ + ρ * (‖L‖ * ‖y - w‖) + δ * ρ ≤ (↑C : ℝ) * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ
calc₄ : (↑C : ℝ) * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ = ((↑C : ℝ) + ‖L‖ + 1) * δ * ρ
calc₅ : ((↑C : ℝ) + ‖L‖ + 1) * δ * ρ = ε * ‖v‖
⊢ Membership.mem (γ := Set E)
    {x_1 : E | (fun (x_2 : E) ↦ ‖HSub.hSub (β := F) (f (x + x_2) - f x) ((L : (a : E) → F) x_2 : F)‖ ≤ ε * ‖x_2‖) x_1} v

Tactic:
calc ‖f (x + v) - f x - L v‖
      = ‖f (x + ρ • w) - f x - ρ • L w‖ := by simp [hvw]
    _ = ‖(f (x + ρ • w) - f (x + ρ • y)) + (ρ • L y - ρ • L w)
          + (f (x + ρ • y) - f x - ρ • L y)‖ := by congr; abel
    _ ≤ ‖f (x + ρ • w) - f (x + ρ • y)‖ + ‖ρ • L y - ρ • L w‖
          + ‖f (x + ρ • y) - f x - ρ • L y‖ := norm_add₃_le
    _ ≤ C * ‖(x + ρ • w) - (x + ρ • y)‖ + ρ * (‖L‖ * ‖y - w‖) + δ * ρ := by
      gcongr
      · exact hf.norm_sub_le _ _
      · rw [← smul_sub, norm_smul, norm_rho]
        gcongr
        exact L.lipschitz.norm_sub_le _ _
      · conv_rhs => rw [← norm_rho]
        apply hr _ _ _ yq
        simpa [norm_rho, hρ] using hv
    _ ≤ C * (ρ * δ) + ρ * (‖L‖ * δ) + δ * ρ := by
      simp only [add_sub_add_left_eq_sub, ← smul_sub, norm_smul, norm_rho]; gcongr
    _ = ((C + ‖L‖ + 1) * δ) * ρ := by ring
    _ = ε * ‖v‖ := by rw [hδ, hρ]

Premises used: Norm.norm, HMul.hMul, norm_add₃_le, HSub.hSub, HAdd.hAdd, HSMul.hSMul, OfNat.ofNat, DFunLike.coe, NNReal.toReal