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 = 0
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 = 0
refine' ⟨fun h => _, norm_add_eq_add_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‖ = ‖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 = 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‖ = ‖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_add_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‖ + ‖y‖) ^ 2 - ‖x‖ ^ 2 - ‖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‖ + ‖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‖ ^ 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‖ + ‖y‖) ^ 2 - ‖x‖ ^ 2 - ‖y‖ ^ 2) / 2 = ‖x‖ * ‖y‖
ring