awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
refine :
  ∀ (x : E) (hx : x ∈ s) (y : E) (hy : y ∈ s) (hxy : x ≠ y) (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1),
    0 < a * b * φ ‖x - y‖
⊢ StrictConvexOn ℝ s f

Tactic:
refine ⟨hf.1, fun x hx y hy hxy a b ha hb hab ↦ (hf.2 hx hy ha.le hb.le hab).trans_lt <|
    sub_lt_self _ ?_⟩
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
rw : ∀ (hxy : 0 < ‖x - y‖) (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1), 0 < a * b * φ ‖x - y‖
⊢ 0 < a * b * φ ‖x - y‖

Tactic:
rw [← sub_ne_zero, ← norm_pos_iff] at hxy

Premises used: norm_pos_iff, sub_ne_zero
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : 0 < ‖x - y‖
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
positivity positivity₁ positivity₂ positivity₃ : 0 < φ ‖x - y‖ → 0 < a * b * φ ‖x - y‖
⊢ 0 < a * b * φ ‖x - y‖

Tactic:
positivity [hφ _ hxy.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
⊢ StrictConcaveOn ℝ s f

Tactic:
⟨hf.1, fun x hx y hy hxy a b ha hb hab ↦ (hf.2 hx hy ha.le hb.le hab).trans_lt' <|
    lt_add_of_pos_right _ ?_⟩

Premises used: StrictConcaveOn, lt_add_of_pos_right, LT.lt.le, And.right, LE.le.trans_lt', And.left, HAdd.hAdd, And.intro, HSMul.hSMul
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
refine :
  ∀ (x : E) (hx : x ∈ s) (y : E) (hy : y ∈ s) (hxy : x ≠ y) (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1),
    0 < a * b * φ ‖x - y‖
⊢ StrictConcaveOn ℝ s f

Tactic:
refine ⟨hf.1, fun x hx y hy hxy a b ha hb hab ↦ (hf.2 hx hy ha.le hb.le hab).trans_lt' <|
    lt_add_of_pos_right _ ?_⟩
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
rw : ∀ (hxy : 0 < ‖x - y‖) (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1), 0 < a * b * φ ‖x - y‖
⊢ 0 < a * b * φ ‖x - y‖

Tactic:
rw [← sub_ne_zero, ← norm_pos_iff] at hxy

Premises used: norm_pos_iff, sub_ne_zero
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
hφ : ∀ (r : ℝ), r ≠ 0 → 0 < φ r
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : 0 < ‖x - y‖
a b : ℝ
ha : 0 < a
hb : 0 < b
hab : a + b = 1
positivity positivity₁ positivity₂ positivity₃ : 0 < φ ‖x - y‖ → 0 < a * b * φ ‖x - y‖
⊢ 0 < a * b * φ ‖x - y‖

Tactic:
positivity [hφ _ hxy.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f g : E → ℝ
hf : UniformConvexOn s φ f
hg : UniformConvexOn s ψ g
⊢ UniformConvexOn s (φ + ψ) (f + g)

Tactic:
⟨hf.1, fun x hx y hy a b ha hb hab ↦ ?_⟩

Premises used: UniformConvexOn, And.left, And.intro
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f g : E → ℝ
hf : UniformConvexOn s φ f
hg : UniformConvexOn s ψ g
refine :
  ∀ (x : E) (hx : x ∈ s) (y : E) (hy : y ∈ s) (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
    (f + g) (a • x + b • y) ≤ a • (f + g) x + b • (f + g) y - a * b * (φ + ψ) ‖x - y‖
⊢ UniformConvexOn s (φ + ψ) (f + g)

Tactic:
refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ ?_⟩
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f g : E → ℝ
hf : UniformConvexOn s φ f
hg : UniformConvexOn s ψ g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (f + g) (a • x + b • y) ≤ a • (f + g) x + b • (f + g) y - a * b * (φ + ψ) ‖x - y‖

Tactic:
simpa [mul_add, add_add_add_comm, sub_add_sub_comm]
    using add_le_add (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab)

Premises used: add_le_add, sub_add_sub_comm, And.right, mul_add, add_add_add_comm
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f g : E → ℝ
hf : UniformConcaveOn s φ f
hg : UniformConcaveOn s ψ g
⊢ UniformConcaveOn s (φ + ψ) (f + g)

Tactic:
⟨hf.1, fun x hx y hy a b ha hb hab ↦ ?_⟩

Premises used: And.left, And.intro, UniformConcaveOn
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f g : E → ℝ
hf : UniformConcaveOn s φ f
hg : UniformConcaveOn s ψ g
refine :
  ∀ (x : E) (hx : x ∈ s) (y : E) (hy : y ∈ s) (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
    a • (f + g) x + b • (f + g) y + a * b * (φ + ψ) ‖x - y‖ ≤ (f + g) (a • x + b • y)
⊢ UniformConcaveOn s (φ + ψ) (f + g)

Tactic:
refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ ?_⟩
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f g : E → ℝ
hf : UniformConcaveOn s φ f
hg : UniformConcaveOn s ψ g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (f + g) x + b • (f + g) y + a * b * (φ + ψ) ‖x - y‖ ≤ (f + g) (a • x + b • y)

Tactic:
simpa [mul_add, add_add_add_comm] using add_le_add (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab)

Premises used: add_le_add, And.right, mul_add, add_add_add_comm
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
⊢ UniformConcaveOn s φ (-f)

Tactic:
⟨hf.1, fun x hx y hy a b ha hb hab ↦ le_of_neg_le_neg ?_⟩

Premises used: le_of_neg_le_neg, And.left, And.intro, UniformConcaveOn
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
refine :
  ∀ (x : E) (hx : x ∈ s) (y : E) (hy : y ∈ s) (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
    -(-f) (a • x + b • y) ≤ -(a • (-f) x + b • (-f) y + a * b * φ ‖x - y‖)
⊢ UniformConcaveOn s φ (-f)

Tactic:
refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ le_of_neg_le_neg ?_⟩
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ -(-f) (a • x + b • y) ≤ -(a • (-f) x + b • (-f) y + a * b * φ ‖x - y‖)

Tactic:
simpa [add_comm, -neg_le_neg_iff, le_sub_iff_add_le'] using hf.2 hx hy ha hb hab

Premises used: le_sub_iff_add_le', add_comm, And.right, neg_le_neg_iff
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
⊢ UniformConvexOn s φ (-f)

Tactic:
⟨hf.1, fun x hx y hy a b ha hb hab ↦ le_of_neg_le_neg ?_⟩

Premises used: le_of_neg_le_neg, UniformConvexOn, And.left, And.intro
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
refine :
  ∀ (x : E) (hx : x ∈ s) (y : E) (hy : y ∈ s) (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
    -(a • (-f) x + b • (-f) y - a * b * φ ‖x - y‖) ≤ -(-f) (a • x + b • y)
⊢ UniformConvexOn s φ (-f)

Tactic:
refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ le_of_neg_le_neg ?_⟩
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ -(a • (-f) x + b • (-f) y - a * b * φ ‖x - y‖) ≤ -(-f) (a • x + b • y)

Tactic:
simpa [add_comm, -neg_le_neg_iff, ← le_sub_iff_add_le', sub_eq_add_neg, neg_add]
    using hf.2 hx hy ha hb hab

Premises used: sub_eq_add_neg, le_sub_iff_add_le', neg_add, add_comm, And.right, neg_le_neg_iff
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f g : E → ℝ
hf : UniformConvexOn s φ f
hg : UniformConcaveOn s ψ g
⊢ UniformConvexOn s (φ + ψ) (f - g)

Tactic:
simpa using hf.add hg.neg

Premises used: UniformConvexOn.add, UniformConcaveOn.neg
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f g : E → ℝ
hf : UniformConcaveOn s φ f
hg : UniformConvexOn s ψ g
⊢ UniformConcaveOn s (φ + ψ) (f - g)

Tactic:
simpa using hf.add hg.neg

Premises used: UniformConcaveOn.add, UniformConvexOn.neg
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
f : E → ℝ
m n : ℝ
hmn : m ≤ n
hf : StrongConvexOn s n f
r : ℝ
ha : 0 ≤ HPow.hPow (β := ℕ) r 2
hbc : LE.le (α := (fun (a : ℝ) ↦ ℝ) r) 0 2
⊢ m / 2 * HPow.hPow (β := ℕ) r 2 ≤ n / 2 * HPow.hPow (β := ℕ) r 2

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
f : E → ℝ
m n : ℝ
hmn : m ≤ n
hf : StrongConcaveOn s n f
r : ℝ
ha : 0 ≤ HPow.hPow (β := ℕ) r 2
hbc : LE.le (α := (fun (a : ℝ) ↦ ℝ) r) 0 2
⊢ m / 2 * HPow.hPow (β := ℕ) r 2 ≤ n / 2 * HPow.hPow (β := ℕ) r 2

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
f : E → ℝ
⊢ StrongConvexOn s 0 f ↔ ConvexOn ℝ s f

Tactic:
simp [StrongConvexOn, ← Pi.zero_def]

Premises used: Pi.zero_def, StrongConvexOn
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
f : E → ℝ
⊢ StrongConcaveOn s 0 f ↔ ConcaveOn ℝ s f

Tactic:
simp [StrongConcaveOn, ← Pi.zero_def]

Premises used: Pi.zero_def, StrongConcaveOn
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
f : E → ℝ
m : ℝ
hf : StrongConvexOn s m f
hm : 0 < m
r : ℝ
hr : r ≠ 0
⊢ 0 < m / 2 * HPow.hPow (β := ℕ) r 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
f : E → ℝ
m : ℝ
hf : StrongConcaveOn s m f
hm : 0 < m
r : ℝ
hr : r ≠ 0
⊢ 0 < m / 2 * HPow.hPow (β := ℕ) r 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
a b m : ℝ
x y : E
f : E → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
rw :
  a * (f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b * (f y - m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) +
      m / 2 *
        (HPow.hPow (β := ℕ) a 2 * HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * (a * (b * inner ℝ x y)) +
          HPow.hPow (β := ℕ) b 2 * HPow.hPow (β := ℕ) ‖y‖ 2) =
    a * f x + b * f y - m / 2 * a * b * (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * inner ℝ x y + HPow.hPow (β := ℕ) ‖y‖ 2)
⊢ a * (f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b * (f y - m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) +
      m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2 =
    a * f x + b * f y - m / 2 * a * b * HPow.hPow (β := ℕ) ‖x - y‖ 2

Tactic:
rw [norm_add_sq_real, norm_sub_sq_real, norm_smul, norm_smul, real_inner_smul_left,
    inner_smul_right, norm_of_nonneg ha, norm_of_nonneg hb, mul_pow, mul_pow]

Premises used: norm_sub_sq_real, norm_smul, inner_smul_right, norm_add_sq_real, real_inner_smul_left, mul_pow, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
a b m : ℝ
x y : E
f : E → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
obtain :
  ∀ (ha : 0 ≤ 1 - b) (hab : 1 - b + b = 1),
    (1 - b) * (f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b * (f y - m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) +
        m / 2 *
          (HPow.hPow (β := ℕ) (1 - b) 2 * HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ((1 - b) * (b * inner ℝ x y)) +
            HPow.hPow (β := ℕ) b 2 * HPow.hPow (β := ℕ) ‖y‖ 2) =
      (1 - b) * f x + b * f y -
        m / 2 * (1 - b) * b * (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * inner ℝ x y + HPow.hPow (β := ℕ) ‖y‖ 2)
⊢ a * (f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b * (f y - m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) +
      m / 2 *
        (HPow.hPow (β := ℕ) a 2 * HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * (a * (b * inner ℝ x y)) +
          HPow.hPow (β := ℕ) b 2 * HPow.hPow (β := ℕ) ‖y‖ 2) =
    a * f x + b * f y - m / 2 * a * b * (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * inner ℝ x y + HPow.hPow (β := ℕ) ‖y‖ 2)

Tactic:
obtain rfl := eq_sub_of_add_eq hab

Premises used: eq_sub_of_add_eq, rfl
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
b m : ℝ
x y : E
f : E → ℝ
hb : 0 ≤ b
ha : 0 ≤ 1 - b
hab : 1 - b + b = 1
⊢ (1 - b) * (f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b * (f y - m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) +
      m / 2 *
        (HPow.hPow (β := ℕ) (1 - b) 2 * HPow.hPow (β := ℕ) ‖x‖ 2 + 2 * ((1 - b) * (b * inner ℝ x y)) +
          HPow.hPow (β := ℕ) b 2 * HPow.hPow (β := ℕ) ‖y‖ 2) =
    (1 - b) * f x + b * f y -
      m / 2 * (1 - b) * b * (HPow.hPow (β := ℕ) ‖x‖ 2 - 2 * inner ℝ x y + HPow.hPow (β := ℕ) ‖y‖ 2)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
a b m : ℝ
x y : E
f : E → ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a * (f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b * (f y + m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) -
      m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2 =
    a * f x + b * f y + m / 2 * a * b * HPow.hPow (β := ℕ) ‖x - y‖ 2

Tactic:
simpa [neg_div] using aux_sub (E := E) (m := -m) ha hb hab

Premises used: neg_div, _private.0.aux_sub
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
⊢ StrongConvexOn s m f ↔ ConvexOn ℝ (β := ℝ) s fun (x : E) ↦ f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
and_congr_right fun _ ↦ forall₄_congr fun x _ y _ ↦ forall₅_congr fun a b ha hb hab ↦ ?_

Premises used: forall₅_congr, and_congr_right, UniformConvexOn, StrongConvexOn, forall₄_congr, ConvexOn
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
refine :
  Convex ℝ s →
    ∀ x ∈ s,
      ∀ y ∈ s,
        ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
          f (a • x + b • y) ≤ a • f x + b • f y - a * b * (fun (r : ℝ) ↦ m / 2 * HPow.hPow (β := ℕ) r 2) ‖x - y‖ ↔
            (fun (x : E) ↦ f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) (a • x + b • y) ≤
              HSMul.hSMul (β := ℝ) a ((fun (x : E) ↦ f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) x) +
                HSMul.hSMul (β := ℝ) b ((fun (x : E) ↦ f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) y)
⊢ StrongConvexOn s m f ↔ ConvexOn ℝ (β := ℝ) s fun (x : E) ↦ f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
refine and_congr_right fun _ ↦ forall₄_congr fun x _ y _ ↦ forall₅_congr fun a b ha hb hab ↦ ?_

Premises used: forall₅_congr, and_congr_right, forall₄_congr
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
h : Convex ℝ s
x : E
h_1 : x ∈ s
y : E
h_2 : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
simp_rw simp_rw₁ :
  f (a • x + b • y) ≤ a • f x + b • f y - a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ↔
    f (a • x + b • y) - m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2 ≤
      a • (f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b • (f y - m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2)
simp_rw₂ :
  f (a • x + b • y) ≤ a • f x + b • f y - a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ↔
    f (a • x + b • y) ≤
      a • (f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b • (f y - m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) +
        m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2
simp_rw₃ :
  f (a • x + b • y) ≤ a * f x + b * f y - a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ↔
    f (a • x + b • y) ≤
      a * (f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b * (f y - m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) +
        m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2
simp_rw₄ :
  f (a • x + b • y) ≤ a * f x + b * f y - a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ↔
    f (a • x + b • y) ≤ a * f x + b * f y - m / 2 * a * b * HPow.hPow (β := ℕ) ‖x - y‖ 2
simp_rw₅ :
  f (a • x + b • y) ≤ a * f x + b * f y - a * (b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2)) ↔
    f (a • x + b • y) ≤ a * f x + b * f y - m / 2 * (a * (b * HPow.hPow (β := ℕ) ‖x - y‖ 2))
⊢ f (a • x + b • y) ≤ a • f x + b • f y - a * b * (fun (r : ℝ) ↦ m / 2 * HPow.hPow (β := ℕ) r 2) ‖x - y‖ ↔
    (fun (x : E) ↦ f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) (a • x + b • y) ≤
      HSMul.hSMul (β := ℝ) a ((fun (x : E) ↦ f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) x) +
        HSMul.hSMul (β := ℝ) b ((fun (x : E) ↦ f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) y)

Tactic:
simp_rw [sub_le_iff_le_add, smul_eq_mul, aux_sub ha hb hab, mul_assoc, mul_left_comm]

Premises used: mul_assoc, sub_le_iff_le_add, _private.0.aux_sub, mul_left_comm, smul_eq_mul
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
⊢ StrongConcaveOn s m f ↔ ConcaveOn ℝ (β := ℝ) s fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
and_congr_right fun _ ↦ forall₄_congr fun x _ y _ ↦ forall₅_congr fun a b ha hb hab ↦ ?_

Premises used: forall₅_congr, StrongConcaveOn, and_congr_right, ConcaveOn, UniformConcaveOn, forall₄_congr
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
refine :
  Convex ℝ s →
    ∀ x ∈ s,
      ∀ y ∈ s,
        ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
          a • f x + b • f y + a * b * (fun (r : ℝ) ↦ m / 2 * HPow.hPow (β := ℕ) r 2) ‖x - y‖ ≤ f (a • x + b • y) ↔
            HSMul.hSMul (β := ℝ) a ((fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) x) +
                HSMul.hSMul (β := ℝ) b ((fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) y) ≤
              (fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) (a • x + b • y)
⊢ StrongConcaveOn s m f ↔ ConcaveOn ℝ (β := ℝ) s fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
refine and_congr_right fun _ ↦ forall₄_congr fun x _ y _ ↦ forall₅_congr fun a b ha hb hab ↦ ?_

Premises used: forall₅_congr, and_congr_right, forall₄_congr
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
h : Convex ℝ s
x : E
h_1 : x ∈ s
y : E
h_2 : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
simp_rw simp_rw₁ :
  a • f x + b • f y + a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ≤ f (a • x + b • y) ↔
    a • (f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b • (f y + m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) ≤
      f (a • x + b • y) + m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2
simp_rw₂ :
  a • f x + b • f y + a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ≤ f (a • x + b • y) ↔
    a • (f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b • (f y + m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) -
        m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2 ≤
      f (a • x + b • y)
simp_rw₃ :
  a * f x + b * f y + a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ≤ f (a • x + b • y) ↔
    a * (f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b * (f y + m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) -
        m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2 ≤
      f (a • x + b • y)
simp_rw₄ :
  a * f x + b * f y + a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ≤ f (a • x + b • y) ↔
    a * f x + b * f y + m / 2 * a * b * HPow.hPow (β := ℕ) ‖x - y‖ 2 ≤ f (a • x + b • y)
simp_rw₅ :
  a * f x + b * f y + a * (b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2)) ≤ f (a • x + b • y) ↔
    a * f x + b * f y + m / 2 * (a * (b * HPow.hPow (β := ℕ) ‖x - y‖ 2)) ≤ f (a • x + b • y)
⊢ a • f x + b • f y + a * b * (fun (r : ℝ) ↦ m / 2 * HPow.hPow (β := ℕ) r 2) ‖x - y‖ ≤ f (a • x + b • y) ↔
    HSMul.hSMul (β := ℝ) a ((fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) x) +
        HSMul.hSMul (β := ℝ) b ((fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) y) ≤
      (fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) (a • x + b • y)

Tactic:
simp_rw [← sub_le_iff_le_add, smul_eq_mul, aux_add ha hb hab, mul_assoc, mul_left_comm]

Premises used: mul_assoc, sub_le_iff_le_add, _private.0.aux_add, mul_left_comm, smul_eq_mul
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
r ε : ℝ
hε : 0 ≤ ε
rw : Icc (r - ε) (r + ε) = [r - ε -[ℝ] r + ε]
rw₁ rw₂ : Icc (r - ε) (r + ε) = Icc (r - ε) (r + ε)
⊢ closedBall r ε = [r - ε -[ℝ] r + ε]

Tactic:
rw [closedBall_eq_Icc, segment_eq_Icc ((sub_le_self _ hε).trans <| le_add_of_nonneg_right hε)]

Premises used: Real.closedBall_eq_Icc, segment_eq_Icc, le_add_of_nonneg_right, sub_le_self, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
r ε : ℝ
hε : 0 < ε
rw : Ioo (r - ε) (r + ε) = openSegment ℝ (r - ε) (r + ε)
rw₁ rw₂ : Ioo (r - ε) (r + ε) = Ioo (r - ε) (r + ε)
⊢ ball r ε = openSegment ℝ (r - ε) (r + ε)

Tactic:
rw [ball_eq_Ioo, openSegment_eq_Ioo ((sub_lt_self _ hε).trans <| lt_add_of_pos_right _ hε)]

Premises used: lt_add_of_pos_right, Real.ball_eq_Ioo, openSegment_eq_Ioo, sub_lt_self, LT.lt.trans
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
s : Set ℝ
⊢ Convex ℝ s ↔ IsPreconnected s

Tactic:
convex_iff_ordConnected.trans isPreconnected_iff_ordConnected.symm

Premises used: convex_iff_ordConnected, isPreconnected_iff_ordConnected, Iff.trans, Iff.symm
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DenselyOrdered 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
inst_6 : AddCommGroup E
inst_7 : TopologicalSpace E
inst_8 : ContinuousAdd E
inst_9 : Module 𝕜 E
inst_10 : ContinuousSMul 𝕜 E
x y : E
rw :
  Subset.{u_3} (α := Set E) ((fun (θ : 𝕜) ↦ (1 - θ) • x + θ • y) '' closure (Ioo 0 1))
    (closure ((fun (θ : 𝕜) ↦ (1 - θ) • x + θ • y) '' Ioo 0 1))
⊢ [x -[𝕜] y] ⊆ closure (openSegment 𝕜 x y)

Tactic:
rw [segment_eq_image, openSegment_eq_image, ← closure_Ioo (zero_ne_one' 𝕜)]

Premises used: segment_eq_image, openSegment_eq_image, zero_ne_one', closure_Ioo
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DenselyOrdered 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
inst_6 : AddCommGroup E
inst_7 : TopologicalSpace E
inst_8 : ContinuousAdd E
inst_9 : Module 𝕜 E
inst_10 : ContinuousSMul 𝕜 E
x y : E
⊢ Continuous.{u_2, u_3} (Y := E) fun (θ : 𝕜) ↦ (1 - θ) • x + θ • y

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Convex.Topology
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DenselyOrdered 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
inst_6 : AddCommGroup E
inst_7 : TopologicalSpace E
inst_8 : ContinuousAdd E
inst_9 : Module 𝕜 E
inst_10 : ContinuousSMul 𝕜 E
x y : E
⊢ Subset.{u_3} (α := Set E) ((fun (θ : 𝕜) ↦ (1 - θ) • x + θ • y) '' closure (Ioo 0 1))
    (closure ((fun (θ : 𝕜) ↦ (1 - θ) • x + θ • y) '' Ioo 0 1))

Tactic:
exact image_closure_subset_closure_image (by fun_prop)

Premises used: image_closure_subset_closure_image