CH2.tanh_add_int_mul_pi_I

theorem tanh_add_int_mul_pi_I (z : ℂ) (m : ℤ) : tanh (z + π * I * m) = tanh z := by  have step (w : ℂ) : tanh (w + π * I) = tanh w := by    rw [Complex.tanh_eq_sinh_div_cosh, Complex.tanh_eq_sinh_div_cosh,      sinh_add_pi_mul_I, cosh_add_pi_mul_I]; field_simp  induction m using Int.induction_on with  | zero => simp  | succ n ih =>    push_cast at ih ⊢    rw [show z + π * I * (n + 1) = (z + π * I * n) + π * I from by ring, step]; exact ih  | pred n ih =>    push_cast at ih ⊢    have h := step (z + π * I * (-n - 1))    rw [show z + π * I * (-n - 1) + π * I = z + π * I * -n from by ring] at h    rw [← h]; exact ih