V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y x : V
⊢ arccos (inner x 0 / (‖x‖ * ‖0‖)) = π / 2
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y x : V
⊢ angle x 0 = π / 2
unfold angle
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x✝ y x : V
⊢ arccos (inner x 0 / (‖x‖ * ‖0‖)) = π / 2
rw [inner_zero_right, zero_div, Real.arccos_zero]