awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
⊢ y -ᵥ x ∈ [0 -[ℝ] z -ᵥ x]

Tactic:
have : y -ᵥ x ∈ [(0 : E) -[ℝ] z -ᵥ x] := by
    rw [mem_segment_iff_wbtw, ← dist_add_dist_eq_iff, dist_zero, dist_vsub_cancel_right,
      ← dist_eq_norm_vsub', ← dist_eq_norm_vsub', hxy, hyz, ← add_mul, add_sub_cancel,
      one_mul]
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
this : y -ᵥ x ∈ [0 -[ℝ] z -ᵥ x]
inl :
  ∀ (hxy : dist x y = r * dist x x) (hyz : dist y x = (1 - r) * dist x x) (this : y -ᵥ x ∈ [0 -[ℝ] x -ᵥ x]),
    y = (AffineMap.lineMap x x : (a : ℝ) → PE) r
inr : ∀ (hne : x ≠ z), y = (AffineMap.lineMap x z : (a : ℝ) → PE) r
⊢ y = (AffineMap.lineMap x z : (a : ℝ) → PE) r

Tactic:
obtain rfl | hne := eq_or_ne x z

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
x y : PE
hxy : dist x y = r * dist x x
hyz : dist y x = (1 - r) * dist x x
this : y -ᵥ x ∈ [0 -[ℝ] x -ᵥ x]
⊢ y = x

Tactic:
simpa
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
x y : PE
hxy : dist x y = r * dist x x
hyz : dist y x = (1 - r) * dist x x
this : y -ᵥ x ∈ [0 -[ℝ] x -ᵥ x]
inl :
  ∀ (hxy : dist y y = r * dist y y) (hyz : dist y y = (1 - r) * dist y y) (this : y -ᵥ y ∈ [0 -[ℝ] y -ᵥ y]),
    y = (AffineMap.lineMap y y : (a : ℝ) → PE) r
⊢ y = (AffineMap.lineMap x x : (a : ℝ) → PE) r

Tactic:
obtain rfl : y = x := by simpa

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
y : PE
hxy : dist y y = r * dist y y
hyz : dist y y = (1 - r) * dist y y
this : y -ᵥ y ∈ [0 -[ℝ] y -ᵥ y]
⊢ y = (AffineMap.lineMap y y : (a : ℝ) → PE) r

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
this : y -ᵥ x ∈ [0 -[ℝ] z -ᵥ x]
hne : x ≠ z
⊢ dist x z ≠ 0

Tactic:
rw [← dist_ne_zero] at hne

Premises used: dist_ne_zero
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
this : y -ᵥ x ∈ [0 -[ℝ] z -ᵥ x]
hne : dist x z ≠ 0
inr :
  ∀ (a b : ℝ),
    0 ≤ a →
      ∀ (hb : 0 ≤ b),
        a + b = 1 →
          ∀ (H : HSMul.hSMul (β := E) a 0 + b • (z -ᵥ x) = y -ᵥ x), y = (AffineMap.lineMap x z : (a : ℝ) → PE) r
⊢ y = (AffineMap.lineMap x z : (a : ℝ) → PE) r

Tactic:
obtain ⟨a, b, _, hb, _, H⟩ := this
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
hne : dist x z ≠ 0
a b : ℝ
left : 0 ≤ a
hb : 0 ≤ b
left_1 : a + b = 1
H : HSMul.hSMul (β := E) a 0 + b • (z -ᵥ x) = y -ᵥ x
⊢ b • (z -ᵥ x) = y -ᵥ x

Tactic:
rw [smul_zero, zero_add] at H

Premises used: smul_zero, zero_add
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
hne : dist x z ≠ 0
a b : ℝ
left : 0 ≤ a
hb : 0 ≤ b
left_1 : a + b = 1
H : b • (z -ᵥ x) = y -ᵥ x
⊢ ‖b • (z -ᵥ x)‖ = ‖y -ᵥ x‖

Tactic:
have H' := congr_arg norm H
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
hne : dist x z ≠ 0
a b : ℝ
left : 0 ≤ a
hb : 0 ≤ b
left_1 : a + b = 1
H : b • (z -ᵥ x) = y -ᵥ x
H' : ‖b • (z -ᵥ x)‖ = ‖y -ᵥ x‖
⊢ b = r

Tactic:
rw [norm_smul, Real.norm_of_nonneg hb, ← dist_eq_norm_vsub', ← dist_eq_norm_vsub', hxy,
      mul_left_inj' hne] at H'

Premises used: norm_smul, dist_eq_norm_vsub', mul_left_inj', Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
r : ℝ
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
hne : dist x z ≠ 0
a b : ℝ
left : 0 ≤ a
hb : 0 ≤ b
left_1 : a + b = 1
H : b • (z -ᵥ x) = y -ᵥ x
H' : b = r
inr : y = r • (z -ᵥ x) +ᵥ x
inr₁ : y = b • (z -ᵥ x) +ᵥ x
inr₂ : y = (y -ᵥ x) +ᵥ x
inr₃ inr₄ : y = y
⊢ y = (AffineMap.lineMap x z : (a : ℝ) → PE) r

Tactic:
rw [AffineMap.lineMap_apply, ← H', H, vsub_vadd]

Premises used: AffineMap.lineMap_apply, vsub_vadd
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
hxy : dist x y = @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * dist x z
hyz : dist y z = HSub.hSub (α := ℝ) 1 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) * dist x z
⊢ y = midpoint ℝ x z

Tactic:
apply eq_lineMap_of_dist_eq_mul_of_dist_eq_mul

Premises used: eq_lineMap_of_dist_eq_mul_of_dist_eq_mul
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
hxy : dist x y = 2⁻¹ * dist x z
hxy₁ hxy₂ hxy₃ hxy₄ : dist x y = dist x z / 2
⊢ dist x y = @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * dist x z

Tactic:
rwa [invOf_eq_inv, ← div_eq_inv_mul]

Premises used: invOf_eq_inv, div_eq_inv_mul
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
E : Type u_3
PE : Type u_5
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : StrictConvexSpace ℝ E
inst_3 : MetricSpace PE
inst_4 : NormedAddTorsor E PE
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
hyz : dist y z = HSub.hSub (α := ℝ) 1 2⁻¹ * dist x z
hyz₁ : dist y z = (1 - 1 / 2) * dist x z
hyz₂ : dist y z = 1 / 2 * dist x z
hyz₃ : dist y z = 2⁻¹ * dist x z
hyz₄ hyz₅ hyz₆ hyz₇ : dist y z = dist x z / 2
⊢ dist y z = HSub.hSub (α := ℝ) 1 (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) * dist x z

Tactic:
rwa [invOf_eq_inv, ← one_div, sub_half, one_div, ← div_eq_inv_mul]

Premises used: one_div, invOf_eq_inv, sub_half, div_eq_inv_mul
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
E : Type u_3
F : Type u_4
PE : Type u_5
PF : Type u_6
inst_3 : NormedAddCommGroup E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
inst_7 : StrictConvexSpace ℝ E
inst_8 : MetricSpace PE
inst_9 : MetricSpace PF
inst_10 : NormedAddTorsor E PE
inst_11 : NormedAddTorsor F PF
r : ℝ
f : PF → PE
x_1 y_1 z : PE
hi : Isometry f
x y : PF
hx : dist (f x) (f (midpoint ℝ x y)) = dist (f x) (f y) / 2
hy : dist (f (midpoint ℝ x y)) (f y) = dist (f x) (f y) / 2
⊢ f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)

Tactic:
apply eq_midpoint_of_dist_eq_half

Premises used: eq_midpoint_of_dist_eq_half
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
E : Type u_3
F : Type u_4
PE : Type u_5
PF : Type u_6
inst_3 : NormedAddCommGroup E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
inst_7 : StrictConvexSpace ℝ E
inst_8 : MetricSpace PE
inst_9 : MetricSpace PF
inst_10 : NormedAddTorsor E PE
inst_11 : NormedAddTorsor F PF
r : ℝ
f : PF → PE
x_1 y_1 z : PE
hi : Isometry f
x y : PF
hx : dist x (midpoint ℝ x y) = dist x y / 2
⊢ dist (f x) (f (midpoint ℝ x y)) = dist (f x) (f y) / 2

