no goals
V : Type ?u.9920
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
x y : V
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E →ₗᵢ[ℝ] F
u v : E
⊢ angle (↑f u) (↑f v) = angle u v
rw [angle, angle, f.inner_map_map, f.norm_map, f.norm_map]