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)))
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‖)
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]
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)))
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)))
nth_rw 3 [← Real.sqrt_sq (norm_nonneg x)]
no goals
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)))
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]