-- Mathlib/Analysis/Convex/Continuous.lean
lemma ConvexOn.isBoundedUnder_abs (hf : ConvexOn ℝ C f) {x₀ : E} (hC : C ∈ 𝓝 x₀) :
    (𝓝 x₀).IsBoundedUnder (· ≤ ·) |f| ↔ (𝓝 x₀).IsBoundedUnder (· ≤ ·) f

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this✝ : Filter.Tendsto (fun y => 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
this : f ((1 / 2) • y + (1 / 2) • (2 • x₀ - y)) ≤ (1 / 2) • f y + (1 / 2) • f (2 • x₀ - y)
⊢ 2 * f x₀ ≤ f y + f (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

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this✝ : Filter.Tendsto (fun y => 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
this : f x₀ ≤ 2⁻¹ * f y + 2⁻¹ * f (2 • x₀ - y)
⊢ 2 * f x₀ ≤ f y + f (2 • x₀ - y)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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:
rintro ⟨r, hr⟩

Result:
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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|

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun y => 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
⊢ |r| ≤ |r| + 2 * |f x₀|

Tactic:
simp

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun y => 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
⊢ 0 ≤ 1 / 2

Tactic:
positivity

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun y => 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
⊢ 2 * f x₀ ≤ f y + f (2 • x₀ - y)

Tactic:
have := hf.2 hx' hx (by positivity) (by positivity) (add_halves _)

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this✝ : Filter.Tendsto (fun y => 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
this : f ((1 / 2) • y + (1 / 2) • (2 • x₀ - y)) ≤ (1 / 2) • f y + (1 / 2) • f (2 • x₀ - y)
⊢ 2 * f x₀ ≤ f y + f (2 • x₀ - y)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
x1✝ : ℝ
x2✝ : x1✝ > 0
⊢ ∀ ⦃x : E⦄, dist x x₀ < x1✝ → dist (2 • x₀ - x) x₀ < x1✝

Tactic:
simp [two_nsmul, dist_comm]

Result:
no goals

Proof state:
case bc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun y => 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
⊢ f (2 • x₀ - y) ≤ |r|

Tactic:
exact hfr'.trans (le_abs_self _)

Result:
no goals

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun y => 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - 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]

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun y => 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
⊢ -|2 * f x₀| ≤ f y + |r|

Proof state:
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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:
refine ⟨|r| + 2 * |f x₀|, ?_⟩

Result:
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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₀|)

Proof state:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun y => 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
⊢ f y ≤ |r| + 2 * |f x₀| ∧ -f y ≤ |r| + 2 * |f x₀|

Tactic:
refine ⟨hfr.trans <| (le_abs_self _).trans <| by simp, ?_⟩

Result:
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun y => 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
⊢ -f y ≤ |r| + 2 * |f x₀|

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun y => 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
⊢ f y + f (2 • x₀ - y) ≤ f y + |r|

Tactic:
gcongr

Result:
case bc
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun y => 2 • x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : 2 • x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (2 • x₀ - y) ≤ r
⊢ f (2 • x₀ - y) ≤ |r|

Proof state:
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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 => 2 • x₀ - y) (𝓝 x₀) (𝓝 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 ⊢

Result:
case intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun y => 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₀|