V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = ‖x‖ + ‖y‖
⊢ angle x y = π
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x - y‖ = ‖x‖ + ‖y‖ ↔ angle x y = π
refine' ⟨fun h => _, norm_sub_eq_add_norm_of_angle_eq_pi⟩
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
hx : x ≠ 0
hy : y ≠ 0
h : ‖x - y‖ = ‖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‖ = ‖x‖ + ‖y‖
⊢ angle x y = π
rw [← inner_eq_neg_mul_norm_iff_angle_eq_pi 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‖ = ‖x‖ + ‖y‖
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖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‖ = ‖x‖ + ‖y‖
⊢ inner x y = -(‖x‖ * ‖y‖)
obtain ⟨hxy₁, hxy₂⟩ := norm_nonneg (x - y), add_nonneg (norm_nonneg x) (norm_nonneg 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‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
h : ‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖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‖ = ‖x‖ + ‖y‖
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ inner x y = -(‖x‖ * ‖y‖)
rw [← sq_eq_sq hxy₁ hxy₂, norm_sub_pow_two_real] at 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‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
h : ‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ inner x y = -(‖x‖ * ‖y‖)
calc
  ⟪x, y⟫ = (‖x‖ ^ 2 + ‖y‖ ^ 2 - (‖x‖ + ‖y‖) ^ 2) / 2 := by linarith
  _ = -(‖x‖ * ‖y‖) := by ring
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‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
h : ‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ inner x y = (‖x‖ ^ 2 + ‖y‖ ^ 2 - (‖x‖ + ‖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‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
h : ‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2 = (‖x‖ + ‖y‖) ^ 2
hxy₁ : 0 ≤ ‖x - y‖
hxy₂ : 0 ≤ ‖x‖ + ‖y‖
⊢ (‖x‖ ^ 2 + ‖y‖ ^ 2 - (‖x‖ + ‖y‖) ^ 2) / 2 = -(‖x‖ * ‖y‖)
ring