awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Continuous
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
h : f x * (ε + ‖x - y‖) ≤ ε * f y + ‖x - y‖ * f z
⊢ ε * (f x - f y) ≤ ‖x - y‖ * (f z - f x)

Tactic:
linear_combination h
-- Module: Mathlib.Analysis.Convex.Continuous
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
rw : ‖x - y‖ * (f z + -f x) ≤ ‖x - y‖ * (M + M)
⊢ ‖x - y‖ * (f z - f x) ≤ ‖x - y‖ * (2 * M)

Tactic:
rw [sub_eq_add_neg (f _), two_mul]

Premises used: sub_eq_add_neg, two_mul
-- Module: Mathlib.Analysis.Convex.Continuous
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
hbc : f z ≤ M
hbc₁ : -f x ≤ M
⊢ ‖x - y‖ * (f z + -f x) ≤ ‖x - y‖ * (M + M)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Continuous
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 z ≤ M

Tactic:
(le_abs_self _).trans <| hM _ hz

Premises used: le_abs_self, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Continuous
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 z ≤ M

Tactic:
exact (le_abs_self _).trans <| hM _ hz

Premises used: le_abs_self, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Continuous
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 ≤ M

Tactic:
(neg_le_abs _).trans <| hM _ hx'

Premises used: neg_le_abs, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Continuous
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 ≤ M

Tactic:
exact (neg_le_abs _).trans <| hM _ hx'

Premises used: neg_le_abs, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Continuous
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)
ε₂ : ‖x - y‖ * (f z - f x) ≤ ‖x - y‖ * (2 * M)
⊢ ε * (f x - f y) ≤ ‖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'

Premises used: HSub.hSub
-- Module: Mathlib.Analysis.Convex.Continuous
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 - ε)), 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'
-- Module: Mathlib.Analysis.Convex.Continuous
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 - ε))

Tactic:
.of_dist_le' fun x hx y hy ↦ ?_

Premises used: LipschitzOnWith.of_dist_le'
-- Module: Mathlib.Analysis.Convex.Continuous
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‖
refine : ∀ (x : E) (hx : x ∈ ball x₀ (r - ε)) (y : E) (hy : y ∈ ball x₀ (r - ε)), dist (f x) (f y) ≤ K * dist x y
⊢ LipschitzOnWith K.toNNReal f (ball x₀ (r - ε))

Tactic:
refine .of_dist_le' fun x hx y hy ↦ ?_
-- Module: Mathlib.Analysis.Convex.Continuous
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 - ε)
simp_rw : f x - f y ≤ K * ‖x - y‖ ∧ f y - f x ≤ K * ‖x - y‖
⊢ dist (f x) (f y) ≤ K * dist x y

Tactic:
simp_rw [dist_eq_norm_sub, Real.norm_eq_abs, abs_sub_le_iff]

Premises used: dist_eq_norm_sub, abs_sub_le_iff, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Convex.Continuous
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 - ε)
⊢ f x - f y ≤ K * ‖x - y‖ ∧ f y - f x ≤ K * ‖x - y‖

Tactic:
⟨oneside hx hy, norm_sub_rev x _ ▸ oneside hy hx⟩

Premises used: Eq.rec, And.intro, norm_sub_rev, Eq.symm
-- Module: Mathlib.Analysis.Convex.Continuous
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 - ε)
⊢ f x - f y ≤ K * ‖x - y‖ ∧ f y - f x ≤ K * ‖x - y‖

Tactic:
exact ⟨oneside hx hy, norm_sub_rev x _ ▸ oneside hy hx⟩
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
⊢ ∀ (a : E), dist a x₀ < r → |(-f) a| ≤ M

Tactic:
simpa using hM
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x₀ : E
ε r M : ℝ
hf : ConcaveOn ℝ (ball x₀ r) f
hε : 0 < ε
hM : ∀ (a : E), dist a x₀ < r → |f a| ≤ M
⊢ LipschitzOnWith (2 * M / ε).toNNReal f (ball x₀ (r - ε))

Tactic:
simpa using hf.neg.lipschitzOnWith_of_abs_le hε <| by simpa using hM

Premises used: ConcaveOn.neg, ConvexOn.lipschitzOnWith_of_abs_le
-- Module: Mathlib.Analysis.Convex.Continuous
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)
⊢ ∃ (r_1 : ℝ), f '' ball x₀ r ⊆ ball 0 r_1

Tactic:
rw [isBounded_iff_subset_ball 0] at hf'

