awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ 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
⊢ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x) f
have this : ∀ᶠ (δ : ℝ) in 𝓝 0, (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀ ∈ C
Tactic: have : ∀ᶠ δ in 𝓝 (0 : ℝ), (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀ ∈ C := by
      have h : ContinuousAt (fun δ : ℝ ↦ (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀) 0 := by
        fun_prop (disch := norm_num)
      exact h (by simpa using hC.mem_nhds hx)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ 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
⊢ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x) f
have obtain : ∀ (δ : ℝ) (hδ₀ : 0 < δ) (hy : (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀ ∈ C) (hδ₁ : δ < 1),
  Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x) f
Tactic: obtain ⟨δ, hδ₀, hy, hδ₁⟩ := (this.and <| eventually_lt_nhds zero_lt_one).exists_gt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ 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
have refine : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x (max r (f y))
Tactic: refine ⟨max r (f y), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ 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 (max r (f y))
have simp : ∀ (hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r), ∀ᶠ (a : E) in 𝓝 x, f a ≤ max r (f y)
Tactic: simp only [Filter.eventually_map] at hr ⊢
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ 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
⊢ ∀ᶠ (a : E) in 𝓝 x, f a ≤ max r (f y)
have obtain : ∀ (ε : ℝ) (hε : ε > 0) (hr : ∀ ⦃y : E⦄, dist y x₀ < ε → f y ≤ r ∧ y ∈ C), ∀ᶠ (a : E) in 𝓝 x, f a ≤ max r (f y)
Tactic: obtain ⟨ε, hε, hr⟩ := Metric.eventually_nhds_iff.1 <| hr.and (hC.eventually_mem hx₀)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ 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_1 : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
ε : ℝ
hε : ε > 0
hr : ∀ ⦃y : E⦄, dist y x₀ < ε → f y ≤ r ∧ y ∈ C
⊢ ∀ᶠ (a : E) in 𝓝 x, f a ≤ max r (f y)
have refine : ∀ (z : E) (hz : dist z x < ε * δ), f z ≤ max r (f y)
Tactic: refine Metric.eventually_nhds_iff.2 ⟨ε * δ, by positivity, fun z hz ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ 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_1 : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
ε : ℝ
hε : ε > 0
hr : ∀ ⦃y : E⦄, dist y x₀ < ε → f y ≤ r ∧ y ∈ C
z : E
hz : dist z x < ε * δ
⊢ f z ≤ max r (f y)
have hx₀' : δ⁻¹ • (x - y) + y = x₀
Tactic: have hx₀' : δ⁻¹ • (x - y) + y = x₀ := MulAction.injective₀ (sub_ne_zero.2 hδ₁.ne') <| by
      simp [y, smul_sub, smul_smul, hδ₀.ne', div_eq_mul_inv, sub_ne_zero.2 hδ₁.ne', mul_left_comm,
        sub_mul, sub_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ 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_1 : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
ε : ℝ
hε : ε > 0
hr : ∀ ⦃y : E⦄, dist y x₀ < ε → f y ≤ r ∧ y ∈ C
z : E
hz : dist z x < ε * δ
hx₀' : δ⁻¹ • (x - y) + y = x₀
w : E := δ⁻¹ • (z - y) + y
⊢ f z ≤ max r (f y)
have hwyz : δ • w + (1 - δ) • y = z
Tactic: have hwyz : δ • w + (1 - δ) • y = z := by simp [w, hδ₀.ne', sub_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ 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_1 : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
ε : ℝ
hε : ε > 0
hr : ∀ ⦃y : E⦄, dist y x₀ < ε → f y ≤ r ∧ y ∈ C
z : E
hz : dist z x < ε * δ
hx₀' : δ⁻¹ • (x - y) + y = x₀
w : E := δ⁻¹ • (z - y) + y
hwyz : δ • w + (1 - δ) • y = z
⊢ f z ≤ max r (f y)
have hw : dist w x₀ < ε
Tactic: have hw : dist w x₀ < ε := by
      simpa [w, ← hx₀', dist_smul₀, abs_of_nonneg, hδ₀.le, inv_mul_lt_iff₀', hδ₀]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ 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_1 : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
ε : ℝ
hε : ε > 0
hr : ∀ ⦃y : E⦄, dist y x₀ < ε → f y ≤ r ∧ y ∈ C
z : E
hz : dist z x < ε * δ
hx₀' : δ⁻¹ • (x - y) + y = x₀
w : E := δ⁻¹ • (z - y) + y
hwyz : δ • w + (1 - δ) • y = z
hw : dist w x₀ < ε
⊢ max (f w) (f y) ≤ max r (f y)
have h₁ : f w ≤ r
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ 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_1 : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
ε : ℝ
hε : ε > 0
hr : ∀ ⦃y : E⦄, dist y x₀ < ε → f y ≤ r ∧ y ∈ C
z : E
hz : dist z x < ε * δ
hx₀' : δ⁻¹ • (x - y) + y = x₀
w : E := δ⁻¹ • (z - y) + y
hwyz : δ • w + (1 - δ) • y = z
hw : dist w x₀ < ε
⊢ f z ≤ max r (f y)
have f₁ : max (f w) (f y) ≤ max r (f y)
Tactic: calc
      f z ≤ max (f w) (f y) :=
        hf.le_max_of_mem_segment (hr hw).2 hy ⟨_, _, hδ₀.le, sub_nonneg.2 hδ₁.le, by simp, hwyz⟩
      _ ≤ max r (f y) := by gcongr; exact (hr hw).1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ x₀ ∈ C, ContinuousAt f x₀), ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) 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
have tfae_4_to_5 : ∀ (a : ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f) ⦃x₀ : E⦄,
  x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
Tactic: tfae_have 4 → 5
  | ⟨x₀, hx₀, r, hr⟩, x, hx => by
    have : ∀ᶠ δ in 𝓝 (0 : ℝ), (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀ ∈ C := by
      have h : ContinuousAt (fun δ : ℝ ↦ (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀) 0 := by
        fun_prop (disch := norm_num)
      exact h (by simpa using hC.mem_nhds hx)
    obtain ⟨δ, hδ₀, hy, hδ₁⟩ := (this.and <| eventually_lt_nhds zero_lt_one).exists_gt
    set y := (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀
    refine ⟨max r (f y), ?_⟩
    simp only [Filter.eventually_map] at hr ⊢
    obtain ⟨ε, hε, hr⟩ := Metric.eventually_nhds_iff.1 <| hr.and (hC.eventually_mem hx₀)
    refine Metric.eventually_nhds_iff.2 ⟨ε * δ, by positivity, fun z hz ↦ ?_⟩
    have hx₀' : δ⁻¹ • (x - y) + y = x₀ := MulAction.injective₀ (sub_ne_zero.2 hδ₁.ne') <| by
      simp [y, smul_sub, smul_smul, hδ₀.ne', div_eq_mul_inv, sub_ne_zero.2 hδ₁.ne', mul_left_comm,
        sub_mul, sub_smul]
    let w := δ⁻¹ • (z - y) + y
    have hwyz : δ • w + (1 - δ) • y = z := by simp [w, hδ₀.ne', sub_smul]
    have hw : dist w x₀ < ε := by
      simpa [w, ← hx₀', dist_smul₀, abs_of_nonneg, hδ₀.le, inv_mul_lt_iff₀', hδ₀]
    calc
      f z ≤ max (f w) (f y) :=
        hf.le_max_of_mem_segment (hr hw).2 hy ⟨_, _, hδ₀.le, sub_nonneg.2 hδ₁.le, by simp, hwyz⟩
      _ ≤ max r (f y) := by gcongr; exact (hr hw).1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ x₀ ∈ C, ContinuousAt f x₀), ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_4_to_5 :
  ∀ (a : ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f) ⦃x₀ : E⦄,
    x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) 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
have 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
Tactic: tfae_have 6 ↔ 5 := forall₂_congr fun x₀ hx₀ ↦ hf.isBoundedUnder_abs (hC.mem_nhds hx₀)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ x₀ ∈ C, ContinuousAt f x₀), ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_4_to_5 :
  ∀ (a : ∃ 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
⊢ ∃ (K : NNReal), ∃ t ∈ 𝓝[C] x, LipschitzOnWith K f t
have obtain : ∀ (r : ℝ) (hr : ∀ᶠ (x : ℝ) in Filter.map |f| (𝓝 x), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r),
  ∃ (K : NNReal), ∃ t ∈ 𝓝[C] x, LipschitzOnWith K f t
Tactic: obtain ⟨r, hr⟩ := h hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ x₀ ∈ C, ContinuousAt f x₀), ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_4_to_5 :
  ∀ (a : ∃ 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
⊢ ∃ (K : NNReal), ∃ t ∈ 𝓝[C] x, LipschitzOnWith K f t
have obtain : ∀ (ε : ℝ) (hε : ε > 0)
  (hεD : ball x ε ⊆ C ∩ |f| ⁻¹' {x : ℝ | (fun (x : ℝ) ↦ ((fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r : Prop)) x}),
  ∃ (K : NNReal), ∃ t ∈ 𝓝[C] x, LipschitzOnWith K f t
Tactic: obtain ⟨ε, hε, hεD⟩ := Metric.mem_nhds_iff.1 <| Filter.inter_mem (hC.mem_nhds hx) hr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ x₀ ∈ C, ContinuousAt f x₀), ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_4_to_5 :
  ∀ (a : ∃ 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 ∩ |f| ⁻¹' {x : ℝ | (fun (x : ℝ) ↦ ((fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r : Prop)) x}
⊢ ∃ (K : NNReal), ∃ t ∈ 𝓝[C] x, LipschitzOnWith K f t
have simp : ∀ (hεD : ball x ε ⊆ C ∧ ball x ε ⊆ {a : E | |f a| ≤ r}), ∃ (K : NNReal), ∃ t ∈ 𝓝 x, LipschitzOnWith K f t
Tactic: simp only [preimage_setOf_eq, Pi.abs_apply, subset_inter_iff, hC.nhdsWithin_eq hx] at hεD ⊢
Cleared hypotheses: hεD
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ x₀ ∈ C, ContinuousAt f x₀), ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_4_to_5 :
  ∀ (a : ∃ 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 : E | |f a| ≤ r}
⊢ ∃ (K : NNReal), ∃ t ∈ 𝓝 x, LipschitzOnWith K f t
have obtain : ∀ (K : NNReal) (hK : LipschitzOnWith K f (ball x (ε / 2))), ∃ (K : NNReal), ∃ 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⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ x₀ ∈ C, ContinuousAt f x₀), ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_4_to_5 :
  ∀ (a : ∃ 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
⊢ [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
have tfae_6_to_1 : ∀ (a : ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|), LocallyLipschitzOn C f
Tactic: tfae_have 6 → 1
  | h, x, hx => by
    obtain ⟨r, hr⟩ := h hx
    obtain ⟨ε, hε, hεD⟩ := Metric.mem_nhds_iff.1 <| Filter.inter_mem (hC.mem_nhds hx) hr
    simp only [preimage_setOf_eq, Pi.abs_apply, subset_inter_iff, hC.nhdsWithin_eq hx] at hεD ⊢
    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⟩
    exact ⟨K, _, ball_mem_nhds _ (by simpa), hK⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConcaveOn ℝ 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
have this : [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: have := hf.neg.continuousOn_tfae hC hC'