[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ angle x y = π / 2
[PROOFSTEP]
rw [norm_add_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ inner x y = 0 ↔ angle x y = π / 2
[PROOFSTEP]
exact inner_eq_zero_iff_angle_eq_pi_div_two x y
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ angle x y = π / 2
[PROOFSTEP]
rw [norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ inner x y = 0 ↔ angle x y = π / 2
[PROOFSTEP]
exact inner_eq_zero_iff_angle_eq_pi_div_two x y
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ angle x (x + y) = Real.arccos (‖x‖ / ‖x + y‖)
[PROOFSTEP]
rw [angle, inner_add_right, h, add_zero, real_inner_self_eq_norm_mul_norm]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)
[PROOFSTEP]
by_cases hx : ‖x‖ = 0
[GOAL]
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
hx : ‖x‖ = 0
⊢ Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
hx : ¬‖x‖ = 0
⊢ Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)
[PROOFSTEP]
rw [div_mul_eq_div_div, mul_self_div_self]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ angle x (x + y) = Real.arcsin (‖y‖ / ‖x + y‖)
[PROOFSTEP]
have hxy : ‖x + y‖ ^ 2 ≠ 0 :=
  by
  rw [pow_two, norm_add_sq_eq_norm_sq_add_norm_sq_real h, ne_comm]
  refine' ne_of_lt _
  rcases h0 with (h0 | h0)
  · exact Left.add_pos_of_pos_of_nonneg (mul_self_pos.2 (norm_ne_zero_iff.2 h0)) (mul_self_nonneg _)
  · exact Left.add_pos_of_nonneg_of_pos (mul_self_nonneg _) (mul_self_pos.2 (norm_ne_zero_iff.2 h0))
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ ‖x + y‖ ^ 2 ≠ 0
[PROOFSTEP]
rw [pow_two, norm_add_sq_eq_norm_sq_add_norm_sq_real h, ne_comm]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ 0 ≠ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
[PROOFSTEP]
refine' ne_of_lt _
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
[PROOFSTEP]
rcases h0 with (h0 | h0)
[GOAL]
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
[PROOFSTEP]
exact Left.add_pos_of_pos_of_nonneg (mul_self_pos.2 (norm_ne_zero_iff.2 h0)) (mul_self_nonneg _)
[GOAL]
case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : y ≠ 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
[PROOFSTEP]
exact Left.add_pos_of_nonneg_of_pos (mul_self_nonneg _) (mul_self_pos.2 (norm_ne_zero_iff.2 h0))
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y ≠ 0
hxy : ‖x + y‖ ^ 2 ≠ 0
⊢ angle x (x + y) = Real.arcsin (‖y‖ / ‖x + y‖)
[PROOFSTEP]
rw [angle_add_eq_arccos_of_inner_eq_zero h, Real.arccos_eq_arcsin (div_nonneg (norm_nonneg _) (norm_nonneg _)), div_pow,
  one_sub_div hxy]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y ≠ 0
hxy : ‖x + y‖ ^ 2 ≠ 0
⊢ Real.arcsin (Real.sqrt ((‖x + y‖ ^ 2 - ‖x‖ ^ 2) / ‖x + y‖ ^ 2)) = Real.arcsin (‖y‖ / ‖x + y‖)
[PROOFSTEP]
nth_rw 1 [pow_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y ≠ 0
hxy : ‖x + y‖ ^ 2 ≠ 0
⊢ Real.arcsin (Real.sqrt ((‖x + y‖ * ‖x + y‖ - ‖x‖ ^ 2) / ‖x + y‖ ^ 2)) = Real.arcsin (‖y‖ / ‖x + y‖)
[PROOFSTEP]
rw [norm_add_sq_eq_norm_sq_add_norm_sq_real h, pow_two, add_sub_cancel', ← pow_two, ← div_pow,
  Real.sqrt_sq (div_nonneg (norm_nonneg _) (norm_nonneg _))]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ angle x (x + y) = Real.arctan (‖y‖ / ‖x‖)
[PROOFSTEP]
rw [angle_add_eq_arcsin_of_inner_eq_zero h (Or.inl h0), Real.arctan_eq_arcsin, ← div_mul_eq_div_div,
  norm_add_eq_sqrt_iff_real_inner_eq_zero.2 h]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ Real.arcsin (‖y‖ / Real.sqrt (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) = Real.arcsin (‖y‖ / (‖x‖ * Real.sqrt (↑1 + (‖y‖ / ‖x‖) ^ 2)))
[PROOFSTEP]
nth_rw 3 [← Real.sqrt_sq (norm_nonneg x)]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ Real.arcsin (‖y‖ / Real.sqrt (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)) =
    Real.arcsin (‖y‖ / (Real.sqrt (‖x‖ ^ 2) * Real.sqrt (↑1 + (‖y‖ / ‖x‖) ^ 2)))
[PROOFSTEP]
rw_mod_cast [← Real.sqrt_mul (sq_nonneg _), div_pow, pow_two, pow_two, mul_add, mul_one, mul_div, mul_comm (‖x‖ * ‖x‖),
  ← mul_div, div_self (mul_self_pos.2 (norm_ne_zero_iff.2 h0)).ne', mul_one]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
⊢ 0 < angle x (x + y)
[PROOFSTEP]
rw [angle_add_eq_arccos_of_inner_eq_zero h, Real.arccos_pos, norm_add_eq_sqrt_iff_real_inner_eq_zero.2 h]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖x‖ / Real.sqrt (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
hx : x = 0
⊢ ‖x‖ / Real.sqrt (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
hx : ¬x = 0
⊢ ‖x‖ / Real.sqrt (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖) < 1
[PROOFSTEP]
rw [div_lt_one
    (Real.sqrt_pos.2 (Left.add_pos_of_pos_of_nonneg (mul_self_pos.2 (norm_ne_zero_iff.2 hx)) (mul_self_nonneg _))),
  Real.lt_sqrt (norm_nonneg _), pow_two]
[GOAL]
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
hx : ¬x = 0
⊢ ‖x‖ * ‖x‖ < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
[PROOFSTEP]
simpa [hx] using h0
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ angle x (x + y) ≤ π / 2
[PROOFSTEP]
rw [angle_add_eq_arccos_of_inner_eq_zero h, Real.arccos_le_pi_div_two]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ 0 ≤ ‖x‖ / ‖x + y‖
[PROOFSTEP]
exact div_nonneg (norm_nonneg _) (norm_nonneg _)
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ angle x (x + y) < π / 2
[PROOFSTEP]
rw [angle_add_eq_arccos_of_inner_eq_zero h, Real.arccos_lt_pi_div_two, norm_add_eq_sqrt_iff_real_inner_eq_zero.2 h]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ 0 < ‖x‖ / Real.sqrt (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖)
[PROOFSTEP]
exact
  div_pos (norm_pos_iff.2 h0)
    (Real.sqrt_pos.2 (Left.add_pos_of_pos_of_nonneg (mul_self_pos.2 (norm_ne_zero_iff.2 h0)) (mul_self_nonneg _)))
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ Real.cos (angle x (x + y)) = ‖x‖ / ‖x + y‖
[PROOFSTEP]
rw [angle_add_eq_arccos_of_inner_eq_zero h,
  Real.cos_arccos (le_trans (by norm_num) (div_nonneg (norm_nonneg _) (norm_nonneg _)))
    (div_le_one_of_le _ (norm_nonneg _))]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ -1 ≤ 0
[PROOFSTEP]
norm_num
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ ‖x‖ ≤ ‖x + y‖
[PROOFSTEP]
rw [mul_self_le_mul_self_iff (norm_nonneg _) (norm_nonneg _), norm_add_sq_eq_norm_sq_add_norm_sq_real h]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ ‖x‖ * ‖x‖ ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
[PROOFSTEP]
exact le_add_of_nonneg_right (mul_self_nonneg _)
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ Real.sin (angle x (x + y)) = ‖y‖ / ‖x + y‖
[PROOFSTEP]
rw [angle_add_eq_arcsin_of_inner_eq_zero h h0,
  Real.sin_arcsin (le_trans (by norm_num) (div_nonneg (norm_nonneg _) (norm_nonneg _)))
    (div_le_one_of_le _ (norm_nonneg _))]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ -1 ≤ 0
[PROOFSTEP]
norm_num
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ ‖y‖ ≤ ‖x + y‖
[PROOFSTEP]
rw [mul_self_le_mul_self_iff (norm_nonneg _) (norm_nonneg _), norm_add_sq_eq_norm_sq_add_norm_sq_real h]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ ‖y‖ * ‖y‖ ≤ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
[PROOFSTEP]
exact le_add_of_nonneg_left (mul_self_nonneg _)
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖
[PROOFSTEP]
by_cases h0 : x = 0
[GOAL]
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0
⊢ Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖
[PROOFSTEP]
simp [h0]
[GOAL]
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬x = 0
⊢ Real.tan (angle x (x + y)) = ‖y‖ / ‖x‖
[PROOFSTEP]
rw [angle_add_eq_arctan_of_inner_eq_zero h h0, Real.tan_arctan]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ Real.cos (angle x (x + y)) * ‖x + y‖ = ‖x‖
[PROOFSTEP]
rw [cos_angle_add_of_inner_eq_zero h]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
[PROOFSTEP]
by_cases hxy : ‖x + y‖ = 0
[GOAL]
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
hxy : ‖x + y‖ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
[PROOFSTEP]
have h' := norm_add_sq_eq_norm_sq_add_norm_sq_real h
[GOAL]
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
hxy : ‖x + y‖ = 0
h' : ‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
[PROOFSTEP]
rw [hxy, zero_mul, eq_comm, add_eq_zero_iff' (mul_self_nonneg ‖x‖) (mul_self_nonneg ‖y‖), mul_self_eq_zero] at h'
[GOAL]
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
hxy : ‖x + y‖ = 0
h' : ‖x‖ = 0 ∧ ‖y‖ * ‖y‖ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
[PROOFSTEP]
simp [h'.1]
[GOAL]
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
hxy : ¬‖x + y‖ = 0
⊢ ‖x‖ / ‖x + y‖ * ‖x + y‖ = ‖x‖
[PROOFSTEP]
exact div_mul_cancel _ hxy
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖
[PROOFSTEP]
by_cases h0 : x = 0 ∧ y = 0
[GOAL]
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∧ y = 0
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖
[PROOFSTEP]
simp [h0]
[GOAL]
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬(x = 0 ∧ y = 0)
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖
[PROOFSTEP]
rw [not_and_or] at h0
[GOAL]
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬x = 0 ∨ ¬y = 0
⊢ Real.sin (angle x (x + y)) * ‖x + y‖ = ‖y‖
[PROOFSTEP]
rw [sin_angle_add_of_inner_eq_zero h h0, div_mul_cancel]
[GOAL]
case neg.h
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬x = 0 ∨ ¬y = 0
⊢ ‖x + y‖ ≠ 0
[PROOFSTEP]
rw [← mul_self_ne_zero, norm_add_sq_eq_norm_sq_add_norm_sq_real h]
[GOAL]
case neg.h
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬x = 0 ∨ ¬y = 0
⊢ ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ≠ 0
[PROOFSTEP]
refine' (ne_of_lt _).symm
[GOAL]
case neg.h
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬x = 0 ∨ ¬y = 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
[PROOFSTEP]
rcases h0 with (h0 | h0)
[GOAL]
case neg.h.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬x = 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
[PROOFSTEP]
exact Left.add_pos_of_pos_of_nonneg (mul_self_pos.2 (norm_ne_zero_iff.2 h0)) (mul_self_nonneg _)
[GOAL]
case neg.h.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : ¬y = 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
[PROOFSTEP]
exact Left.add_pos_of_nonneg_of_pos (mul_self_nonneg _) (mul_self_pos.2 (norm_ne_zero_iff.2 h0))
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y = 0
⊢ Real.tan (angle x (x + y)) * ‖x‖ = ‖y‖
[PROOFSTEP]
rw [tan_angle_add_of_inner_eq_zero h]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y = 0
⊢ ‖y‖ / ‖x‖ * ‖x‖ = ‖y‖
[PROOFSTEP]
rcases h0 with (h0 | h0)
[GOAL]
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ ‖y‖ / ‖x‖ * ‖x‖ = ‖y‖
[PROOFSTEP]
simp [h0]
[GOAL]
case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : y = 0
⊢ ‖y‖ / ‖x‖ * ‖x‖ = ‖y‖
[PROOFSTEP]
simp [h0]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y = 0
⊢ ‖x‖ / Real.cos (angle x (x + y)) = ‖x + y‖
[PROOFSTEP]
rw [cos_angle_add_of_inner_eq_zero h]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y = 0
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖
[PROOFSTEP]
rcases h0 with (h0 | h0)
[GOAL]
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖
[PROOFSTEP]
rw [div_div_eq_mul_div, mul_comm, div_eq_mul_inv, mul_inv_cancel_right₀ (norm_ne_zero_iff.2 h0)]
[GOAL]
case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : y = 0
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖
[PROOFSTEP]
simp [h0]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖
[PROOFSTEP]
rcases h0 with (h0 | h0)
[GOAL]
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0
⊢ ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖
[PROOFSTEP]
simp [h0]
[GOAL]
case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : y ≠ 0
⊢ ‖y‖ / Real.sin (angle x (x + y)) = ‖x + y‖
[PROOFSTEP]
rw [sin_angle_add_of_inner_eq_zero h (Or.inr h0), div_div_eq_mul_div, mul_comm, div_eq_mul_inv,
  mul_inv_cancel_right₀ (norm_ne_zero_iff.2 h0)]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / Real.tan (angle x (x + y)) = ‖x‖
[PROOFSTEP]
rw [tan_angle_add_of_inner_eq_zero h]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖
[PROOFSTEP]
rcases h0 with (h0 | h0)
[GOAL]
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0
⊢ ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖
[PROOFSTEP]
simp [h0]
[GOAL]
case inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : y ≠ 0
⊢ ‖y‖ / (‖y‖ / ‖x‖) = ‖x‖
[PROOFSTEP]
rw [div_div_eq_mul_div, mul_comm, div_eq_mul_inv, mul_inv_cancel_right₀ (norm_ne_zero_iff.2 h0)]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ angle x (x - y) = Real.arccos (‖x‖ / ‖x - y‖)
[PROOFSTEP]
rw [← neg_eq_zero, ← inner_neg_right] at h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ angle x (x - y) = Real.arccos (‖x‖ / ‖x - y‖)
[PROOFSTEP]
rw [sub_eq_add_neg, angle_add_eq_arccos_of_inner_eq_zero h]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ angle x (x - y) = Real.arcsin (‖y‖ / ‖x - y‖)
[PROOFSTEP]
rw [← neg_eq_zero, ← inner_neg_right] at h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ angle x (x - y) = Real.arcsin (‖y‖ / ‖x - y‖)
[PROOFSTEP]
rw [or_comm, ← neg_ne_zero, or_comm] at h0
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0 ∨ -y ≠ 0
⊢ angle x (x - y) = Real.arcsin (‖y‖ / ‖x - y‖)
[PROOFSTEP]
rw [sub_eq_add_neg, angle_add_eq_arcsin_of_inner_eq_zero h h0, norm_neg]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ angle x (x - y) = Real.arctan (‖y‖ / ‖x‖)
[PROOFSTEP]
rw [← neg_eq_zero, ← inner_neg_right] at h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0
⊢ angle x (x - y) = Real.arctan (‖y‖ / ‖x‖)
[PROOFSTEP]
rw [sub_eq_add_neg, angle_add_eq_arctan_of_inner_eq_zero h h0, norm_neg]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
⊢ 0 < angle x (x - y)
[PROOFSTEP]
rw [← neg_eq_zero, ← inner_neg_right] at h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x = 0 ∨ y ≠ 0
⊢ 0 < angle x (x - y)
[PROOFSTEP]
rw [← neg_ne_zero] at h0
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x = 0 ∨ -y ≠ 0
⊢ 0 < angle x (x - y)
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x = 0 ∨ -y ≠ 0
⊢ 0 < angle x (x + -y)
[PROOFSTEP]
exact angle_add_pos_of_inner_eq_zero h h0
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ angle x (x - y) ≤ π / 2
[PROOFSTEP]
rw [← neg_eq_zero, ← inner_neg_right] at h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ angle x (x - y) ≤ π / 2
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ angle x (x + -y) ≤ π / 2
[PROOFSTEP]
exact angle_add_le_pi_div_two_of_inner_eq_zero h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0
⊢ angle x (x - y) < π / 2
[PROOFSTEP]
rw [← neg_eq_zero, ← inner_neg_right] at h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0
⊢ angle x (x - y) < π / 2
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0
⊢ angle x (x + -y) < π / 2
[PROOFSTEP]
exact angle_add_lt_pi_div_two_of_inner_eq_zero h h0
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ Real.cos (angle x (x - y)) = ‖x‖ / ‖x - y‖
[PROOFSTEP]
rw [← neg_eq_zero, ← inner_neg_right] at h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ Real.cos (angle x (x - y)) = ‖x‖ / ‖x - y‖
[PROOFSTEP]
rw [sub_eq_add_neg, cos_angle_add_of_inner_eq_zero h]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ Real.sin (angle x (x - y)) = ‖y‖ / ‖x - y‖
[PROOFSTEP]
rw [← neg_eq_zero, ← inner_neg_right] at h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ Real.sin (angle x (x - y)) = ‖y‖ / ‖x - y‖
[PROOFSTEP]
rw [or_comm, ← neg_ne_zero, or_comm] at h0
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0 ∨ -y ≠ 0
⊢ Real.sin (angle x (x - y)) = ‖y‖ / ‖x - y‖
[PROOFSTEP]
rw [sub_eq_add_neg, sin_angle_add_of_inner_eq_zero h h0, norm_neg]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ Real.tan (angle x (x - y)) = ‖y‖ / ‖x‖
[PROOFSTEP]
rw [← neg_eq_zero, ← inner_neg_right] at h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ Real.tan (angle x (x - y)) = ‖y‖ / ‖x‖
[PROOFSTEP]
rw [sub_eq_add_neg, tan_angle_add_of_inner_eq_zero h, norm_neg]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ Real.cos (angle x (x - y)) * ‖x - y‖ = ‖x‖
[PROOFSTEP]
rw [← neg_eq_zero, ← inner_neg_right] at h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ Real.cos (angle x (x - y)) * ‖x - y‖ = ‖x‖
[PROOFSTEP]
rw [sub_eq_add_neg, cos_angle_add_mul_norm_of_inner_eq_zero h]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ Real.sin (angle x (x - y)) * ‖x - y‖ = ‖y‖
[PROOFSTEP]
rw [← neg_eq_zero, ← inner_neg_right] at h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
⊢ Real.sin (angle x (x - y)) * ‖x - y‖ = ‖y‖
[PROOFSTEP]
rw [sub_eq_add_neg, sin_angle_add_mul_norm_of_inner_eq_zero h, norm_neg]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y = 0
⊢ Real.tan (angle x (x - y)) * ‖x‖ = ‖y‖
[PROOFSTEP]
rw [← neg_eq_zero, ← inner_neg_right] at h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0 ∨ y = 0
⊢ Real.tan (angle x (x - y)) * ‖x‖ = ‖y‖
[PROOFSTEP]
rw [← neg_eq_zero] at h0
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0 ∨ -y = 0
⊢ Real.tan (angle x (x - y)) * ‖x‖ = ‖y‖
[PROOFSTEP]
rw [sub_eq_add_neg, tan_angle_add_mul_norm_of_inner_eq_zero h h0, norm_neg]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x ≠ 0 ∨ y = 0
⊢ ‖x‖ / Real.cos (angle x (x - y)) = ‖x - y‖
[PROOFSTEP]
rw [← neg_eq_zero, ← inner_neg_right] at h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0 ∨ y = 0
⊢ ‖x‖ / Real.cos (angle x (x - y)) = ‖x - y‖
[PROOFSTEP]
rw [← neg_eq_zero] at h0
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x ≠ 0 ∨ -y = 0
⊢ ‖x‖ / Real.cos (angle x (x - y)) = ‖x - y‖
[PROOFSTEP]
rw [sub_eq_add_neg, norm_div_cos_angle_add_of_inner_eq_zero h h0]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / Real.sin (angle x (x - y)) = ‖x - y‖
[PROOFSTEP]
rw [← neg_eq_zero, ← inner_neg_right] at h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / Real.sin (angle x (x - y)) = ‖x - y‖
[PROOFSTEP]
rw [← neg_ne_zero] at h0
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x = 0 ∨ -y ≠ 0
⊢ ‖y‖ / Real.sin (angle x (x - y)) = ‖x - y‖
[PROOFSTEP]
rw [sub_eq_add_neg, ← norm_neg, norm_div_sin_angle_add_of_inner_eq_zero h h0]
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / Real.tan (angle x (x - y)) = ‖x‖
[PROOFSTEP]
rw [← neg_eq_zero, ← inner_neg_right] at h
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x = 0 ∨ y ≠ 0
⊢ ‖y‖ / Real.tan (angle x (x - y)) = ‖x‖
[PROOFSTEP]
rw [← neg_ne_zero] at h0
[GOAL]
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x (-y) = 0
h0 : x = 0 ∨ -y ≠ 0
⊢ ‖y‖ / Real.tan (angle x (x - y)) = ‖x‖
[PROOFSTEP]
rw [sub_eq_add_neg, ← norm_neg, norm_div_tan_angle_add_of_inner_eq_zero h h0]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p1 p2 p3 : P
⊢ dist p1 p3 * dist p1 p3 = dist p1 p2 * dist p1 p2 + dist p3 p2 * dist p3 p2 ↔ ∠ p1 p2 p3 = π / 2
[PROOFSTEP]
erw [dist_comm p3 p2, dist_eq_norm_vsub V p1 p3, dist_eq_norm_vsub V p1 p2, dist_eq_norm_vsub V p2 p3, ←
  norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two, vsub_sub_vsub_cancel_right p1, ←
  neg_vsub_eq_vsub_rev p2 p3, norm_neg]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
⊢ ∠ p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)
[PROOFSTEP]
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ← inner_neg_left,
  neg_vsub_eq_vsub_rev] at h
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
⊢ ∠ p₂ p₃ p₁ = Real.arccos (dist p₃ p₂ / dist p₁ p₃)
[PROOFSTEP]
rw [angle, dist_eq_norm_vsub' V p₃ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm,
  angle_add_eq_arccos_of_inner_eq_zero h]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)
[PROOFSTEP]
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ← inner_neg_left,
  neg_vsub_eq_vsub_rev] at h
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)
[PROOFSTEP]
rw [← @vsub_ne_zero V, @ne_comm _ p₃, ← @vsub_ne_zero V _ _ _ p₂, or_comm] at h0
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)
[PROOFSTEP]
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm,
  angle_add_eq_arcsin_of_inner_eq_zero h h0]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
[PROOFSTEP]
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ← inner_neg_left,
  neg_vsub_eq_vsub_rev] at h
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
[PROOFSTEP]
rw [ne_comm, ← @vsub_ne_zero V] at h0
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ ≠ 0
⊢ ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
[PROOFSTEP]
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub' V p₃ p₂, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm,
  angle_add_eq_arctan_of_inner_eq_zero h h0]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₁ ≠ p₂ ∨ p₃ = p₂
