V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = abs (‖x‖ - ‖y‖)
⊢ angle x y = 0
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x - y‖ = abs (‖x‖ - ‖y‖) ↔ angle x y = 0
refine' ⟨fun h => _, norm_sub_eq_abs_sub_norm_of_angle_eq_zero⟩
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = abs (‖x‖ - ‖y‖)
⊢ inner x y = ‖x‖ * ‖y‖
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = abs (‖x‖ - ‖y‖)
⊢ angle x y = 0
rw [← inner_eq_mul_norm_iff_angle_eq_zero hx hy]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = abs (‖x‖ - ‖y‖)
h1 : ‖x - y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2
⊢ inner x y = ‖x‖ * ‖y‖
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = abs (‖x‖ - ‖y‖)
⊢ inner x y = ‖x‖ * ‖y‖
have h1 : ‖x - y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2 := by
  rw [h]
  exact sq_abs (‖x‖ - ‖y‖)
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = abs (‖x‖ - ‖y‖)
h1✝ : ‖x - y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2
h1 : ‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2
⊢ inner x y = ‖x‖ * ‖y‖
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = abs (‖x‖ - ‖y‖)
h1 : ‖x - y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2
⊢ inner x y = ‖x‖ * ‖y‖
rw [norm_sub_pow_two_real] at h1
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = abs (‖x‖ - ‖y‖)
h1✝ : ‖x - y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2
h1 : ‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2
⊢ inner x y = ‖x‖ * ‖y‖
calc
  ⟪x, y⟫ = ((‖x‖ + ‖y‖) ^ 2 - ‖x‖ ^ 2 - ‖y‖ ^ 2) / 2 := by linarith
  _ = ‖x‖ * ‖y‖ := by ring
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = abs (‖x‖ - ‖y‖)
⊢ abs (‖x‖ - ‖y‖) ^ 2 = (‖x‖ - ‖y‖) ^ 2
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = abs (‖x‖ - ‖y‖)
⊢ ‖x - y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2
rw [h]
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = abs (‖x‖ - ‖y‖)
⊢ abs (‖x‖ - ‖y‖) ^ 2 = (‖x‖ - ‖y‖) ^ 2
exact sq_abs (‖x‖ - ‖y‖)
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = abs (‖x‖ - ‖y‖)
h1✝ : ‖x - y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2
h1 : ‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2
⊢ inner x y = ((‖x‖ + ‖y‖) ^ 2 - ‖x‖ ^ 2 - ‖y‖ ^ 2) / 2
linarith
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = abs (‖x‖ - ‖y‖)
h1✝ : ‖x - y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2
h1 : ‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2 = (‖x‖ - ‖y‖) ^ 2
⊢ ((‖x‖ + ‖y‖) ^ 2 - ‖x‖ ^ 2 - ‖y‖ ^ 2) / 2 = ‖x‖ * ‖y‖
ring