feat(geometry/euclidean/basic): angles in subspaces (#16610)

Add lemmas that the angle between two vectors or three points in a subspace equals the angle between those vectors or points in the whole space.

Author: jsm28

src/geometry/euclidean/basic.lean

@@ -91,6 +91,10 @@ by rw [angle, angle, real_inner_smul_left, inner_smul_right, norm_smul, norm_smu
   angle (f u) (f v) = angle u v :=
 by rw [angle, angle, f.inner_map_map, f.norm_map, f.norm_map]
 
+@[simp, norm_cast] lemma _root_.submodule.angle_coe {s : submodule ℝ V} (x y : s) :
+  angle (x : V) (y : V) = angle x y :=
+s.subtypeₗᵢ.angle_map x y
+
 lemma is_conformal_map.preserves_angle {E F : Type*}
   [inner_product_space ℝ E] [inner_product_space ℝ F]
   {f' : E →L[ℝ] F} (h : is_conformal_map f') (u v : E) :
@@ -412,6 +416,11 @@ end
   ∠ (f p₁) (f p₂) (f p₃) = ∠ p₁ p₂ p₃ :=
 by simp_rw [angle, ←affine_isometry.map_vsub, linear_isometry.angle_map]
 
+@[simp, norm_cast] lemma _root_.affine_subspace.angle_coe {s : affine_subspace ℝ P}
+  (p₁ p₂ p₃ : s) :
+  by haveI : nonempty s := ⟨p₁⟩; exact ∠ (p₁ : P) (p₂ : P) (p₃ : P) = ∠ p₁ p₂ p₃ :=
+by haveI : nonempty s := ⟨p₁⟩; exact s.subtypeₐᵢ.angle_map p₁ p₂ p₃
+
 /-- The angle at a point does not depend on the order of the other two
 points. -/
 lemma angle_comm (p1 p2 p3 : P) : ∠ p1 p2 p3 = ∠ p3 p2 p1 :=