V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
⊢ ‖x‖ ^ 2 + 2 * inner x y + ‖y‖ ^ 2 = ‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2 ↔ inner x y = 0
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
⊢ ‖x + y‖ = ‖x - y‖ ↔ angle x y = π / 2
rw [← sq_eq_sq (norm_nonneg (x + y)) (norm_nonneg (x - y)),
  ← inner_eq_zero_iff_angle_eq_pi_div_two x y, norm_add_pow_two_real, norm_sub_pow_two_real]
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y✝ x y : V
⊢ ‖x‖ ^ 2 + 2 * inner x y + ‖y‖ ^ 2 = ‖x‖ ^ 2 - 2 * inner x y + ‖y‖ ^ 2 ↔ inner x y = 0
constructor <;> intro h <;> linarith