⊢ 0 < ∠ p₂ p₃ p₁
[PROOFSTEP]
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ← inner_neg_left,
  neg_vsub_eq_vsub_rev] at h
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₁ ≠ p₂ ∨ p₃ = p₂
⊢ 0 < ∠ p₂ p₃ p₁
[PROOFSTEP]
rw [← @vsub_ne_zero V, eq_comm, ← @vsub_eq_zero_iff_eq V, or_comm] at h0
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ 0 < ∠ p₂ p₃ p₁
[PROOFSTEP]
rw [angle, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ 0 < InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂))
[PROOFSTEP]
exact angle_add_pos_of_inner_eq_zero h h0
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
⊢ ∠ p₂ p₃ p₁ ≤ π / 2
[PROOFSTEP]
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ← inner_neg_left,
  neg_vsub_eq_vsub_rev] at h
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
⊢ ∠ p₂ p₃ p₁ ≤ π / 2
[PROOFSTEP]
rw [angle, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) ≤ π / 2
[PROOFSTEP]
exact angle_add_le_pi_div_two_of_inner_eq_zero h
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ < π / 2
[PROOFSTEP]
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ← inner_neg_left,
  neg_vsub_eq_vsub_rev] at h
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ < π / 2
[PROOFSTEP]
rw [ne_comm, ← @vsub_ne_zero V] at h0
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ ≠ 0
⊢ ∠ p₂ p₃ p₁ < π / 2
[PROOFSTEP]
rw [angle, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ ≠ 0
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) < π / 2
[PROOFSTEP]
exact angle_add_lt_pi_div_two_of_inner_eq_zero h h0
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
⊢ Real.cos (∠ p₂ p₃ p₁) = dist p₃ p₂ / dist p₁ p₃
[PROOFSTEP]
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ← inner_neg_left,
  neg_vsub_eq_vsub_rev] at h
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
⊢ Real.cos (∠ p₂ p₃ p₁) = dist p₃ p₂ / dist p₁ p₃
[PROOFSTEP]
rw [angle, dist_eq_norm_vsub' V p₃ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm,
  cos_angle_add_of_inner_eq_zero h]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂
