-- Mathlib/Analysis/Convex/Continuous.lean
lemma ConvexOn.continuousOn_tfae (hC : IsOpen C) (hC' : C.Nonempty) (hf : ConvexOn ℝ C f) : TFAE [
    LocallyLipschitzOn C f,
    ContinuousOn f C,
    ∃ x₀ ∈ C, ContinuousAt f x₀,
    ∃ x₀ ∈ C, (𝓝 x₀).IsBoundedUnder (· ≤ ·) f,
    ∀ ⦃x₀⦄, x₀ ∈ C → (𝓝 x₀).IsBoundedUnder (· ≤ ·) f,
    ∀ ⦃x₀⦄, x₀ ∈ C → (𝓝 x₀).IsBoundedUnder (· ≤ ·) |f|]

Proof state:
case intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : LocallyLipschitzOn C f → ContinuousOn f C
tfae_2_to_3 : ContinuousOn f C → ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : (∃ x₀ ∈ C, ContinuousAt f x₀) → ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) f
tfae_4_to_5 :
  (∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) f) →
    ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) f
tfae_6_iff_5 :
  (∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) |f|) ↔
    ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) f
h : ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) |f|
x : E
hx : x ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map |f| (𝓝 x), (fun x1 x2 => x1 ≤ x2) x r
ε : ℝ
hε : ε > 0
hεD : ball x ε ⊆ C ∧ ball x ε ⊆ {a | |f a| ≤ r}
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K f t

Tactic:
obtain ⟨K, hK⟩ := exists_lipschitzOnWith_of_isBounded (hf.subset hεD.1 (convex_ball ..))
  (half_lt_self hε) <| isBounded_iff_forall_norm_le.2 ⟨r, by simpa using hεD.2⟩

Result:
case intro.intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : LocallyLipschitzOn C f → ContinuousOn f C
tfae_2_to_3 : ContinuousOn f C → ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : (∃ x₀ ∈ C, ContinuousAt f x₀) → ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) f
tfae_4_to_5 :
  (∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) f) →
    ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) f
tfae_6_iff_5 :
  (∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) |f|) ↔
    ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) f
h : ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) |f|
x : E
hx : x ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map |f| (𝓝 x), (fun x1 x2 => x1 ≤ x2) x r
ε : ℝ
hε : ε > 0
hεD : ball x ε ⊆ C ∧ ball x ε ⊆ {a | |f a| ≤ r}
K : NNReal
hK : LipschitzOnWith K f (ball x (ε / 2))
⊢ ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K f t

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : LocallyLipschitzOn C f → ContinuousOn f C
tfae_2_to_3 : ContinuousOn f C → ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : (∃ x₀ ∈ C, ContinuousAt f x₀) → ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) f
x₀ : E
hx₀ : x₀ ∈ C
r : ℝ
x : E
hx : x ∈ C
this : ∀ᶠ (δ : ℝ) in 𝓝 0, (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀ ∈ C
δ : ℝ
hδ₀ : δ > 0
hδ₁ : δ < 1
y : E := (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀
hy : y ∈ C
hr✝ : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
ε : ℝ
hε : ε > 0
hr : ∀ ⦃y : E⦄, dist y x₀ < ε → f y ≤ r ∧ y ∈ C
⊢ ε * δ > 0

Tactic:
positivity

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : LocallyLipschitzOn C f → ContinuousOn f C
⊢ ContinuousOn f C → ∃ x₀ ∈ C, ContinuousAt f x₀

Tactic:
obtain ⟨x₀, hx₀⟩ := hC'

Result:
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen C
hf : ConvexOn ℝ C f
tfae_1_to_2 : LocallyLipschitzOn C f → ContinuousOn f C
x₀ : E
hx₀ : x₀ ∈ C
⊢ ContinuousOn f C → ∃ x₀ ∈ C, ContinuousAt f x₀

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
⊢ [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) f,
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) f,
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) |f|].TFAE

Tactic:
tfae_have 1 → 2 := LocallyLipschitzOn.continuousOn

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : LocallyLipschitzOn C f → ContinuousOn f C
⊢ [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) f,
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) f,
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) |f|].TFAE

Proof state:
case intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : LocallyLipschitzOn C f → ContinuousOn f C
tfae_2_to_3 : ContinuousOn f C → ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : (∃ x₀ ∈ C, ContinuousAt f x₀) → ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) f
x₀ : E
hx₀ : x₀ ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun x1 x2 => x1 ≤ x2) x r
x : E
hx : x ∈ C
this : ∀ᶠ (δ : ℝ) in 𝓝 0, (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀ ∈ C
δ : ℝ
hδ₀ : δ > 0
hδ₁ : δ < 1
y : E := (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀
hy : y ∈ C
⊢ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x) f

Tactic:
refine ⟨max r (f y), ?_⟩

Result:
case intro.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : LocallyLipschitzOn C f → ContinuousOn f C
tfae_2_to_3 : ContinuousOn f C → ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : (∃ x₀ ∈ C, ContinuousAt f x₀) → ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (𝓝 x₀) f
x₀ : E
hx₀ : x₀ ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun x1 x2 => x1 ≤ x2) x r
x : E
hx : x ∈ C
this : ∀ᶠ (δ : ℝ) in 𝓝 0, (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀ ∈ C
δ : ℝ
hδ₀ : δ > 0
hδ₁ : δ < 1
y : E := (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀
hy : y ∈ C
⊢ ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x), (fun x1 x2 => x1 ≤ x2) x (r ⊔ f y)