awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
hz : z ∈ ball x₀ r
a : ℝ := ε / (ε + ‖x - y‖)
b : ℝ := ‖x - y‖ / (ε + ‖x - y‖)
hab : a + b = 1
hxyz : x = a • y + b • z
⊢ ε * (f x - f y) ≤ ‖x - y‖ * (2 * M)
have ε₁ : ε * (f x - f y) ≤ ‖x - y‖ * (f z - f x)
Tactic: calc
      ε * (f x - f y) ≤ ‖x - y‖ * (f z - f x) := by
        have h := hf.2 hy' hz (by positivity) (by positivity) hab
        simp only [← hxyz, smul_eq_mul, a, b] at h
        field_simp at h
        linear_combination h
      _ ≤ _ := by
        rw [sub_eq_add_neg (f _), two_mul]
        gcongr
        · exact (le_abs_self _).trans <| hM _ hz
        · exact (neg_le_abs _).trans <| hM _ hx'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
x y : E
hx : x ∈ ball x₀ (r - ε)
hy : y ∈ ball x₀ (r - ε)
hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r
hx' : x ∈ ball x₀ r
hy' : y ∈ ball x₀ r
z : E := x + (ε / ‖x - y‖) • (x - y)
hxy : 0 < ‖x - y‖
hz : z ∈ ball x₀ r
a : ℝ := ε / (ε + ‖x - y‖)
b : ℝ := ‖x - y‖ / (ε + ‖x - y‖)
hab : a + b = 1
hxyz : x = a • y + b • z
ε₁ : ε * (f x - f y) ≤ ‖x - y‖ * (f z - f x)
⊢ ε * (f x - f y) ≤ ‖x - y‖ * (2 * M)
have ε₂ : ‖x - y‖ * (f z - f x) ≤ ‖x - y‖ * (2 * M)
Tactic: calc
      ε * (f x - f y) ≤ ‖x - y‖ * (f z - f x) := by
        have h := hf.2 hy' hz (by positivity) (by positivity) hab
        simp only [← hxyz, smul_eq_mul, a, b] at h
        field_simp at h
        linear_combination h
      _ ≤ _ := by
        rw [sub_eq_add_neg (f _), two_mul]
        gcongr
        · exact (le_abs_self _).trans <| hM _ hz
        · exact (neg_le_abs _).trans <| hM _ hx'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
