awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2
⊢ StrictConvexSpace ℝ E

Tactic:
StrictConvexSpace.of_norm_combo_ne_one fun x y hx hy hne =>
      ⟨1 / 2, 1 / 2, one_half_pos.le, one_half_pos.le, add_halves _, ?_⟩

Premises used: add_halves, StrictConvexSpace.of_norm_combo_ne_one, HDiv.hDiv, LT.lt.le, one_half_pos, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2
fun : ∀ (x y : E) (hx : ‖x‖ = 1) (hy : ‖y‖ = 1) (hne : x ≠ y), ‖(1 / 2) • x + (1 / 2) • y‖ ≠ 1
⊢ StrictConvexSpace ℝ E

Tactic:
refine
    StrictConvexSpace.of_norm_combo_ne_one fun x y hx hy hne =>
      ⟨1 / 2, 1 / 2, one_half_pos.le, one_half_pos.le, add_halves _, ?_⟩

Premises used: add_halves, StrictConvexSpace.of_norm_combo_ne_one, HDiv.hDiv, LT.lt.le, one_half_pos, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hne : x ≠ y
rw : ¬‖x + y‖ = 2
⊢ ‖(1 / 2) • x + (1 / 2) • y‖ ≠ 1

Tactic:
rw [← smul_add, norm_smul, Real.norm_of_nonneg one_half_pos.le, one_div, ← div_eq_inv_mul, Ne,
    div_eq_one_iff_eq (two_ne_zero' ℝ)]

Premises used: Real, norm_smul, div_eq_one_iff_eq, LT.lt.le, Ne, two_ne_zero', one_half_pos, one_div, div_eq_inv_mul, smul_add, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hne : x ≠ y
⊢ ¬‖x + y‖ = 2

Tactic:
h hx hy hne
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2
x y : E
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hne : x ≠ y
⊢ ¬‖x + y‖ = 2

Tactic:
exact h hx hy hne
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : Set.Pairwise (sphere 0 1) fun (x y : E) ↦ ‖x + y‖ ≠ 2
⊢ StrictConvexSpace ℝ E

Tactic:
StrictConvexSpace.of_norm_add_ne_two fun _ _ hx hy =>
    h (mem_sphere_zero_iff_norm.2 hx) (mem_sphere_zero_iff_norm.2 hy)

Premises used: Iff.mpr, StrictConvexSpace.of_norm_add_ne_two, mem_sphere_zero_iff_norm
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y
⊢ StrictConvexSpace ℝ E

Tactic:
StrictConvexSpace.of_pairwise_sphere_norm_ne_two fun x hx y hy => mt fun h₂ => ?_

Premises used: StrictConvexSpace.of_pairwise_sphere_norm_ne_two, mt
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y
refine :
  ∀ (x : E) (hx : Membership.mem (γ := Set E) (sphere 0 1) x) (y : E) (hy : Membership.mem (γ := Set E) (sphere 0 1) y)
    (h₂ : ‖x + y‖ = 2), x = y
⊢ StrictConvexSpace ℝ E

Tactic:
refine StrictConvexSpace.of_pairwise_sphere_norm_ne_two fun x hx y hy => mt fun h₂ => ?_

Premises used: StrictConvexSpace.of_pairwise_sphere_norm_ne_two, mt
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y
x : E
hx : Membership.mem (γ := Set E) (sphere 0 1) x
y : E
hy : Membership.mem (γ := Set E) (sphere 0 1) y
h₂ : ‖x + y‖ = 2
rw : ∀ (hx : ‖x‖ = 1) (y : E) (hy : ‖y‖ = 1) (h₂ : ‖x + y‖ = 2), x = y
⊢ x = y

Tactic:
rw [mem_sphere_zero_iff_norm] at hx hy

Premises used: mem_sphere_zero_iff_norm
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
h₂ : ‖x + y‖ = 2
⊢ x = y

Tactic:
(sameRay_iff_of_norm_eq (hx.trans hy.symm)).1 (h x y hx hy h₂)

Premises used: sameRay_iff_of_norm_eq, Iff.mp, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
h₂ : ‖x + y‖ = 2
⊢ x = y

Tactic:
exact (sameRay_iff_of_norm_eq (hx.trans hy.symm)).1 (h x y hx hy h₂)

Premises used: sameRay_iff_of_norm_eq, Iff.mp, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
hx : x ∈ closedBall z r
hy : y ∈ closedBall z r
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
inl : ∀ (hx : x ∈ closedBall z 0) (hy : y ∈ closedBall z 0), a • x + b • y ∈ ball z 0
inr : ∀ (hr : r ≠ 0), a • x + b • y ∈ ball z r
⊢ a • x + b • y ∈ ball z r

Tactic:
rcases eq_or_ne r 0 with (rfl | hr)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y z : E
a b : ℝ
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : x ∈ closedBall z 0
hy : y ∈ closedBall z 0
⊢ x = z

Tactic:
rw [closedBall_zero, mem_singleton_iff] at hx hy

Premises used: Metric.closedBall_zero, Set.mem_singleton_iff
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y z : E
a b : ℝ
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : x ∈ closedBall z 0
hy : y ∈ closedBall z 0
hx₁ : x = z
⊢ y = z

Tactic:
rw [closedBall_zero, mem_singleton_iff] at hx hy

Premises used: Metric.closedBall_zero, Set.mem_singleton_iff
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y z : E
a b : ℝ
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : x = z
hy : y = z
⊢ a • x + b • y ∈ ball z 0

Tactic:
(hne (hx.trans hy.symm)).elim

Premises used: False.elim, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y z : E
a b : ℝ
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : x = z
hy : y = z
⊢ a • x + b • y ∈ ball z 0

Tactic:
exact (hne (hx.trans hy.symm)).elim

Premises used: False.elim, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
hx : x ∈ closedBall z r
hy : y ∈ closedBall z r
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hr : r ≠ 0
inr : a • x + b • y ∈ interior (closedBall z r)
⊢ a • x + b • y ∈ ball z r

Tactic:
simp only [← interior_closedBall _ hr] at hx hy ⊢

Premises used: interior_closedBall
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
hx : x ∈ closedBall z r
hy : y ∈ closedBall z r
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hr : r ≠ 0
⊢ a • x + b • y ∈ interior (closedBall z r)

Tactic:
strictConvex_closedBall ℝ z r hx hy hne ha hb hab

Premises used: Real, Set.Mem, strictConvex_closedBall
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
hx : x ∈ closedBall z r
hy : y ∈ closedBall z r
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hr : r ≠ 0
⊢ a • x + b • y ∈ interior (closedBall z r)

Tactic:
exact strictConvex_closedBall ℝ z r hx hy hne ha hb hab

Premises used: Real, strictConvex_closedBall
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y z : E
r : ℝ
hx : x ∈ closedBall z r
hy : y ∈ closedBall z r
hne : x ≠ y
⊢ openSegment ℝ x y ⊆ ball z r

Tactic:
(openSegment_subset_iff _).2 fun _ _ => combo_mem_ball_of_ne hx hy hne

Premises used: Iff.mpr, openSegment_subset_iff, combo_mem_ball_of_ne
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
a b r : ℝ
hx : ‖x‖ ≤ r
hy : ‖y‖ ≤ r
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
simp :
  ∀ (hx : Membership.mem (γ := Set E) (closedBall 0 r) x) (hy : Membership.mem (γ := Set E) (closedBall 0 r) y),
    Membership.mem (γ := Set E) (ball 0 r) (a • x + b • y)
⊢ ‖a • x + b • y‖ < r

Tactic:
simp only [← mem_ball_zero_iff, ← mem_closedBall_zero_iff] at hx hy ⊢

Premises used: mem_closedBall_zero_iff, mem_ball_zero_iff
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
a b r : ℝ
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : Membership.mem (γ := Set E) (closedBall 0 r) x
hy : Membership.mem (γ := Set E) (closedBall 0 r) y
⊢ Membership.mem (γ := Set E) (ball 0 r) (a • x + b • y)

Tactic:
combo_mem_ball_of_ne hx hy hne ha hb hab

Premises used: combo_mem_ball_of_ne, Set.Mem
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
a b r : ℝ
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : Membership.mem (γ := Set E) (closedBall 0 r) x
hy : Membership.mem (γ := Set E) (closedBall 0 r) y
⊢ Membership.mem (γ := Set E) (ball 0 r) (a • x + b • y)

Tactic:
exact combo_mem_ball_of_ne hx hy hne ha hb hab

Premises used: combo_mem_ball_of_ne
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : ¬SameRay ℝ x y
⊢ x ≠ 0 ∧ y ≠ 0 ∧ ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y

Tactic:
simp only [sameRay_iff_inv_norm_smul_eq, not_or, ← Ne.eq_def] at h

Premises used: Ne.eq_def, not_or, sameRay_iff_inv_norm_smul_eq
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : x ≠ 0 ∧ y ≠ 0 ∧ ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
⊢ x ≠ 0

Tactic:
rcases h with ⟨hx, hy, hne⟩
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : x ≠ 0 ∧ y ≠ 0 ∧ ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hx : x ≠ 0
⊢ y ≠ 0

Tactic:
rcases h with ⟨hx, hy, hne⟩
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : x ≠ 0 ∧ y ≠ 0 ∧ ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y

Tactic:
rcases h with ⟨hx, hy, hne⟩
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
hx : x ≠ 0
hy : y ≠ 0
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
⊢ 0 < ‖x‖

Tactic:
rw [← norm_pos_iff] at hx hy

Premises used: norm_pos_iff
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
hx : x ≠ 0
hy : y ≠ 0
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hx₁ : 0 < ‖x‖
⊢ 0 < ‖y‖

Tactic:
rw [← norm_pos_iff] at hx hy

Premises used: norm_pos_iff
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
hx : x ≠ 0
hy : y ≠ 0
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hx₁ : 0 < ‖x‖
hy₁ : 0 < ‖y‖
⊢ ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y

Tactic:
rw [← norm_pos_iff] at hx hy

Premises used: norm_pos_iff
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
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
⊢ 0 < ‖x‖ + ‖y‖

Tactic:
have hxy : 0 < ‖x‖ + ‖y‖ := add_pos hx hy
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
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‖
rw : (‖x‖ + ‖y‖) / (‖x‖ + ‖y‖) = 1
rw₁ rw₂ : Eq (α := ℝ) 1 1
⊢ ‖x‖ / (‖x‖ + ‖y‖) + ‖y‖ / (‖x‖ + ‖y‖) = 1

Tactic:
rw [← add_div, div_self hxy.ne']

Premises used: LT.lt.ne', div_self, add_div
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
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‖
⊢ Membership.mem (γ := Set E) (ball 0 1) ((‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y)

Tactic:
have :=
    combo_mem_ball_of_ne (inv_norm_smul_mem_unitClosedBall x)
      (inv_norm_smul_mem_unitClosedBall y) hne (div_pos hx hxy) (div_pos hy hxy)
      (by rw [← add_div, div_self hxy.ne'])
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
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‖
rwa₁₁ rwa₁₂ rwa₁₃ rwa₁₄ : ∀ (this : ‖x + y‖ < ‖x‖ + ‖y‖), ‖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

Premises used: Iff.mpr, norm_smul, smul_inv_smul₀, inv_pos, LT.lt.le, LT.lt.ne', div_lt_one, div_eq_inv_mul, SemigroupAction.mul_smul, smul_add, mem_ball_zero_iff, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : ¬SameRay ℝ x y
nth_rw : ∀ (h : ¬SameRay ℝ (x - y + y) y), ‖x - y + y‖ - ‖y‖ < ‖x - y‖
⊢ ‖x‖ - ‖y‖ < ‖x - y‖

Tactic:
nth_rw 1 [← sub_add_cancel x y] at h ⊢

Premises used: sub_add_cancel
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : ¬SameRay ℝ (x - y + y) y
⊢ ‖x - y + y‖ - ‖y‖ < ‖x - y‖

Tactic:
sub_lt_iff_lt_add.2 (norm_add_lt_of_not_sameRay fun H' => h <| H'.add_left SameRay.rfl)

Premises used: Iff.mpr, SameRay.add_left, sub_lt_iff_lt_add, SameRay.rfl, norm_add_lt_of_not_sameRay
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : ¬SameRay ℝ (x - y + y) y
⊢ ‖x - y + y‖ - ‖y‖ < ‖x - y‖

Tactic:
exact sub_lt_iff_lt_add.2 (norm_add_lt_of_not_sameRay fun H' => h <| H'.add_left SameRay.rfl)

Premises used: Iff.mpr, SameRay.add_left, sub_lt_iff_lt_add, SameRay.rfl, norm_add_lt_of_not_sameRay
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
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‖

Tactic:
abs_sub_lt_iff.2 ⟨lt_norm_sub_of_not_sameRay h, ?_⟩

Premises used: lt_norm_sub_of_not_sameRay, Iff.mpr, abs_sub_lt_iff, And.intro
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : ¬SameRay ℝ x y
refine : ‖y‖ - ‖x‖ < ‖x - y‖
⊢ |‖x‖ - ‖y‖| < ‖x - y‖

Tactic:
refine abs_sub_lt_iff.2 ⟨lt_norm_sub_of_not_sameRay h, ?_⟩

Premises used: lt_norm_sub_of_not_sameRay, Iff.mpr, abs_sub_lt_iff, And.intro
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h : ¬SameRay ℝ x y
rw : ‖y‖ - ‖x‖ < ‖y - x‖
⊢ ‖y‖ - ‖x‖ < ‖x - y‖

Tactic:
rw [norm_sub_rev]

Premises used: norm_sub_rev
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
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‖ < ‖y - x‖

Tactic:
lt_norm_sub_of_not_sameRay (mt SameRay.symm h)

Premises used: lt_norm_sub_of_not_sameRay, mt, SameRay.symm
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
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‖ < ‖y - x‖

Tactic:
exact lt_norm_sub_of_not_sameRay (mt SameRay.symm h)

Premises used: lt_norm_sub_of_not_sameRay, mt, SameRay.symm
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
⊢ SameRay ℝ x y ↔ ‖x + y‖ = ‖x‖ + ‖y‖

Tactic:
⟨SameRay.norm_add, fun h => Classical.not_not.1 fun h' => (norm_add_lt_of_not_sameRay h').ne h⟩

Premises used: Classical.not_not, Iff.intro, Iff.mp, SameRay.norm_add, norm_add_lt_of_not_sameRay, LT.lt.ne
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
h₁ : ‖x‖ = ‖y‖
h₂ : ‖x + y‖ = ‖x‖ + ‖y‖
⊢ x = y

Tactic:
(sameRay_iff_norm_add.mpr h₂).eq_of_norm_eq h₁

Premises used: Iff.mpr, SameRay.eq_of_norm_eq, sameRay_iff_norm_add
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
⊢ ¬SameRay ℝ x y ↔ ‖x + y‖ < ‖x‖ + ‖y‖

Tactic:
sameRay_iff_norm_add.not.trans (norm_add_le _ _).lt_iff_ne.symm

Premises used: norm_add_le, Iff.not, sameRay_iff_norm_add, LE.le.lt_iff_ne, Iff.trans, Iff.symm
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
⊢ SameRay ℝ x y ↔ ‖x - y‖ = |‖x‖ - ‖y‖|

Tactic:
⟨SameRay.norm_sub, fun h =>
    Classical.not_not.1 fun h' => (abs_lt_norm_sub_of_not_sameRay h').ne' h⟩

Premises used: Classical.not_not, abs_lt_norm_sub_of_not_sameRay, SameRay.norm_sub, LT.lt.ne', Iff.intro, Iff.mp
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
x y : E
⊢ ¬SameRay ℝ x y ↔ |‖x‖ - ‖y‖| < ‖x - y‖

Tactic:
sameRay_iff_norm_sub.not.trans <| ne_comm.trans (abs_norm_sub_norm_le _ _).lt_iff_ne.symm

Premises used: Iff.not, abs_norm_sub_norm_le, sameRay_iff_norm_sub, LE.le.lt_iff_ne, Iff.trans, ne_comm, Iff.symm
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
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‖
rw₈ rw₉ : ‖x + y‖ < ‖y‖ + ‖y‖ ↔ ‖x + y‖ < ‖y‖ + ‖y‖
⊢ ‖(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]

Premises used: Iff.mpr, Real, norm_smul, one_div_nonneg, inv_eq_one_div, not_sameRay_iff_of_norm_eq, div_lt_iff₀, not_sameRay_iff_norm_add_lt, zero_lt_two', zero_le_two, div_eq_inv_mul, mul_two, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Convex.Strong
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
f : E → ℝ
⊢ UniformConvexOn s 0 f ↔ ConvexOn ℝ s f

Tactic:
simp [UniformConvexOn, ConvexOn]

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

Tactic:
simp [UniformConcaveOn, ConcaveOn]

Premises used: ConcaveOn, UniformConcaveOn
-- Module: Mathlib.Analysis.Convex.Strong
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
h : ψ ‖x - y‖ ≤ φ ‖x - y‖
⊢ a • f x + b • f y - a * b * φ ‖x - y‖ ≤ a • f x + b • f y - a * b * ψ ‖x - y‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Strong
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
⊢ ψ ‖x - y‖ ≤ φ ‖x - y‖

Tactic:
apply hψφ
-- Module: Mathlib.Analysis.Convex.Strong
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
bc : ψ ‖x - y‖ ≤ φ ‖x - y‖
⊢ a • f x + b • f y + a * b * ψ ‖x - y‖ ≤ a • f x + b • f y + a * b * φ ‖x - y‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Strong
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
⊢ ψ ‖x - y‖ ≤ φ ‖x - y‖

Tactic:
apply hψφ
-- 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φ : 0 ≤ φ
⊢ ConvexOn ℝ s f

Tactic:
simpa using hf.mono hφ

Premises used: UniformConvexOn.mono
-- 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φ : 0 ≤ φ
⊢ ConcaveOn ℝ s f

Tactic:
simpa using hf.mono hφ

Premises used: UniformConcaveOn.mono
-- 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
⊢ StrictConvexOn ℝ 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 <|
    sub_lt_self _ ?_⟩

Premises used: sub_lt_self, StrictConvexOn, LT.lt.le, And.right, And.left, HAdd.hAdd, And.intro, HSMul.hSMul, LE.le.trans_lt