Tactic:
rw [hi.dist_eq, hi.dist_eq]

Premises used: Isometry.dist_eq
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
E : Type u_3
F : Type u_4
PE : Type u_5
PF : Type u_6
inst_3 : NormedAddCommGroup E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
inst_7 : StrictConvexSpace ℝ E
inst_8 : MetricSpace PE
inst_9 : MetricSpace PF
inst_10 : NormedAddTorsor E PE
inst_11 : NormedAddTorsor F PF
r : ℝ
f : PF → PE
x_1 y_1 z : PE
hi : Isometry f
x y : PF
⊢ dist x (midpoint ℝ x y) = dist x y / 2

Tactic:
simp only [dist_left_midpoint, Real.norm_of_nonneg zero_le_two, div_eq_inv_mul]

Premises used: dist_left_midpoint, zero_le_two, div_eq_inv_mul, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
E : Type u_3
F : Type u_4
PE : Type u_5
PF : Type u_6
inst_3 : NormedAddCommGroup E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
inst_7 : StrictConvexSpace ℝ E
inst_8 : MetricSpace PE
inst_9 : MetricSpace PF
inst_10 : NormedAddTorsor E PE
inst_11 : NormedAddTorsor F PF
r : ℝ
f : PF → PE
x_1 y_1 z : PE
hi : Isometry f
x y : PF
hy : dist (midpoint ℝ x y) y = dist x y / 2
⊢ dist (f (midpoint ℝ x y)) (f y) = dist (f x) (f y) / 2

Tactic:
rw [hi.dist_eq, hi.dist_eq]

Premises used: Isometry.dist_eq
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
E : Type u_3
F : Type u_4
PE : Type u_5
PF : Type u_6
inst_3 : NormedAddCommGroup E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
inst_7 : StrictConvexSpace ℝ E
inst_8 : MetricSpace PE
inst_9 : MetricSpace PF
inst_10 : NormedAddTorsor E PE
inst_11 : NormedAddTorsor F PF
r : ℝ
f : PF → PE
x_1 y_1 z : PE
hi : Isometry f
x y : PF
⊢ dist (midpoint ℝ x y) y = dist x y / 2

Tactic:
simp only [dist_midpoint_right, Real.norm_of_nonneg zero_le_two, div_eq_inv_mul]

Premises used: dist_midpoint_right, zero_le_two, div_eq_inv_mul, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
inst_2 : StrictConvexSpace ℝ V
E : Type u_3
F : Type u_4
PE : Type u_5
PF : Type u_6
inst_3 : NormedAddCommGroup E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
inst_7 : StrictConvexSpace ℝ E
inst_8 : MetricSpace PE
inst_9 : MetricSpace PF
inst_10 : NormedAddTorsor E PE
inst_11 : NormedAddTorsor F PF
r : ℝ
f : PF → PE
x_1 y z : PE
hi : Isometry f
x : F
⊢ norm.{u_3} (E := E) ((AffineMap.linear (AffineMap.ofMapMidpoint f ⋯ ⋯) : (a : F) → E) x : E) = ‖x‖

Tactic:
simp [AffineMap.ofMapMidpoint, ← dist_eq_norm_vsub E, hi.dist_eq]

Premises used: AffineMap.ofMapMidpoint, Isometry.dist_eq, dist_eq_norm_vsub
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
E : Type u_3
F : Type u_4
PE : Type u_5
PF : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℝ F
inst_4 : StrictConvexSpace ℝ E
inst_5 : MetricSpace PE
inst_6 : MetricSpace PF
inst_7 : NormedAddTorsor E PE
inst_8 : NormedAddTorsor F PF
f : PF → PE
hi : Isometry f
⊢ (⇑hi.affineIsometryOfStrictConvexSpace : (a : PF) → PE) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.StrictConvexBetween
Goal:
E : Type u_3
F : Type u_4
PE : Type u_5
PF : Type u_6
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace ℝ E
inst_3 : NormedSpace ℝ F
inst_4 : StrictConvexSpace ℝ E
inst_5 : MetricSpace PE
inst_6 : MetricSpace PF
inst_7 : NormedAddTorsor E PE
inst_8 : NormedAddTorsor F PF
f : PF → PE
hi : Isometry f
p : PF
⊢ (hi.affineIsometryOfStrictConvexSpace : (a : PF) → PE) p = f p

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : StrictConvexSpace 𝕜 E
x : E
r : ℝ
inl : ∀ (hr : r ≤ 0), StrictConvex 𝕜 (closedBall x r)
inr : ∀ (hr : 0 < r), StrictConvex 𝕜 (closedBall x r)
⊢ StrictConvex 𝕜 (closedBall x r)

Tactic:
rcases le_or_gt r 0 with hr | hr

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
⊢ StrictConvex 𝕜 (closedBall x r)

Tactic:
(subsingleton_closedBall x hr).strictConvex

Premises used: Set.Subsingleton.strictConvex, Metric.subsingleton_closedBall
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
⊢ StrictConvex 𝕜 (closedBall x r)

Tactic:
exact (subsingleton_closedBall x hr).strictConvex

Premises used: Set.Subsingleton.strictConvex, Metric.subsingleton_closedBall
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : 0 < r
inr : StrictConvex 𝕜 (HVAdd.hVAdd (β := Set E) x (closedBall 0 r))
⊢ StrictConvex 𝕜 (closedBall x r)

Tactic:
rw [← vadd_closedBall_zero]

Premises used: vadd_closedBall_zero
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : 0 < r
⊢ StrictConvex 𝕜 (HVAdd.hVAdd (β := Set E) x (closedBall 0 r))

Tactic:
(StrictConvexSpace.strictConvex_closedBall r hr).vadd _

Premises used: StrictConvexSpace.strictConvex_closedBall, StrictConvex.vadd
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : 0 < r
⊢ StrictConvex 𝕜 (HVAdd.hVAdd (β := Set E) x (closedBall 0 r))

Tactic:
exact (StrictConvexSpace.strictConvex_closedBall r hr).vadd _

Premises used: StrictConvexSpace.strictConvex_closedBall, StrictConvex.vadd
-- Module: Mathlib.Analysis.Convex.StrictConvexSpace
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace ℝ E
inst_5 : LinearMap.CompatibleSMul E E 𝕜 ℝ
h : StrictConvex.{u_1, u_2} 𝕜 (E := E) (closedBall 0 1)
r : ℝ
hr : 0 < r
⊢ StrictConvex.{u_1, u_2} 𝕜 (E := E) (closedBall 0 r)

Tactic:
simpa only [smul_unitClosedBall_of_nonneg hr.le] using h.smul r

Premises used: smul_unitClosedBall_of_nonneg, LT.lt.le, StrictConvex.smul
-- 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 → ∃ (a : ℝ) (b : ℝ), a + b = 1 ∧ ‖a • x + b • y‖ < 1
⊢ StrictConvexSpace ℝ E