⊢ Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
[PROOFSTEP]
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ← inner_neg_left,
  neg_vsub_eq_vsub_rev] at h
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₁ ≠ p₂ ∨ p₃ ≠ p₂
⊢ Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
[PROOFSTEP]
rw [← @vsub_ne_zero V, @ne_comm _ p₃, ← @vsub_ne_zero V _ _ _ p₂, or_comm] at h0
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
[PROOFSTEP]
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm,
  sin_angle_add_of_inner_eq_zero h h0]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
⊢ Real.tan (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂
[PROOFSTEP]
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ← inner_neg_left,
  neg_vsub_eq_vsub_rev] at h
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
⊢ Real.tan (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂
[PROOFSTEP]
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub' V p₃ p₂, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm,
  tan_angle_add_of_inner_eq_zero h]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
⊢ Real.cos (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂
[PROOFSTEP]
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ← inner_neg_left,
  neg_vsub_eq_vsub_rev] at h
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
⊢ Real.cos (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂
[PROOFSTEP]
rw [angle, dist_eq_norm_vsub' V p₃ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm,
  cos_angle_add_mul_norm_of_inner_eq_zero h]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
⊢ Real.sin (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂
[PROOFSTEP]
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ← inner_neg_left,
  neg_vsub_eq_vsub_rev] at h
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
⊢ Real.sin (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₁ p₂
[PROOFSTEP]
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm,
  sin_angle_add_mul_norm_of_inner_eq_zero h]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₁ = p₂ ∨ p₃ ≠ p₂
⊢ Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂
[PROOFSTEP]
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ← inner_neg_left,
  neg_vsub_eq_vsub_rev] at h
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₁ = p₂ ∨ p₃ ≠ p₂
⊢ Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂
[PROOFSTEP]
rw [ne_comm, ← @vsub_ne_zero V, ← @vsub_eq_zero_iff_eq V, or_comm] at h0
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ = 0
⊢ Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂
[PROOFSTEP]
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub' V p₃ p₂, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm,
  tan_angle_add_mul_norm_of_inner_eq_zero h h0]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₁ = p₂ ∨ p₃ ≠ p₂