⊢ LipschitzOnWith K.toNNReal f (ball x₀ (r - ε))
have oneside : ∀ {x y : E} (hx : x ∈ ball x₀ (r - ε)) (hy : y ∈ ball x₀ (r - ε)), f x - f y ≤ K * ‖x - y‖
Tactic: have oneside {x y : E} (hx : x ∈ ball x₀ (r - ε)) (hy : y ∈ ball x₀ (r - ε)) :
      f x - f y ≤ K * ‖x - y‖ := by
    obtain rfl | hxy := eq_or_ne x y
    · simp
    have hx₀r : ball x₀ (r - ε) ⊆ ball x₀ r := ball_subset_ball <| by linarith
    have hx' : x ∈ ball x₀ r := hx₀r hx
    have hy' : y ∈ ball x₀ r := hx₀r hy
    let z := x + (ε / ‖x - y‖) • (x - y)
    replace hxy : 0 < ‖x - y‖ := by rwa [norm_sub_pos_iff]
    have hz : z ∈ ball x₀ r := mem_ball_iff_norm.2 <| by
      calc
        _ = ‖(x - x₀) + (ε / ‖x - y‖) • (x - y)‖ := by simp only [z, add_sub_right_comm]
        _ ≤ ‖x - x₀‖ + ‖(ε / ‖x - y‖) • (x - y)‖ := norm_add_le ..
        _ < r - ε + ε :=
          add_lt_add_of_lt_of_le (mem_ball_iff_norm.1 hx) <| by
            simp [norm_smul, abs_of_nonneg, hε.le, hxy.ne']
        _ = r := by simp
    let a := ε / (ε + ‖x - y‖)
    let b := ‖x - y‖ / (ε + ‖x - y‖)
    have hab : a + b = 1 := by simp [field, a, b]
    have hxyz : x = a • y + b • z := by
      calc
        x = a • x + b • x := by rw [Convex.combo_self hab]
        _ = a • y + b • z := by simp [z, a, b, smul_smul, hxy.ne', smul_sub]; abel
    rw [hK, mul_comm, ← mul_div_assoc, le_div_iff₀' hε]
    calc
      ε * (f x - f y) ≤ ‖x - y‖ * (f z - f x) := by
        have h := hf.2 hy' hz (by positivity) (by positivity) hab
        simp only [← hxyz, smul_eq_mul, a, b] at h
        field_simp at h
        linear_combination h
      _ ≤ _ := by
        rw [sub_eq_add_neg (f _), two_mul]
        gcongr
        · exact (le_abs_self _).trans <| hM _ hz
        · exact (neg_le_abs _).trans <| hM _ hx'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
oneside : ∀ {x y : E} (hx : x ∈ ball x₀ (r - ε)) (hy : y ∈ ball x₀ (r - ε)), f x - f y ≤ K * ‖x - y‖
⊢ LipschitzOnWith K.toNNReal f (ball x₀ (r - ε))
have refine : ∀ (x : E) (hx : x ∈ ball x₀ (r - ε)) (y : E) (hy : y ∈ ball x₀ (r - ε)), dist (f x) (f y) ≤ K * dist x y
Tactic: refine .of_dist_le' fun x hx y hy ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
K : ℝ := 2 * M / ε
hK : K = 2 * M / ε
oneside : ∀ {x y : E} (hx : x ∈ ball x₀ (r - ε)) (hy : y ∈ ball x₀ (r - ε)), f x - f y ≤ K * ‖x - y‖
x : E
hx : x ∈ ball x₀ (r - ε)
y : E
hy : y ∈ ball x₀ (r - ε)
⊢ dist (f x) (f y) ≤ K * dist x y
have simp_rw : f x - f y ≤ K * ‖x - y‖ ∧ f y - f x ≤ K * ‖x - y‖
Tactic: simp_rw [dist_eq_norm_sub, Real.norm_eq_abs, abs_sub_le_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hr : r' < r
hf' : IsBounded (f '' ball x₀ r)
⊢ ∃ (K : NNReal), LipschitzOnWith K f (ball x₀ r')
have hf'₁ : ∃ (r_1 : ℝ), f '' ball x₀ r ⊆ ball 0 r_1
Tactic: rw [isBounded_iff_subset_ball 0] at hf'
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hr : r' < r
hf' : ∃ (r_1 : ℝ), f '' ball x₀ r ⊆ ball 0 r_1
⊢ ∃ (K : NNReal), LipschitzOnWith K f (ball x₀ r')
have hf'₁ : ∃ (r_1 : ℝ), ∀ (a : E), dist a x₀ < r → |f a| < r_1
Tactic: simp only [Set.subset_def, mem_image, mem_ball, dist_zero_right, Real.norm_eq_abs,
    forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at hf'
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hr : r' < r
hf' : ∃ (r_1 : ℝ), ∀ (a : E), dist a x₀ < r → |f a| < r_1
⊢ ∃ (K : NNReal), LipschitzOnWith K f (ball x₀ r')
have obtain : ∀ (M : ℝ) (hM : ∀ (a : E), dist a x₀ < r → |f a| < M), ∃ (K : NNReal), LipschitzOnWith K f (ball x₀ r')
Tactic: obtain ⟨M, hM⟩ := hf'
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConvexOn ℝ (ball x₀ r) f
hr : r' < r
M : ℝ
hM : ∀ (a : E), dist a x₀ < r → |f a| < M
⊢ ∃ (K : NNReal), LipschitzOnWith K f (ball x₀ r')
have rw : ∃ (K : NNReal), LipschitzOnWith K f (ball x₀ (r - (r - r')))
Tactic: rw [← sub_sub_cancel r r']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hr : r' < r
hf' : IsBounded (f '' ball x₀ r)
⊢ IsBounded ((-f) '' ball x₀ r)
have h : (-f) '' ball x₀ r = -f '' ball x₀ r
Tactic: convert! hf'.neg
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hr : r' < r
hf' : IsBounded (f '' ball x₀ r)
⊢ (-f) '' ball x₀ r = -f '' ball x₀ r
have h : ∀ (x : ℝ), x ∈ (-f) '' ball x₀ r ↔ x ∈ -f '' ball x₀ r
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
r r' : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hr : r' < r
hf' : IsBounded (f '' ball x₀ r)
⊢ ∃ (K : NNReal), LipschitzOnWith K f (ball x₀ r')
have hf'₁ : IsBounded ((-f) '' ball x₀ r)
Tactic: replace hf' : IsBounded ((-f) '' ball x₀ r) := by convert! hf'.neg; ext; simp [neg_eq_iff_eq_neg]
Cleared hypotheses: hf'
-- 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 → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
⊢ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f| ↔
    Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
have refine : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f →
  Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|
Tactic: refine ⟨fun h ↦ h.mono_le <| .of_forall fun x ↦ le_abs_self _, ?_⟩
-- 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 → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r
⊢ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|
have refine : ∀ᶠ (x : ℝ) in Filter.map |f| (𝓝 x₀), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x (|r| + 2 * |f x₀|)
Tactic: refine ⟨|r| + 2 * |f x₀|, ?_⟩
-- 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 → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r
⊢ ∀ᶠ (x : ℝ) in Filter.map |f| (𝓝 x₀), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x (|r| + 2 * |f x₀|)
have this : Filter.Tendsto (fun (y : E) ↦ HSMul.hSMul (α := ℕ) 2 x₀ - y) (𝓝 x₀) (𝓝 x₀)
Tactic: have : (𝓝 x₀).Tendsto (fun y => 2 • x₀ - y) (𝓝 x₀) :=
    tendsto_nhds_nhds.2 (⟨·, ·, by simp [two_nsmul, dist_comm]⟩)
-- 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 → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r
this : Filter.Tendsto (fun (y : E) ↦ HSMul.hSMul (α := ℕ) 2 x₀ - y) (𝓝 x₀) (𝓝 x₀)
⊢ ∀ᶠ (x : ℝ) in Filter.map |f| (𝓝 x₀), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x (|r| + 2 * |f x₀|)
have simp : ∀ (hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r), ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ |r| + 2 * |f x₀| ∧ -f a ≤ |r| + 2 * |f x₀|
Tactic: simp only [Filter.eventually_map, Pi.abs_apply, abs_le'] 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 → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun (y : E) ↦ HSMul.hSMul (α := ℕ) 2 x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
⊢ ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ |r| + 2 * |f x₀| ∧ -f a ≤ |r| + 2 * |f x₀|
have h : ∀ (y : E) (hx : HSMul.hSMul (α := ℕ) 2 x₀ - y ∈ C) (hx' : y ∈ C) (hfr : f y ≤ r)
  (hfr' : f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ r), f y ≤ |r| + 2 * |f x₀| ∧ -f y ≤ |r| + 2 * |f x₀|
Tactic: filter_upwards [this.eventually_mem hC, hC, hr, this.eventually hr] with y hx hx' hfr hfr'
-- 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 → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun (y : E) ↦ HSMul.hSMul (α := ℕ) 2 x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : HSMul.hSMul (α := ℕ) 2 x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ r
⊢ f y ≤ |r| + 2 * |f x₀| ∧ -f y ≤ |r| + 2 * |f x₀|
have h : -f y ≤ |r| + 2 * |f x₀|
Tactic: refine ⟨hfr.trans <| (le_abs_self _).trans <| by simp, ?_⟩
-- 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 → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun (y : E) ↦ HSMul.hSMul (α := ℕ) 2 x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : HSMul.hSMul (α := ℕ) 2 x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ r
⊢ -f y ≤ |r| + 2 * |f x₀|
have h : -|2 * f x₀| ≤ f y + |r|
Tactic: rw [← sub_le_iff_le_add, neg_sub_comm, sub_le_iff_le_add', ← abs_two, ← abs_mul]
-- 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 → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun (y : E) ↦ HSMul.hSMul (α := ℕ) 2 x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : HSMul.hSMul (α := ℕ) 2 x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ r
⊢ 2 * f x₀ ≤ f y + f (HSMul.hSMul (α := ℕ) 2 x₀ - y)
have this₁ : f ((1 / 2) • y + (1 / 2) • (HSMul.hSMul (α := ℕ) 2 x₀ - y)) ≤
  (1 / 2) • f y + (1 / 2) • f (HSMul.hSMul (α := ℕ) 2 x₀ - y)
Tactic: have := hf.2 hx' hx (by positivity) (by positivity) (add_halves _)
-- 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 → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this_1 : Filter.Tendsto (fun (y : E) ↦ HSMul.hSMul (α := ℕ) 2 x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : HSMul.hSMul (α := ℕ) 2 x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ r
this :
  f ((1 / 2) • y + (1 / 2) • (HSMul.hSMul (α := ℕ) 2 x₀ - y)) ≤
    (1 / 2) • f y + (1 / 2) • f (HSMul.hSMul (α := ℕ) 2 x₀ - y)
⊢ 2 * f x₀ ≤ f y + f (HSMul.hSMul (α := ℕ) 2 x₀ - y)
have this₁ : f x₀ ≤ 2⁻¹ * f y + 2⁻¹ * f (HSMul.hSMul (α := ℝ) 2 x₀ - y)
Tactic: simp only [one_div, ← Nat.cast_smul_eq_nsmul ℝ, Nat.cast_ofNat, smul_sub, ne_eq,
        OfNat.ofNat_ne_zero, not_false_eq_true, inv_smul_smul₀, add_sub_cancel, smul_eq_mul] at this
Cleared hypotheses: this
-- 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 → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this_1 : Filter.Tendsto (fun (y : E) ↦ HSMul.hSMul (α := ℕ) 2 x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : HSMul.hSMul (α := ℕ) 2 x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ r
this : f x₀ ≤ 2⁻¹ * f y + 2⁻¹ * f (HSMul.hSMul (α := ℝ) 2 x₀ - y)
⊢ 2 * f x₀ ≤ f y + f (HSMul.hSMul (α := ℕ) 2 x₀ - y)
have this₁ : 2 * f x₀ ≤ f y + f (HSMul.hSMul (α := ℝ) 2 x₀ - y)
Tactic: cancel_denoms at this
Cleared hypotheses: this
-- 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 → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this_1 : Filter.Tendsto (fun (y : E) ↦ HSMul.hSMul (α := ℕ) 2 x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : HSMul.hSMul (α := ℕ) 2 x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ r
this : 2 * f x₀ ≤ f y + f (HSMul.hSMul (α := ℝ) 2 x₀ - y)
⊢ 2 * f x₀ ≤ f y + f (HSMul.hSMul (α := ℕ) 2 x₀ - y)
have rwa : ∀ (this : (↑2 : ℝ) * f x₀ ≤ f y + f (HSMul.hSMul (α := ℝ) (↑2 : ℝ) x₀ - y)),
  2 * f x₀ ≤ f y + f (HSMul.hSMul (α := ℕ) 2 x₀ - y)
Tactic: rwa [← Nat.cast_two, Nat.cast_smul_eq_nsmul] at this
Cleared hypotheses: this
-- 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 → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this_1 : Filter.Tendsto (fun (y : E) ↦ HSMul.hSMul (α := ℕ) 2 x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : HSMul.hSMul (α := ℕ) 2 x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ r
this : 2 * f x₀ ≤ f y + f (HSMul.hSMul (α := ℝ) 2 x₀ - y)
rwa :
  ∀ (this : (↑2 : ℝ) * f x₀ ≤ f y + f (HSMul.hSMul (α := ℝ) (↑2 : ℝ) x₀ - y)),
    2 * f x₀ ≤ f y + f (HSMul.hSMul (α := ℕ) 2 x₀ - y)
⊢ 2 * f x₀ ≤ f y + f (HSMul.hSMul (α := ℕ) 2 x₀ - y)
have rwa₁ : ∀ (this : (↑2 : ℝ) * f x₀ ≤ f y + f (HSMul.hSMul (α := ℕ) 2 x₀ - y)), 2 * f x₀ ≤ f y + f (HSMul.hSMul (α := ℕ) 2 x₀ - y)
Tactic: rwa [← Nat.cast_two, Nat.cast_smul_eq_nsmul] at this
Cleared hypotheses: this
-- 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 → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun (y : E) ↦ HSMul.hSMul (α := ℕ) 2 x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : HSMul.hSMul (α := ℕ) 2 x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ r
⊢ f y + f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ f y + |r|
have bc : f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ |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 → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun (y : E) ↦ HSMul.hSMul (α := ℕ) 2 x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : HSMul.hSMul (α := ℕ) 2 x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ r
⊢ -|2 * f x₀| ≤ f y + |r|
have f₁ : 2 * f x₀ ≤ f y + f (HSMul.hSMul (α := ℕ) 2 x₀ - y)
Tactic: calc
    -|2 * f x₀| ≤ 2 * f x₀ := neg_abs_le _
    _ ≤ f y + f (2 • x₀ - y) := by
      have := hf.2 hx' hx (by positivity) (by positivity) (add_halves _)
      simp only [one_div, ← Nat.cast_smul_eq_nsmul ℝ, Nat.cast_ofNat, smul_sub, ne_eq,
        OfNat.ofNat_ne_zero, not_false_eq_true, inv_smul_smul₀, add_sub_cancel, smul_eq_mul] at this
      cancel_denoms at this
      rwa [← Nat.cast_two, Nat.cast_smul_eq_nsmul] at this
    _ ≤ f y + |r| := by gcongr; exact hfr'.trans (le_abs_self _)
-- 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 → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun (y : E) ↦ HSMul.hSMul (α := ℕ) 2 x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : HSMul.hSMul (α := ℕ) 2 x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ r
f₁ : 2 * f x₀ ≤ f y + f (HSMul.hSMul (α := ℕ) 2 x₀ - y)
⊢ -|2 * f x₀| ≤ f y + |r|
have f₂ : f y + f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ f y + |r|
Tactic: calc
    -|2 * f x₀| ≤ 2 * f x₀ := neg_abs_le _
    _ ≤ f y + f (2 • x₀ - y) := by
      have := hf.2 hx' hx (by positivity) (by positivity) (add_halves _)
      simp only [one_div, ← Nat.cast_smul_eq_nsmul ℝ, Nat.cast_ofNat, smul_sub, ne_eq,
        OfNat.ofNat_ne_zero, not_false_eq_true, inv_smul_smul₀, add_sub_cancel, smul_eq_mul] at this
      cancel_denoms at this
      rwa [← Nat.cast_two, Nat.cast_smul_eq_nsmul] at this
    _ ≤ f y + |r| := by gcongr; exact hfr'.trans (le_abs_self _)
-- 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
⊢ [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_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
Tactic: tfae_have 1 → 2 := LocallyLipschitzOn.continuousOn
-- 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
⊢ ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
have obtain : ∀ (x₀ : E) (hx₀ : x₀ ∈ C) (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
Tactic: obtain ⟨x₀, hx₀⟩ := hC'
Cleared hypotheses: hC'
-- 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
⊢ [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_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
Tactic: tfae_have 2 → 3 := by
    obtain ⟨x₀, hx₀⟩ := hC'
    exact fun h ↦ ⟨x₀, hx₀, h.continuousAt <| hC.mem_nhds hx₀⟩
-- 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₀
⊢ [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_3_to_4 : ∀ (a : ∃ x₀ ∈ C, ContinuousAt f x₀), ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
Tactic: tfae_have 3 → 4
  | ⟨x₀, hx₀, h⟩ =>
    ⟨x₀, hx₀, f x₀ + 1, by simpa using h.eventually (eventually_le_nhds (by simp))⟩
-- 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
⊢ ContinuousAt.{0, u_1} (Y := E) (fun (δ : ℝ) ↦ (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀) 0
have funProp : HSub.hSub (α := ℝ) 1 0 ≠ 0
Tactic: fun_prop (disch := norm_num)
-- 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
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀ ∈ C
have h : ContinuousAt.{0, u_1} (Y := E) (fun (δ : ℝ) ↦ (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀) 0
Tactic: have h : ContinuousAt (fun δ : ℝ ↦ (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀) 0 := by
        fun_prop (disch := norm_num)