refactor(analysis/special_functions/trigonometric): simpler proof (#6133

)

... of `complex.tan_int_mul_pi`

3X faster elaboration, 2X smaller proof term

Co-authors: `lean-gptf`, Stanislas Polu

This was found by `formal-lean-wm-to-tt-m1-m2-v4-c4` when we evaluated it on theorems added to `mathlib` after we last extracted training data.

src/analysis/special_functions/trigonometric.lean

@@ -2400,7 +2400,7 @@ lemma tan_int_mul_pi_div_two (n : ℤ) : tan (n * π/2) = 0 :=
 tan_eq_zero_iff.mpr (by use n)
 
 lemma tan_int_mul_pi (n : ℤ) : tan (n * π) = 0 :=
-by rw tan_eq_zero_iff; use (2*n); field_simp [mul_comm ((n:ℂ)*(π:ℂ)) 2, ← mul_assoc]
+by simp [tan, add_mul, sin_add, sin_int_mul_pi]
 
 lemma cos_eq_cos_iff {x y : ℂ} :
   cos x = cos y ↔ ∃ k : ℤ, y = 2 * k * π + x ∨ y = 2 * k * π - x :=