⊢ dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃
[PROOFSTEP]
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ← inner_neg_left,
  neg_vsub_eq_vsub_rev] at h
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₁ = p₂ ∨ p₃ ≠ p₂
⊢ dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃
[PROOFSTEP]
rw [ne_comm, ← @vsub_ne_zero V, ← @vsub_eq_zero_iff_eq V, or_comm] at h0
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ ≠ 0 ∨ p₁ -ᵥ p₂ = 0
⊢ dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃
[PROOFSTEP]
rw [angle, dist_eq_norm_vsub' V p₃ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm,
  norm_div_cos_angle_add_of_inner_eq_zero h h0]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₁ ≠ p₂ ∨ p₃ = p₂
⊢ dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃
[PROOFSTEP]
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ← inner_neg_left,
  neg_vsub_eq_vsub_rev] at h
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₁ ≠ p₂ ∨ p₃ = p₂
⊢ dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃
[PROOFSTEP]
rw [eq_comm, ← @vsub_ne_zero V, ← @vsub_eq_zero_iff_eq V, or_comm] at h0
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃
[PROOFSTEP]
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm,
  norm_div_sin_angle_add_of_inner_eq_zero h h0]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
h0 : p₁ ≠ p₂ ∨ p₃ = p₂
⊢ dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂
[PROOFSTEP]
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ← inner_neg_left,
  neg_vsub_eq_vsub_rev] at h
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₁ ≠ p₂ ∨ p₃ = p₂
⊢ dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂
[PROOFSTEP]
rw [eq_comm, ← @vsub_ne_zero V, ← @vsub_eq_zero_iff_eq V, or_comm] at h0
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0
⊢ dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂
[PROOFSTEP]
rw [angle, dist_eq_norm_vsub V p₁ p₂, dist_eq_norm_vsub' V p₃ p₂, ← vsub_add_vsub_cancel p₁ p₂ p₃, add_comm,
  norm_div_tan_angle_add_of_inner_eq_zero h h0]