Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf : LocallyLipschitzOn s f
⊢ ∃ K, LipschitzOnWith K f s

Tactic:
by
  /- `f` being locally Lipschitz on `s` means that it is continuous and that it is Lipschitz on a
  ball of some radius `ε x hx` within `s` with Lipschitz bound `K x hx` around every `x ∈ s`. -/
  have hf' := hf.continuousOn
  replace hf : ∀ x ∈ s, ∃ ε > 0, ∃ K, LipschitzOnWith K f (ball x ε ∩ s) := fun x hx ↦ by
    let ⟨K, t, ht, hf⟩ := hf hx
    let ⟨ε, hε, hε'⟩ := Metric.mem_nhdsWithin_iff.1 ht
    exact ⟨ε, hε, K, hf.mono hε'⟩
  choose ε hε K hf using hf
  /- We also have constants `K' x hx` for all `x ∈ s` such that `edist (f x) (f y) ≤ K' * edist x y`
  for all `y ∈ s` outside of `ball x (ε x hx)`, by continuity of
  `fun y ↦ dist (f x) (f y) / dist x y` on the compact set `s.diff (ball x (ε x hx))`. -/
  have (x) (hx : x ∈ s) : ∃ K' : ℝ≥0, ∀ y ∈ s.diff (ball x (ε x hx)),
      edist (f x) (f y) ≤ K' * edist x y := by
    let ⟨K', hK'⟩ := (hs.diff isOpen_ball).bddAbove_image
      (f := fun y ↦ dist (f x) (f y) / dist x y) <| .div (.mono (by fun_prop) s.sdiff_subset)
        (by fun_prop) fun y hy ↦ ((hε x hx).trans_le <| not_lt.1 <| dist_comm x y ▸ hy.2).ne'
    refine ⟨.mk (K' ⊔ 0) le_sup_right, fun y hy ↦ ?_⟩
    simp_rw [edist_nndist, ← ENNReal.coe_mul, ENNReal.coe_le_coe]
    refine (div_le_iff₀ ?_).1 ?_
    · exact NNReal.coe_pos.1 <| coe_nndist x y ▸
        ((hε x hx).trans_le <| not_lt.1 <| dist_comm x y ▸ hy.2)
    · simp [← NNReal.coe_le_coe, (mem_upperBounds.1 hK') _ <| mem_image_of_mem _ hy]
  choose K' hK' using this
  /- By compactness of `s`, there exists some finite set `t` such that the balls of radius
  `ε x hx / 2` around all `x ∈ t` cover `s`. -/
  obtain ⟨t, ht⟩ := hs.elim_nhdsWithin_subcover' (fun x hx ↦ s ∩ ball x (ε x hx / 2))
    (fun x hx ↦ inter_mem_nhdsWithin s <| ball_mem_nhds x <| half_pos <| hε x hx)
  /- For every `z ∈ t` we can show that `f` satisfies the Lipschitz condition with bound
  `K z hz + 2 * K' z hz` for all points `x ∈ s ∩ ball z (ε z hz / 2)` and `y ∈ s`, so `f` is
  Lipschitz on `s` with the supremum of these bounds over all `z ∈ t` as its bound. -/
  use t.sup fun i ↦ K _ i.2 + 2 * K' _ i.2
  intro x hx y hy
  let ⟨z, hz, hx'⟩ := mem_iUnion₂.1 <| ht hx
  by_cases hy' : y ∈ ball z.1 (ε _ z.2)
  · /- For `y ∈ ball z (ε z hz)` this follows from `f` being Lipschitz with bound `K z hz`
    on `ball z (ε z hz)`. -/
    refine (hf _ z.2 ⟨hx'.2.trans <| half_lt_self <| hε _ z.2, hx⟩ ⟨hy', hy⟩).trans <|
      mul_le_mul_of_nonneg_right ?_ zero_le
    exact ENNReal.coe_le_coe.2 <| t.le_sup_of_le hz <| le_self_add
  · /- For `y ∉ ball z (ε z hz)` this follows by using the triangle inequality, bounding
    the distances from `f z` to `f x` and `f y` using the bounds `K z hz` and `K' z hz`, and then
    using the triangle inequality again for `edist z y ≤ edist x z + edist x y ≤ 2 * edist x y`. -/
    calc edist (f x) (f y)
      _ ≤ edist (f z) (f x) + edist (f z) (f y) := edist_triangle_left _ _ _
      _ ≤ (K _ z.2) * edist z.1 x + edist (f z) (f y) := add_le_add_left
        (hf _ z.2 ⟨mem_ball_self <| hε _ z.2, z.2⟩ ⟨hx'.2.trans <| half_lt_self <| hε _ z.2, hx⟩) _
      _ ≤ (K _ z.2) * edist z.1 x + (K' _ z.2) * edist z.1 y :=
        add_le_add_right (hK' _ z.2 _ ⟨hy, hy'⟩) _
      _ ≤ (K _ z.2) * edist z.1 x + (K' _ z.2) * (edist x z.1 + edist x y) := by
        gcongr; exact edist_triangle_left z.1 y x
      _ ≤ (K _ z.2) * edist x y + (K' _ z.2) * (edist x y + edist x y) := by
        simp_rw [edist_dist, dist_comm _ x]
        gcongr <;> linarith [mem_ball.1 hx'.2, (not_lt (α := ℝ)).1 hy', dist_triangle_left y z x]
      _ = ↑(K _ z.2 + 2 * K' _ z.2) * edist x y := by push_cast; ring
      _ ≤ _ := by gcongr; exact .trans (by rfl) (t.le_sup hz)

Goal state after: