[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : StrictConvexSpace 𝕜 E
x : E
r : ℝ
⊢ StrictConvex 𝕜 (closedBall x r)
[PROOFSTEP]
cases' le_or_lt r 0 with hr hr
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
⊢ StrictConvex 𝕜 (closedBall x r)
[PROOFSTEP]
exact (subsingleton_closedBall x hr).strictConvex
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : 0 < r
⊢ StrictConvex 𝕜 (closedBall x r)
[PROOFSTEP]
rw [← vadd_closedBall_zero]
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : StrictConvexSpace 𝕜 E
x : E
r : ℝ
hr : 0 < r
⊢ StrictConvex 𝕜 (x +ᵥ closedBall 0 r)
[PROOFSTEP]
exact (StrictConvexSpace.strictConvex_closedBall r hr).vadd _
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : LinearMap.CompatibleSMul E E 𝕜 ℝ
h : StrictConvex 𝕜 (closedBall 0 1)
r : ℝ
hr : 0 < r
⊢ StrictConvex 𝕜 (closedBall 0 r)
[PROOFSTEP]
simpa only [smul_closedUnitBall_of_nonneg hr.le] using h.smul r
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, a + b = 1 ∧ ‖a • x + b • y‖ < 1
⊢ StrictConvexSpace ℝ E
[PROOFSTEP]
refine'
  StrictConvexSpace.of_strictConvex_closed_unit_ball ℝ ((convex_closedBall _ _).strictConvex' fun x hx y hy hne => _)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : 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 ∈ closedBall 0 1 \ interior (closedBall 0 1)
y : E
hy : y ∈ closedBall 0 1 \ interior (closedBall 0 1)
hne : x ≠ y
⊢ (fun x y => ∃ c, ↑(AffineMap.lineMap x y) c ∈ interior (closedBall 0 1)) x y
[PROOFSTEP]
rw [interior_closedBall (0 : E) one_ne_zero, closedBall_diff_ball, mem_sphere_zero_iff_norm] at hx hy 
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : 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
⊢ ∃ c, ↑(AffineMap.lineMap x y) c ∈ interior (closedBall 0 1)
[PROOFSTEP]
rcases h x y hx hy hne with ⟨a, b, hab, hlt⟩
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : 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
⊢ ∃ c, ↑(AffineMap.lineMap x y) c ∈ interior (closedBall 0 1)
[PROOFSTEP]
use b
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : 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
⊢ ↑(AffineMap.lineMap x y) b ∈ interior (closedBall 0 1)
[PROOFSTEP]
rwa [AffineMap.lineMap_apply_module, interior_closedBall (0 : E) one_ne_zero, mem_ball_zero_iff,
  sub_eq_iff_eq_add.2 hab.symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : 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
[PROOFSTEP]
refine' StrictConvexSpace.of_strictConvex_closed_unit_ball ℝ ((convex_closedBall _ _).strictConvex _)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : 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
⊢ Set.Pairwise (closedBall 0 1 \ interior (closedBall 0 1)) fun x y =>
    Set.Nonempty ([x-[ℝ]y] \ frontier (closedBall 0 1))
[PROOFSTEP]
simp only [interior_closedBall _ one_ne_zero, closedBall_diff_ball, Set.Pairwise, frontier_closedBall _ one_ne_zero,
  mem_sphere_zero_iff_norm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : 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⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → x ≠ y → Set.Nonempty ([x-[ℝ]y] \ sphere 0 1)
[PROOFSTEP]
intro x hx y hy hne
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : 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
⊢ Set.Nonempty ([x-[ℝ]y] \ sphere 0 1)
[PROOFSTEP]
rcases h x y hx hy hne with ⟨a, b, ha, hb, hab, hne'⟩
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : 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
⊢ Set.Nonempty ([x-[ℝ]y] \ sphere 0 1)
[PROOFSTEP]
exact ⟨_, ⟨a, b, ha, hb, hab, rfl⟩, mt mem_sphere_zero_iff_norm.1 hne'⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
h : ∀ ⦃x y : E⦄, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ‖x + y‖ ≠ 2
⊢ StrictConvexSpace ℝ E
[PROOFSTEP]
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 _, _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : 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
⊢ ‖(1 / 2) • x + (1 / 2) • y‖ ≠ 1
[PROOFSTEP]
rw [← smul_add, norm_smul, Real.norm_of_nonneg one_half_pos.le, one_div, ← div_eq_inv_mul, Ne.def,
  div_eq_one_iff_eq (two_ne_zero' ℝ)]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : 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
[PROOFSTEP]
exact h hx hy hne
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y
⊢ StrictConvexSpace ℝ E
[PROOFSTEP]
refine' StrictConvexSpace.of_pairwise_sphere_norm_ne_two fun x hx y hy => mt fun h₂ => _
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → ‖x + y‖ = 2 → SameRay ℝ x y
x : E
hx : x ∈ sphere 0 1
y : E
hy : y ∈ sphere 0 1
h₂ : ‖x + y‖ = 2
⊢ x = y
[PROOFSTEP]
rw [mem_sphere_zero_iff_norm] at hx hy 
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedLinearOrderedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : 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
[PROOFSTEP]
exact (sameRay_iff_of_norm_eq (hx.trans hy.symm)).1 (h x y hx hy h₂)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : 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
⊢ a • x + b • y ∈ ball z r
[PROOFSTEP]
rcases eq_or_ne r 0 with (rfl | hr)
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : 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
⊢ a • x + b • y ∈ ball z 0
[PROOFSTEP]
rw [closedBall_zero, mem_singleton_iff] at hx hy 
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : 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
[PROOFSTEP]
exact (hne (hx.trans hy.symm)).elim
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : 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 ∈ ball z r
[PROOFSTEP]
simp only [← interior_closedBall _ hr] at hx hy ⊢
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : 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)
[PROOFSTEP]
exact strictConvex_closedBall ℝ z r hx hy hne ha hb hab
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
hx : ‖x‖ ≤ r
hy : ‖y‖ ≤ r
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ‖a • x + b • y‖ < r
[PROOFSTEP]
simp only [← mem_ball_zero_iff, ← mem_closedBall_zero_iff] at hx hy ⊢
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
hne : x ≠ y
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : x ∈ closedBall 0 r
hy : y ∈ closedBall 0 r
⊢ a • x + b • y ∈ ball 0 r
[PROOFSTEP]
exact combo_mem_ball_of_ne hx hy hne ha hb hab
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
h : ¬SameRay ℝ x y
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
[PROOFSTEP]
simp only [sameRay_iff_inv_norm_smul_eq, not_or, ← Ne.def] at h 
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
h : x ≠ 0 ∧ y ≠ 0 ∧ ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
[PROOFSTEP]
rcases h with ⟨hx, hy, hne⟩
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
hx : x ≠ 0
hy : y ≠ 0
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
[PROOFSTEP]
rw [← norm_pos_iff] at hx hy 
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
[PROOFSTEP]
have hxy : 0 < ‖x‖ + ‖y‖ := add_pos hx hy
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
[PROOFSTEP]
have :=
  combo_mem_ball_of_ne (inv_norm_smul_mem_closed_unit_ball x) (inv_norm_smul_mem_closed_unit_ball y) hne
    (div_pos hx hxy) (div_pos hy hxy) (by rw [← add_div, div_self hxy.ne'])
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
⊢ ‖x‖ / (‖x‖ + ‖y‖) + ‖y‖ / (‖x‖ + ‖y‖) = 1
[PROOFSTEP]
rw [← add_div, div_self hxy.ne']
[GOAL]
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
hx : 0 < ‖x‖
hy : 0 < ‖y‖
hne : ‖x‖⁻¹ • x ≠ ‖y‖⁻¹ • y
hxy : 0 < ‖x‖ + ‖y‖
this : (‖x‖ / (‖x‖ + ‖y‖)) • ‖x‖⁻¹ • x + (‖y‖ / (‖x‖ + ‖y‖)) • ‖y‖⁻¹ • y ∈ ball 0 1
⊢ ‖x + y‖ < ‖x‖ + ‖y‖
[PROOFSTEP]
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 
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
h : ¬SameRay ℝ x y
⊢ ‖x‖ - ‖y‖ < ‖x - y‖
[PROOFSTEP]
nth_rw 1 [← sub_add_cancel x y] at h ⊢
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
h : ¬SameRay ℝ (x - y + y) y
⊢ ‖x - y + y‖ - ‖y‖ < ‖x - y‖
[PROOFSTEP]
exact sub_lt_iff_lt_add.2 (norm_add_lt_of_not_sameRay fun H' => h <| H'.add_left SameRay.rfl)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
h : ¬SameRay ℝ x y
⊢ |‖x‖ - ‖y‖| < ‖x - y‖
[PROOFSTEP]
refine' abs_sub_lt_iff.2 ⟨lt_norm_sub_of_not_sameRay h, _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
h : ¬SameRay ℝ x y
⊢ ‖y‖ - ‖x‖ < ‖x - y‖
[PROOFSTEP]
rw [norm_sub_rev]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
h : ¬SameRay ℝ x y
⊢ ‖y‖ - ‖x‖ < ‖y - x‖
[PROOFSTEP]
exact lt_norm_sub_of_not_sameRay (mt SameRay.symm h)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
⊢ dist x y + dist y z = dist x z ↔ y ∈ [x-[ℝ]z]
[PROOFSTEP]
simp only [mem_segment_iff_sameRay, sameRay_iff_norm_add, dist_eq_norm', sub_add_sub_cancel', eq_comm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
h : ‖x‖ = ‖y‖
⊢ ‖(1 / 2) • (x + y)‖ < ‖x‖ ↔ x ≠ y
[PROOFSTEP]
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]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NormedLinearOrderedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : StrictConvexSpace ℝ E
x✝ y✝ z✝ : E
a b r : ℝ
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
PF : Type u
PE : Type u_4
inst✝³ : MetricSpace PF
inst✝² : MetricSpace PE
inst✝¹ : NormedAddTorsor F PF
inst✝ : NormedAddTorsor E PE
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
⊢ y = ↑(AffineMap.lineMap x z) r
[PROOFSTEP]
have : y -ᵥ x ∈ [(0 : E)-[ℝ]z -ᵥ x] := by
  rw [← dist_add_dist_eq_iff, dist_zero_left, dist_vsub_cancel_right, ← dist_eq_norm_vsub', ← dist_eq_norm_vsub', hxy,
    hyz, ← add_mul, add_sub_cancel'_right, one_mul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NormedLinearOrderedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : StrictConvexSpace ℝ E
x✝ y✝ z✝ : E
a b r : ℝ
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
PF : Type u
PE : Type u_4
inst✝³ : MetricSpace PF
inst✝² : MetricSpace PE
inst✝¹ : NormedAddTorsor F PF
inst✝ : NormedAddTorsor E PE
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]
[PROOFSTEP]
rw [← dist_add_dist_eq_iff, dist_zero_left, dist_vsub_cancel_right, ← dist_eq_norm_vsub', ← dist_eq_norm_vsub', hxy,
  hyz, ← add_mul, add_sub_cancel'_right, one_mul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NormedLinearOrderedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : StrictConvexSpace ℝ E
x✝ y✝ z✝ : E
a b r : ℝ
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
PF : Type u
PE : Type u_4
inst✝³ : MetricSpace PF
inst✝² : MetricSpace PE
inst✝¹ : NormedAddTorsor F PF
inst✝ : NormedAddTorsor E PE
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]
⊢ y = ↑(AffineMap.lineMap x z) r
[PROOFSTEP]
rcases eq_or_ne x z with (rfl | hne)
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NormedLinearOrderedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : StrictConvexSpace ℝ E
x✝ y✝ z : E
a b r : ℝ
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
PF : Type u
PE : Type u_4
inst✝³ : MetricSpace PF
inst✝² : MetricSpace PE
inst✝¹ : NormedAddTorsor F PF
inst✝ : NormedAddTorsor E PE
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 = ↑(AffineMap.lineMap x x) r
[PROOFSTEP]
obtain rfl : y = x := by simpa
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NormedLinearOrderedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : StrictConvexSpace ℝ E
x✝ y✝ z : E
a b r : ℝ
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
PF : Type u
PE : Type u_4
inst✝³ : MetricSpace PF
inst✝² : MetricSpace PE
inst✝¹ : NormedAddTorsor F PF
inst✝ : NormedAddTorsor E PE
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
[PROOFSTEP]
simpa
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NormedLinearOrderedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : StrictConvexSpace ℝ E
x y✝ z : E
a b r : ℝ
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
PF : Type u
PE : Type u_4
inst✝³ : MetricSpace PF
inst✝² : MetricSpace PE
inst✝¹ : NormedAddTorsor F PF
inst✝ : NormedAddTorsor E PE
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) r
[PROOFSTEP]
simp
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NormedLinearOrderedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : StrictConvexSpace ℝ E
x✝ y✝ z✝ : E
a b r : ℝ
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
PF : Type u
PE : Type u_4
inst✝³ : MetricSpace PF
inst✝² : MetricSpace PE
inst✝¹ : NormedAddTorsor F PF
inst✝ : NormedAddTorsor E PE
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
⊢ y = ↑(AffineMap.lineMap x z) r
[PROOFSTEP]
rw [← dist_ne_zero] at hne 
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NormedLinearOrderedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : StrictConvexSpace ℝ E
x✝ y✝ z✝ : E
a b r : ℝ
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
PF : Type u
PE : Type u_4
inst✝³ : MetricSpace PF
inst✝² : MetricSpace PE
inst✝¹ : NormedAddTorsor F PF
inst✝ : NormedAddTorsor E PE
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
hne : dist x z ≠ 0
⊢ y = ↑(AffineMap.lineMap x z) r
[PROOFSTEP]
rcases this with ⟨a, b, _, hb, _, H⟩
[GOAL]
case inr.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NormedLinearOrderedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : StrictConvexSpace ℝ E
x✝ y✝ z✝ : E
a✝ b✝ r : ℝ
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
PF : Type u
PE : Type u_4
inst✝³ : MetricSpace PF
inst✝² : MetricSpace PE
inst✝¹ : NormedAddTorsor F PF
inst✝ : NormedAddTorsor E PE
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
hne✝ : x ≠ z
hne : dist x z ≠ 0
a b : ℝ
w✝¹ : 0 ≤ a
hb : 0 ≤ b
w✝ : a + b = 1
H : a • 0 + b • (z -ᵥ x) = y -ᵥ x
⊢ y = ↑(AffineMap.lineMap x z) r
[PROOFSTEP]
rw [smul_zero, zero_add] at H 
[GOAL]
case inr.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NormedLinearOrderedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : StrictConvexSpace ℝ E
x✝ y✝ z✝ : E
a✝ b✝ r : ℝ
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
PF : Type u
PE : Type u_4
inst✝³ : MetricSpace PF
inst✝² : MetricSpace PE
inst✝¹ : NormedAddTorsor F PF
inst✝ : NormedAddTorsor E PE
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
hne✝ : x ≠ z
hne : dist x z ≠ 0
a b : ℝ
w✝¹ : 0 ≤ a
hb : 0 ≤ b
w✝ : a + b = 1
H : b • (z -ᵥ x) = y -ᵥ x
⊢ y = ↑(AffineMap.lineMap x z) r
[PROOFSTEP]
have H' := congr_arg norm H
[GOAL]
case inr.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NormedLinearOrderedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : StrictConvexSpace ℝ E
x✝ y✝ z✝ : E
a✝ b✝ r : ℝ
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
PF : Type u
PE : Type u_4
inst✝³ : MetricSpace PF
inst✝² : MetricSpace PE
inst✝¹ : NormedAddTorsor F PF
inst✝ : NormedAddTorsor E PE
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
hne✝ : x ≠ z
hne : dist x z ≠ 0
a b : ℝ
w✝¹ : 0 ≤ a
hb : 0 ≤ b
w✝ : a + b = 1
H : b • (z -ᵥ x) = y -ᵥ x
H' : ‖b • (z -ᵥ x)‖ = ‖y -ᵥ x‖
⊢ y = ↑(AffineMap.lineMap x z) r
[PROOFSTEP]
rw [norm_smul, Real.norm_of_nonneg hb, ← dist_eq_norm_vsub', ← dist_eq_norm_vsub', hxy, mul_left_inj' hne] at H' 
[GOAL]
case inr.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NormedLinearOrderedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : StrictConvexSpace ℝ E
x✝ y✝ z✝ : E
a✝ b✝ r : ℝ
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
PF : Type u
PE : Type u_4
inst✝³ : MetricSpace PF
inst✝² : MetricSpace PE
inst✝¹ : NormedAddTorsor F PF
inst✝ : NormedAddTorsor E PE
x y z : PE
hxy : dist x y = r * dist x z
hyz : dist y z = (1 - r) * dist x z
hne✝ : x ≠ z
hne : dist x z ≠ 0
a b : ℝ
w✝¹ : 0 ≤ a
hb : 0 ≤ b
w✝ : a + b = 1
H : b • (z -ᵥ x) = y -ᵥ x
H' : b = r
⊢ y = ↑(AffineMap.lineMap x z) r
[PROOFSTEP]
rw [AffineMap.lineMap_apply, ← H', H, vsub_vadd]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NormedLinearOrderedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : StrictConvexSpace ℝ E
x✝ y✝ z✝ : E
a b r : ℝ
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
PF : Type u
PE : Type u_4
inst✝³ : MetricSpace PF
inst✝² : MetricSpace PE
inst✝¹ : NormedAddTorsor F PF
inst✝ : NormedAddTorsor E PE
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
⊢ y = midpoint ℝ x z
[PROOFSTEP]
apply eq_lineMap_of_dist_eq_mul_of_dist_eq_mul
[GOAL]
case hxy
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NormedLinearOrderedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : StrictConvexSpace ℝ E
x✝ y✝ z✝ : E
a b r : ℝ
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
PF : Type u
PE : Type u_4
inst✝³ : MetricSpace PF
inst✝² : MetricSpace PE
inst✝¹ : NormedAddTorsor F PF
inst✝ : NormedAddTorsor E PE
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
⊢ dist x y = ⅟2 * dist x z
[PROOFSTEP]
rwa [invOf_eq_inv, ← div_eq_inv_mul]
[GOAL]
case hyz
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NormedLinearOrderedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : StrictConvexSpace ℝ E
x✝ y✝ z✝ : E
a b r : ℝ
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
PF : Type u
PE : Type u_4
inst✝³ : MetricSpace PF
inst✝² : MetricSpace PE
inst✝¹ : NormedAddTorsor F PF
inst✝ : NormedAddTorsor E PE
x y z : PE
hx : dist x y = dist x z / 2
hy : dist y z = dist x z / 2
⊢ dist y z = (1 - ⅟2) * dist x z
[PROOFSTEP]
rwa [invOf_eq_inv, ← one_div, sub_half, one_div, ← div_eq_inv_mul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NormedLinearOrderedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : StrictConvexSpace ℝ E
x✝ y✝ z : E
a b r : ℝ
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
PF : Type u
PE : Type u_4
inst✝³ : MetricSpace PF
inst✝² : MetricSpace PE
inst✝¹ : NormedAddTorsor F PF
inst✝ : NormedAddTorsor E PE
f : PF → PE
hi : Isometry f
x y : PF
⊢ f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
[PROOFSTEP]
apply eq_midpoint_of_dist_eq_half
[GOAL]
case hx
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NormedLinearOrderedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : StrictConvexSpace ℝ E
x✝ y✝ z : E
a b r : ℝ
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
PF : Type u
PE : Type u_4
inst✝³ : MetricSpace PF
inst✝² : MetricSpace PE
inst✝¹ : NormedAddTorsor F PF
inst✝ : NormedAddTorsor E PE
f : PF → PE
hi : Isometry f
x y : PF
⊢ dist (f x) (f (midpoint ℝ x y)) = dist (f x) (f y) / 2
[PROOFSTEP]
rw [hi.dist_eq, hi.dist_eq]
[GOAL]
case hx
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NormedLinearOrderedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : StrictConvexSpace ℝ E
x✝ y✝ z : E
a b r : ℝ
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
PF : Type u
PE : Type u_4
inst✝³ : MetricSpace PF
inst✝² : MetricSpace PE
inst✝¹ : NormedAddTorsor F PF
inst✝ : NormedAddTorsor E PE
f : PF → PE
hi : Isometry f
x y : PF
⊢ dist x (midpoint ℝ x y) = dist x y / 2
[PROOFSTEP]
simp only [dist_left_midpoint, Real.norm_of_nonneg zero_le_two, div_eq_inv_mul]
[GOAL]
case hy
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NormedLinearOrderedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : StrictConvexSpace ℝ E
x✝ y✝ z : E
a b r : ℝ
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
PF : Type u
PE : Type u_4
inst✝³ : MetricSpace PF
inst✝² : MetricSpace PE
inst✝¹ : NormedAddTorsor F PF
inst✝ : NormedAddTorsor E PE
f : PF → PE
hi : Isometry f
x y : PF
⊢ dist (f (midpoint ℝ x y)) (f y) = dist (f x) (f y) / 2
[PROOFSTEP]
rw [hi.dist_eq, hi.dist_eq]
[GOAL]
case hy
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NormedLinearOrderedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : StrictConvexSpace ℝ E
x✝ y✝ z : E
a b r : ℝ
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
PF : Type u
PE : Type u_4
inst✝³ : MetricSpace PF
inst✝² : MetricSpace PE
inst✝¹ : NormedAddTorsor F PF
inst✝ : NormedAddTorsor E PE
f : PF → PE
hi : Isometry f
x y : PF
⊢ dist (midpoint ℝ x y) y = dist x y / 2
[PROOFSTEP]
simp only [dist_midpoint_right, Real.norm_of_nonneg zero_le_two, div_eq_inv_mul]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝¹⁰ : NormedLinearOrderedField 𝕜
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : StrictConvexSpace ℝ E
x✝ y z : E
a b r : ℝ
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
PF : Type u
PE : Type u_4
inst✝³ : MetricSpace PF
inst✝² : MetricSpace PE
inst✝¹ : NormedAddTorsor F PF
inst✝ : NormedAddTorsor E PE
f : PF → PE
hi : Isometry f
src✝ : PF →ᵃ[ℝ] PE :=
  AffineMap.ofMapMidpoint f (_ : ∀ (x y : PF), f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)) (_ : Continuous f)
x : F
⊢ ‖↑{ toFun := src✝.toFun, linear := src✝.linear,
              map_vadd' :=
                (_ :
                  ∀ (p : PF) (v : F), AffineMap.toFun src✝ (v +ᵥ p) = ↑src✝.linear v +ᵥ AffineMap.toFun src✝ p) }.linear
        x‖ =
    ‖x‖
[PROOFSTEP]
simp [AffineMap.ofMapMidpoint, ← dist_eq_norm_vsub E, hi.dist_eq]
