awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
this : Membership.mem (γ := Set E) (ball 0 1) ((‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y)
rwa : ∀ (this : ‖(‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₁ : ∀ (this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₂ : ∀ (this : ‖((‖x‖ + ‖y‖)⁻¹ * ‖x‖) • ‖x‖⁻¹ • x + ((‖x‖ + ‖y‖)⁻¹ * ‖y‖) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₃ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • ‖x‖ • ‖x‖⁻¹ • x + ((‖x‖ + ‖y‖)⁻¹ * ‖y‖) • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₄ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • ‖x‖ • ‖x‖⁻¹ • x + (‖x‖ + ‖y‖)⁻¹ • ‖y‖ • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₅ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • x + (‖x‖ + ‖y‖)⁻¹ • ‖y‖ • ‖y‖⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₆ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • x + (‖x‖ + ‖y‖)⁻¹ • y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₇ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹ • (x + y)‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₈ : ∀ (this : ‖(‖x‖ + ‖y‖)⁻¹‖ * ‖x + y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₉ : ∀ (this : (‖x‖ + ‖y‖)⁻¹ * ‖x + y‖ < 1), ‖x + y‖ < ‖x‖ + ‖y‖
rwa₁₀ : ∀ (this : ‖x + y‖ / (‖x‖ + ‖y‖) < 1), ‖x + y‖ < ‖x‖ + ‖y‖
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
have rwa₁₁ : ∀ (this : ‖x + y‖ < ‖x‖ + ‖y‖), ‖x + y‖ < ‖x‖ + ‖y‖
Tactic: rwa [mem_ball_zero_iff, div_eq_inv_mul, div_eq_inv_mul, mul_smul, mul_smul, smul_inv_smul₀ hx.ne',
    smul_inv_smul₀ hy.ne', ← smul_add, norm_smul, Real.norm_of_nonneg (inv_pos.2 hxy).le, ←
    div_eq_inv_mul, div_lt_one hxy] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : ¬SameRay ℝ x y
⊢ ‖x‖ - ‖y‖ < ‖x - y‖
have nth_rw : ∀ (h : ¬SameRay ℝ (x - y + y) y), ‖x - y + y‖ - ‖y‖ < ‖x - y‖
Tactic: nth_rw 1 [← sub_add_cancel x y] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : ¬SameRay ℝ x y
⊢ |‖x‖ - ‖y‖| < ‖x - y‖
have refine : ‖y‖ - ‖x‖ < ‖x - y‖
Tactic: refine abs_sub_lt_iff.2 ⟨lt_norm_sub_of_not_sameRay h, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : ¬SameRay ℝ x y
⊢ ‖y‖ - ‖x‖ < ‖x - y‖
have rw : ‖y‖ - ‖x‖ < ‖y - x‖
Tactic: rw [norm_sub_rev]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : ‖x‖ = ‖y‖
⊢ ‖(1 / 2) • (x + y)‖ < ‖x‖ ↔ x ≠ y
have rw : ‖1 / 2‖ * ‖x + y‖ < ‖x‖ ↔ x ≠ y
Tactic: rw [norm_smul, Real.norm_of_nonneg (one_div_nonneg.2 zero_le_two), ← inv_eq_one_div, ←
    div_eq_inv_mul, div_lt_iff₀ (zero_lt_two' ℝ), mul_two, ← not_sameRay_iff_of_norm_eq h,
    not_sameRay_iff_norm_add_lt, h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : ‖x‖ = ‖y‖
rw : ‖1 / 2‖ * ‖x + y‖ < ‖x‖ ↔ x ≠ y
⊢ ‖(1 / 2) • (x + y)‖ < ‖x‖ ↔ x ≠ y
have rw₁ : 1 / 2 * ‖x + y‖ < ‖x‖ ↔ x ≠ y
Tactic: rw [norm_smul, Real.norm_of_nonneg (one_div_nonneg.2 zero_le_two), ← inv_eq_one_div, ←
    div_eq_inv_mul, div_lt_iff₀ (zero_lt_two' ℝ), mul_two, ← not_sameRay_iff_of_norm_eq h,
    not_sameRay_iff_norm_add_lt, h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : ‖x‖ = ‖y‖
rw : ‖1 / 2‖ * ‖x + y‖ < ‖x‖ ↔ x ≠ y
rw₁ : 1 / 2 * ‖x + y‖ < ‖x‖ ↔ x ≠ y
⊢ ‖(1 / 2) • (x + y)‖ < ‖x‖ ↔ x ≠ y
have rw₂ : 2⁻¹ * ‖x + y‖ < ‖x‖ ↔ x ≠ y
Tactic: rw [norm_smul, Real.norm_of_nonneg (one_div_nonneg.2 zero_le_two), ← inv_eq_one_div, ←
    div_eq_inv_mul, div_lt_iff₀ (zero_lt_two' ℝ), mul_two, ← not_sameRay_iff_of_norm_eq h,
    not_sameRay_iff_norm_add_lt, h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : ‖x‖ = ‖y‖
rw : ‖1 / 2‖ * ‖x + y‖ < ‖x‖ ↔ x ≠ y
rw₁ : 1 / 2 * ‖x + y‖ < ‖x‖ ↔ x ≠ y
rw₂ : 2⁻¹ * ‖x + y‖ < ‖x‖ ↔ x ≠ y
⊢ ‖(1 / 2) • (x + y)‖ < ‖x‖ ↔ x ≠ y
have rw₃ : ‖x + y‖ / 2 < ‖x‖ ↔ x ≠ y
Tactic: rw [norm_smul, Real.norm_of_nonneg (one_div_nonneg.2 zero_le_two), ← inv_eq_one_div, ←
    div_eq_inv_mul, div_lt_iff₀ (zero_lt_two' ℝ), mul_two, ← not_sameRay_iff_of_norm_eq h,
    not_sameRay_iff_norm_add_lt, h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : ‖x‖ = ‖y‖
rw : ‖1 / 2‖ * ‖x + y‖ < ‖x‖ ↔ x ≠ y
rw₁ : 1 / 2 * ‖x + y‖ < ‖x‖ ↔ x ≠ y
rw₂ : 2⁻¹ * ‖x + y‖ < ‖x‖ ↔ x ≠ y
rw₃ : ‖x + y‖ / 2 < ‖x‖ ↔ x ≠ y
⊢ ‖(1 / 2) • (x + y)‖ < ‖x‖ ↔ x ≠ y
have rw₄ : ‖x + y‖ < ‖x‖ * 2 ↔ x ≠ y
Tactic: rw [norm_smul, Real.norm_of_nonneg (one_div_nonneg.2 zero_le_two), ← inv_eq_one_div, ←
    div_eq_inv_mul, div_lt_iff₀ (zero_lt_two' ℝ), mul_two, ← not_sameRay_iff_of_norm_eq h,
    not_sameRay_iff_norm_add_lt, h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : ‖x‖ = ‖y‖
rw : ‖1 / 2‖ * ‖x + y‖ < ‖x‖ ↔ x ≠ y
rw₁ : 1 / 2 * ‖x + y‖ < ‖x‖ ↔ x ≠ y
rw₂ : 2⁻¹ * ‖x + y‖ < ‖x‖ ↔ x ≠ y
rw₃ : ‖x + y‖ / 2 < ‖x‖ ↔ x ≠ y
rw₄ : ‖x + y‖ < ‖x‖ * 2 ↔ x ≠ y
⊢ ‖(1 / 2) • (x + y)‖ < ‖x‖ ↔ x ≠ y
have rw₅ : ‖x + y‖ < ‖x‖ + ‖x‖ ↔ x ≠ y
Tactic: rw [norm_smul, Real.norm_of_nonneg (one_div_nonneg.2 zero_le_two), ← inv_eq_one_div, ←
    div_eq_inv_mul, div_lt_iff₀ (zero_lt_two' ℝ), mul_two, ← not_sameRay_iff_of_norm_eq h,
    not_sameRay_iff_norm_add_lt, h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : ‖x‖ = ‖y‖
rw : ‖1 / 2‖ * ‖x + y‖ < ‖x‖ ↔ x ≠ y
rw₁ : 1 / 2 * ‖x + y‖ < ‖x‖ ↔ x ≠ y
rw₂ : 2⁻¹ * ‖x + y‖ < ‖x‖ ↔ x ≠ y
rw₃ : ‖x + y‖ / 2 < ‖x‖ ↔ x ≠ y
rw₄ : ‖x + y‖ < ‖x‖ * 2 ↔ x ≠ y
rw₅ : ‖x + y‖ < ‖x‖ + ‖x‖ ↔ x ≠ y
⊢ ‖(1 / 2) • (x + y)‖ < ‖x‖ ↔ x ≠ y
have rw₆ : ‖x + y‖ < ‖x‖ + ‖x‖ ↔ ¬SameRay ℝ x y
Tactic: rw [norm_smul, Real.norm_of_nonneg (one_div_nonneg.2 zero_le_two), ← inv_eq_one_div, ←
    div_eq_inv_mul, div_lt_iff₀ (zero_lt_two' ℝ), mul_two, ← not_sameRay_iff_of_norm_eq h,
    not_sameRay_iff_norm_add_lt, h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : ‖x‖ = ‖y‖
rw : ‖1 / 2‖ * ‖x + y‖ < ‖x‖ ↔ x ≠ y
rw₁ : 1 / 2 * ‖x + y‖ < ‖x‖ ↔ x ≠ y
rw₂ : 2⁻¹ * ‖x + y‖ < ‖x‖ ↔ x ≠ y
rw₃ : ‖x + y‖ / 2 < ‖x‖ ↔ x ≠ y
rw₄ : ‖x + y‖ < ‖x‖ * 2 ↔ x ≠ y
rw₅ : ‖x + y‖ < ‖x‖ + ‖x‖ ↔ x ≠ y
rw₆ : ‖x + y‖ < ‖x‖ + ‖x‖ ↔ ¬SameRay ℝ x y
⊢ ‖(1 / 2) • (x + y)‖ < ‖x‖ ↔ x ≠ y
have rw₇ : ‖x + y‖ < ‖x‖ + ‖x‖ ↔ ‖x + y‖ < ‖x‖ + ‖y‖
Tactic: rw [norm_smul, Real.norm_of_nonneg (one_div_nonneg.2 zero_le_two), ← inv_eq_one_div, ←
    div_eq_inv_mul, div_lt_iff₀ (zero_lt_two' ℝ), mul_two, ← not_sameRay_iff_of_norm_eq h,
    not_sameRay_iff_norm_add_lt, h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.StrictConvexSpace (goal)
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : ‖x‖ = ‖y‖
rw : ‖1 / 2‖ * ‖x + y‖ < ‖x‖ ↔ x ≠ y
rw₁ : 1 / 2 * ‖x + y‖ < ‖x‖ ↔ x ≠ y
rw₂ : 2⁻¹ * ‖x + y‖ < ‖x‖ ↔ x ≠ y
rw₃ : ‖x + y‖ / 2 < ‖x‖ ↔ x ≠ y
rw₄ : ‖x + y‖ < ‖x‖ * 2 ↔ x ≠ y
rw₅ : ‖x + y‖ < ‖x‖ + ‖x‖ ↔ x ≠ y
rw₆ : ‖x + y‖ < ‖x‖ + ‖x‖ ↔ ¬SameRay ℝ x y
rw₇ : ‖x + y‖ < ‖x‖ + ‖x‖ ↔ ‖x + y‖ < ‖x‖ + ‖y‖
⊢ ‖(1 / 2) • (x + y)‖ < ‖x‖ ↔ x ≠ y
have rw₈ : ‖x + y‖ < ‖y‖ + ‖y‖ ↔ ‖x + y‖ < ‖y‖ + ‖y‖
Tactic: rw [norm_smul, Real.norm_of_nonneg (one_div_nonneg.2 zero_le_two), ← inv_eq_one_div, ←
    div_eq_inv_mul, div_lt_iff₀ (zero_lt_two' ℝ), mul_two, ← not_sameRay_iff_of_norm_eq h,
    not_sameRay_iff_norm_add_lt, h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f : E → ℝ
hψφ : ψ ≤ φ
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
⊢ a • f x + b • f y - a * b * φ ‖x - y‖ ≤ a • f x + b • f y - a * b * ψ ‖x - y‖
have h : ψ ‖x - y‖ ≤ φ ‖x - y‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f : E → ℝ
hψφ : ψ ≤ φ
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‖ ≤ a • f x + b • f y + a * b * φ ‖x - y‖
have bc : ψ ‖x - y‖ ≤ φ ‖x - y‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
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
⊢ StrictConvexOn ℝ s f
have 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‖
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 _ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
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
⊢ 0 < a * b * φ ‖x - y‖
have rw : ∀ (hxy : 0 < ‖x - y‖) (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1), 0 < a * b * φ ‖x - y‖
Tactic: rw [← sub_ne_zero, ← norm_pos_iff] at hxy
Cleared hypotheses: hxy, a, b, ha, hb, hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
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
⊢ 0 < a * b * φ ‖x - y‖
have positivity : 0 < φ ‖x - y‖ → 0 < a * b * φ ‖x - y‖
Tactic: positivity [hφ _ hxy.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
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
have 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‖
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 _ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
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
⊢ 0 < a * b * φ ‖x - y‖
have rw : ∀ (hxy : 0 < ‖x - y‖) (a b : ℝ) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1), 0 < a * b * φ ‖x - y‖
Tactic: rw [← sub_ne_zero, ← norm_pos_iff] at hxy
Cleared hypotheses: hxy, a, b, ha, hb, hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
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
⊢ 0 < a * b * φ ‖x - y‖
have positivity : 0 < φ ‖x - y‖ → 0 < a * b * φ ‖x - y‖
Tactic: positivity [hφ _ hxy.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
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)
have 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‖
Tactic: refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
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)
have 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)
Tactic: refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConvexOn s φ f
⊢ UniformConcaveOn s φ (-f)
have 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‖)
Tactic: refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ le_of_neg_le_neg ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
φ : ℝ → ℝ
s : Set E
f : E → ℝ
hf : UniformConcaveOn s φ f
⊢ UniformConvexOn s φ (-f)
have 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)
Tactic: refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ le_of_neg_le_neg ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
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 : ℝ
⊢ m / 2 * HPow.hPow (β := ℕ) r 2 ≤ n / 2 * HPow.hPow (β := ℕ) r 2
have ha : 0 ≤ HPow.hPow (β := ℕ) r 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
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
⊢ m / 2 * HPow.hPow (β := ℕ) r 2 ≤ n / 2 * HPow.hPow (β := ℕ) r 2
have hbc : LE.le (α := (fun (a : ℝ) ↦ ℝ) r) 0 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
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 : ℝ
⊢ m / 2 * HPow.hPow (β := ℕ) r 2 ≤ n / 2 * HPow.hPow (β := ℕ) r 2
have ha : 0 ≤ HPow.hPow (β := ℕ) r 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
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
⊢ m / 2 * HPow.hPow (β := ℕ) r 2 ≤ n / 2 * HPow.hPow (β := ℕ) r 2
have hbc : LE.le (α := (fun (a : ℝ) ↦ ℝ) r) 0 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
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
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
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 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)
have 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)
Tactic: obtain rfl := eq_sub_of_add_eq hab
Cleared hypotheses: a, ha, hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
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
have 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)
Tactic: refine and_congr_right fun _ ↦ forall₄_congr fun x _ y _ ↦ forall₅_congr fun a b ha hb hab ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
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)
⊢ 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)
have 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
Tactic: simp_rw [sub_le_iff_le_add, smul_eq_mul, aux_sub ha hb hab, mul_assoc, mul_left_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
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
⊢ 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)
have 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
Tactic: simp_rw [sub_le_iff_le_add, smul_eq_mul, aux_sub ha hb hab, mul_assoc, mul_left_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
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
⊢ 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)
have 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
Tactic: simp_rw [sub_le_iff_le_add, smul_eq_mul, aux_sub ha hb hab, mul_assoc, mul_left_comm]