Tactic:
StrictConvexSpace.of_strictConvex_unitClosedBall ℝ
      ((convex_closedBall _ _).strictConvex' fun x hx y hy hne => ?_)

Premises used: Real, StrictConvexSpace.of_strictConvex_unitClosedBall, Convex.strictConvex', convex_closedBall
-- 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 → ∃ (a : ℝ) (b : ℝ), a + b = 1 ∧ ‖a • x + b • y‖ < 1
_ :
  ∀ (x : E) (hx : Membership.mem (γ := Set E) (closedBall 0 1 \ interior (closedBall 0 1)) x) (y : E)
    (hy : Membership.mem (γ := Set E) (closedBall 0 1 \ interior (closedBall 0 1)) y) (hne : x ≠ y),
    (fun (x y : E) ↦
        ∃ (c : ℝ),
          Membership.mem (α := E) (γ := Set E) (interior (closedBall 0 1))
            ((AffineMap.lineMap x y : (a : ℝ) → E) c : E))
      x y
⊢ StrictConvexSpace ℝ E

Tactic:
refine
    StrictConvexSpace.of_strictConvex_unitClosedBall ℝ
      ((convex_closedBall _ _).strictConvex' fun x hx y hy hne => ?_)

Premises used: Real, StrictConvexSpace.of_strictConvex_unitClosedBall, Convex.strictConvex', convex_closedBall
-- 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 → ∃ (a : ℝ) (b : ℝ), a + b = 1 ∧ ‖a • x + b • y‖ < 1
x : E
hx : Membership.mem (γ := Set E) (closedBall 0 1 \ interior (closedBall 0 1)) x
y : E
hy : Membership.mem (γ := Set E) (closedBall 0 1 \ interior (closedBall 0 1)) y
hne : x ≠ y
rw :
  ∀ (hx : ‖x‖ = 1) (y : E) (hy : ‖y‖ = 1) (hne : x ≠ y),
    ∃ (c : ℝ),
      Membership.mem (α := E) (γ := Set E) (interior (closedBall 0 1)) ((AffineMap.lineMap x y : (a : ℝ) → E) c : E)
⊢ ∃ (c : ℝ),
    Membership.mem (α := E) (γ := Set E) (interior (closedBall 0 1)) ((AffineMap.lineMap x y : (a : ℝ) → E) c : E)

Tactic:
rw [interior_closedBall (0 : E) one_ne_zero, closedBall_diff_ball,
    mem_sphere_zero_iff_norm] at hx hy

Premises used: interior_closedBall, mem_sphere_zero_iff_norm, Metric.closedBall_diff_ball, one_ne_zero, 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 → ∃ (a : ℝ) (b : ℝ), a + b = 1 ∧ ‖a • x + b • y‖ < 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
hne : x ≠ y
rcases :
  ∀ (a b : ℝ) (hab : a + b = 1) (hlt : ‖a • x + b • y‖ < 1),
    ∃ (c : ℝ),
      Membership.mem (α := E) (γ := Set E) (interior (closedBall 0 1)) ((AffineMap.lineMap x y : (a : ℝ) → E) c : E)
⊢ ∃ (c : ℝ),
    Membership.mem (α := E) (γ := Set E) (interior (closedBall 0 1)) ((AffineMap.lineMap x y : (a : ℝ) → E) c : E)

Tactic:
rcases h x y hx hy hne with ⟨a, b, hab, hlt⟩
-- 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 → ∃ (a : ℝ) (b : ℝ), a + b = 1 ∧ ‖a • x + b • y‖ < 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
hne : x ≠ y
a b : ℝ
hab : a + b = 1
hlt : ‖a • x + b • y‖ < 1
h₁ : Membership.mem (α := E) (γ := Set E) (interior (closedBall 0 1)) ((AffineMap.lineMap x y : (a : ℝ) → E) b : E)
⊢ ∃ (c : ℝ),
    Membership.mem (α := E) (γ := Set E) (interior (closedBall 0 1)) ((AffineMap.lineMap x y : (a : ℝ) → E) c : E)

Tactic:
use b
-- 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 → ∃ (a : ℝ) (b : ℝ), a + b = 1 ∧ ‖a • x + b • y‖ < 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
hne : x ≠ y
a b : ℝ
hab : a + b = 1
hlt : ‖a • x + b • y‖ < 1
h₁ : Membership.mem (γ := Set E) (interior (closedBall 0 1)) ((1 - b) • x + b • y)
h₂ : Membership.mem (γ := Set E) (ball 0 1) ((1 - b) • x + b • y)
h₃ : ‖(1 - b) • x + b • y‖ < 1
h₄ h₅ h₆ h₇ : ‖a • x + b • y‖ < 1
⊢ Membership.mem (α := E) (γ := Set E) (interior (closedBall 0 1)) ((AffineMap.lineMap x y : (a : ℝ) → E) b : E)

Tactic:
rwa [AffineMap.lineMap_apply_module, interior_closedBall (0 : E) one_ne_zero, mem_ball_zero_iff,
    sub_eq_iff_eq_add.2 hab.symm]

Premises used: AffineMap.lineMap_apply_module, Iff.mpr, interior_closedBall, sub_eq_iff_eq_add, one_ne_zero, OfNat.ofNat, Eq.symm, mem_ball_zero_iff
-- 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 → ∃ (a : ℝ) (b : ℝ), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ‖a • x + b • y‖ ≠ 1
⊢ StrictConvexSpace ℝ E

Tactic:
StrictConvexSpace.of_strictConvex_unitClosedBall ℝ
    ((convex_closedBall _ _).strictConvex ?_)

Premises used: Real, Convex.strictConvex, StrictConvexSpace.of_strictConvex_unitClosedBall, convex_closedBall
-- 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 → ∃ (a : ℝ) (b : ℝ), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ‖a • x + b • y‖ ≠ 1
refine :
  Set.Pairwise (closedBall 0 1 \ interior (closedBall 0 1)) fun (x y : E) ↦
    ([x -[ℝ] y] \ frontier (closedBall 0 1)).Nonempty
⊢ StrictConvexSpace ℝ E

Tactic:
refine StrictConvexSpace.of_strictConvex_unitClosedBall ℝ
    ((convex_closedBall _ _).strictConvex ?_)

Premises used: Real, Convex.strictConvex, StrictConvexSpace.of_strictConvex_unitClosedBall, convex_closedBall
-- 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 → ∃ (a : ℝ) (b : ℝ), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ‖a • x + b • y‖ ≠ 1
simp : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → x ≠ y → ([x -[ℝ] y] \ sphere 0 1).Nonempty
⊢ Set.Pairwise (closedBall 0 1 \ interior (closedBall 0 1)) fun (x y : E) ↦
    ([x -[ℝ] y] \ frontier (closedBall 0 1)).Nonempty

Tactic:
simp only [interior_closedBall _ one_ne_zero, closedBall_diff_ball, Set.Pairwise,
    frontier_closedBall _ one_ne_zero, mem_sphere_zero_iff_norm]

Premises used: interior_closedBall, mem_sphere_zero_iff_norm, Set.Pairwise, frontier_closedBall, Metric.closedBall_diff_ball, one_ne_zero
-- 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 → ∃ (a : ℝ) (b : ℝ), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ‖a • x + b • y‖ ≠ 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
hne : x ≠ y
rcases :
  ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (hne' : ‖a • x + b • y‖ ≠ 1),
    ([x -[ℝ] y] \ sphere 0 1).Nonempty
⊢ ([x -[ℝ] y] \ sphere 0 1).Nonempty

Tactic:
rcases h x y hx hy hne with ⟨a, b, ha, hb, hab, 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 → ∃ (a : ℝ) (b : ℝ), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ‖a • x + b • y‖ ≠ 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
hne : x ≠ y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hne' : ‖a • x + b • y‖ ≠ 1
⊢ ([x -[ℝ] y] \ sphere 0 1).Nonempty

Tactic:
⟨_, ⟨a, b, ha, hb, hab, rfl⟩, mt mem_sphere_zero_iff_norm.1 hne'⟩

Premises used: mt, mem_sphere_zero_iff_norm, Set.Nonempty, And.intro, Exists.intro, Iff.mp, rfl
-- 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 → ∃ (a : ℝ) (b : ℝ), 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ‖a • x + b • y‖ ≠ 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
hne : x ≠ y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
hne' : ‖a • x + b • y‖ ≠ 1
⊢ ([x -[ℝ] y] \ sphere 0 1).Nonempty

Tactic:
exact ⟨_, ⟨a, b, ha, hb, hab, rfl⟩, mt mem_sphere_zero_iff_norm.1 hne'⟩