fix(geometry/euclidean/angle/unoriented/right_angle): lemma naming co…

…nsistency (#17273)

Adjust the name of one lemma for `tan` to be consistent with the names of corresponding `sin` and `cos` lemmas.

src/geometry/euclidean/angle/unoriented/right_angle.lean

@@ -486,7 +486,7 @@ begin
 end
 
 /-- The tangent of an angle in a right-angled triangle as a ratio of sides. -/
-lemma tan_angle_eq_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2) :
+lemma tan_angle_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2) :
   real.tan (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₃ p₂ :=
 begin
   rw [angle, ←inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ←neg_eq_zero,