Premises used: Metric.isBounded_iff_subset_ball, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Continuous
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
⊢ ∃ (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'

Premises used: Set.subset_def, and_imp, Set.mem_image, forall_exists_index, Metric.mem_ball, dist_zero_right, forall_apply_eq_imp_iff₂, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Convex.Continuous
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
obtain : ∀ (M : ℝ) (hM : ∀ (a : E), dist a x₀ < r → |f a| < M), ∃ (K : NNReal), LipschitzOnWith K f (ball x₀ r')
⊢ ∃ (K : NNReal), LipschitzOnWith K f (ball x₀ r')

Tactic:
obtain ⟨M, hM⟩ := hf'
-- Module: Mathlib.Analysis.Convex.Continuous
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
rw : ∃ (K : NNReal), LipschitzOnWith K f (ball x₀ (r - (r - r')))
⊢ ∃ (K : NNReal), LipschitzOnWith K f (ball x₀ r')

Tactic:
rw [← sub_sub_cancel r r']

Premises used: sub_sub_cancel
-- Module: Mathlib.Analysis.Convex.Continuous
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 - (r - r')))

Tactic:
⟨_, hf.lipschitzOnWith_of_abs_le (sub_pos.2 hr) fun a ha ↦ (hM a ha).le⟩

Premises used: Iff.mpr, sub_pos, LT.lt.le, Exists.intro, ConvexOn.lipschitzOnWith_of_abs_le
-- Module: Mathlib.Analysis.Convex.Continuous
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 - (r - r')))

Tactic:
exact ⟨_, hf.lipschitzOnWith_of_abs_le (sub_pos.2 hr) fun a ha ↦ (hM a ha).le⟩
-- Module: Mathlib.Analysis.Convex.Continuous
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)

Tactic:
hf'.neg

Premises used: Bornology.IsBounded.neg
-- Module: Mathlib.Analysis.Convex.Continuous
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)
h : (-f) '' ball x₀ r = -f '' ball x₀ r
⊢ IsBounded ((-f) '' ball x₀ r)

Tactic:
convert! hf'.neg

Premises used: Bornology.IsBounded.neg
-- Module: Mathlib.Analysis.Convex.Continuous
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)
h : ∀ (x : ℝ), x ∈ (-f) '' ball x₀ r ↔ x ∈ -f '' ball x₀ r
⊢ (-f) '' ball x₀ r = -f '' ball x₀ r

Tactic:
ext
-- Module: Mathlib.Analysis.Convex.Continuous
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)
x : ℝ
⊢ x ∈ (-f) '' ball x₀ r ↔ x ∈ -f '' ball x₀ r

Tactic:
simp [neg_eq_iff_eq_neg]

Premises used: neg_eq_iff_eq_neg
-- Module: Mathlib.Analysis.Convex.Continuous
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)

Tactic:
replace hf' : IsBounded ((-f) '' ball x₀ r) := by convert! hf'.neg; ext; simp [neg_eq_iff_eq_neg]
-- Module: Mathlib.Analysis.Convex.Continuous
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')

Tactic:
simpa using hf.neg.exists_lipschitzOnWith_of_isBounded hr hf'

Premises used: ConcaveOn.neg, ConvexOn.exists_lipschitzOnWith_of_isBounded
-- Module: Mathlib.Analysis.Convex.Continuous
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

Tactic:
⟨fun h ↦ h.mono_le <| .of_forall fun x ↦ le_abs_self _, ?_⟩

Premises used: le_abs_self, Filter.IsBoundedUnder.mono_le, Filter.Eventually.of_forall, Iff.intro
-- Module: Mathlib.Analysis.Convex.Continuous
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₀
refine :
  Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f →
    Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|
⊢ 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 _, ?_⟩
-- Module: Mathlib.Analysis.Convex.Continuous
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|

Tactic:
⟨|r| + 2 * |f x₀|, ?_⟩

Premises used: HMul.hMul, abs, Filter.IsBounded, HAdd.hAdd, Exists.intro, OfNat.ofNat, Filter.IsBoundedUnder
-- Module: Mathlib.Analysis.Convex.Continuous
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
refine : ∀ᶠ (x : ℝ) in Filter.map |f| (𝓝 x₀), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x (|r| + 2 * |f x₀|)
⊢ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|

Tactic:
refine ⟨|r| + 2 * |f x₀|, ?_⟩
-- Module: Mathlib.Analysis.Convex.Continuous
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.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]⟩)
-- Module: Mathlib.Analysis.Convex.Continuous
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₀)
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₀|
⊢ ∀ᶠ (x : ℝ) in Filter.map |f| (𝓝 x₀), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x (|r| + 2 * |f x₀|)

Tactic:
simp only [Filter.eventually_map, Pi.abs_apply, abs_le'] at hr ⊢

Premises used: Pi.abs_apply, Filter.eventually_map, abs_le'
-- Module: Mathlib.Analysis.Convex.Continuous
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
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₀|
⊢ ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ |r| + 2 * |f x₀| ∧ -f a ≤ |r| + 2 * |f x₀|

Tactic:
filter_upwards [this.eventually_mem hC, hC, hr, this.eventually hr] with y hx hx' hfr hfr'

Premises used: Filter.Tendsto.eventually_mem, Filter.Tendsto.eventually
-- Module: Mathlib.Analysis.Convex.Continuous
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
⊢ |r| ≤ |r| + 2 * |f x₀|

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Continuous
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
h : -f y ≤ |r| + 2 * |f x₀|
⊢ f y ≤ |r| + 2 * |f x₀| ∧ -f y ≤ |r| + 2 * |f x₀|

Tactic:
refine ⟨hfr.trans <| (le_abs_self _).trans <| by simp, ?_⟩
-- Module: Mathlib.Analysis.Convex.Continuous
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
h : -|2 * f x₀| ≤ f y + |r|
⊢ -f y ≤ |r| + 2 * |f x₀|

Tactic:
rw [← sub_le_iff_le_add, neg_sub_comm, sub_le_iff_le_add', ← abs_two, ← abs_mul]

Premises used: abs_mul, neg_sub_comm, sub_le_iff_le_add, sub_le_iff_le_add', abs_two
-- Module: Mathlib.Analysis.Convex.Continuous
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₀| ≤ 2 * f x₀

Tactic:
neg_abs_le _

Premises used: neg_abs_le
-- Module: Mathlib.Analysis.Convex.Continuous
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
⊢ 0 ≤ 1 / 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Continuous
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 ((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 _)
-- Module: Mathlib.Analysis.Convex.Continuous
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)
⊢ 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

Premises used: Nat.cast_ofNat, inv_smul_smul₀, Real, OfNat.ofNat_ne_zero, ne_eq, smul_sub, add_sub_cancel, one_div, Nat.cast_smul_eq_nsmul, smul_eq_mul, not_false_eq_true