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‖
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‖
rw [tan_angle_add_of_inner_eq_zero h]
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‖

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‖
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‖
rcases h0 with (h0 | h0)
no goals
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‖
simp [h0]
no goals
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‖
rw [div_div_eq_mul_div, mul_comm, div_eq_mul_inv, mul_inv_cancel_right₀ (norm_ne_zero_iff.2 h0)]