V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : sin (angle x y) = 1
⊢ angle x y = π / 2
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ sin (angle x y) = 1 ↔ angle x y = π / 2
refine' ⟨fun h => _, fun h => by rw [h, sin_pi_div_two]⟩
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : sin (angle x y) = 1
⊢ sqrt (1 - 1 ^ 2) = 0
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : sin (angle x y) = 1
⊢ angle x y = π / 2
rw [← cos_eq_zero_iff_angle_eq_pi_div_two, ← abs_eq_zero, abs_cos_eq_sqrt_one_sub_sin_sq, h]
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : sin (angle x y) = 1
⊢ sqrt (1 - 1 ^ 2) = 0
simp
no goals
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : angle x y = π / 2
⊢ sin (angle x y) = 1
rw [h, sin_pi_div_two]