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‖
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‖
rw [cos_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
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖

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‖
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‖
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
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖
rw [div_div_eq_mul_div, mul_comm, div_eq_mul_inv, mul_inv_cancel_right₀ (norm_ne_zero_iff.2 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
⊢ ‖x‖ / (‖x‖ / ‖x + y‖) = ‖x + y‖
simp [h0]