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