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‖

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‖
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‖
by_cases h0 : x = 0
no goals
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‖
rw [angle_add_eq_arctan_of_inner_eq_zero h h0, Real.tan_arctan]
no goals
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‖
simp [h0]