x y : ℂ
h : I * sin (x * I) = -sinh x
⊢ sin (x * I) = sinh x * I
x y : ℂ
⊢ sin (x * I) = sinh x * I
have h : I * sin (x * I) = -sinh x := by
  rw [mul_comm, ← sinh_mul_I]
  ring_nf
  simp
x y : ℂ
h : I * sin (x * I) = -sinh x
⊢ sin (x * I) = -(I * sin (x * I)) * I
x y : ℂ
h : I * sin (x * I) = -sinh x
⊢ sin (x * I) = sinh x * I
rw [← neg_neg (sinh x), ← h]
no goals
x y : ℂ
h : I * sin (x * I) = -sinh x
⊢ sin (x * I) = -(I * sin (x * I)) * I
ext <;> simp
x y : ℂ
⊢ sinh (x * I * I) = -sinh x
x y : ℂ
⊢ I * sin (x * I) = -sinh x
rw [mul_comm, ← sinh_mul_I]
x y : ℂ
⊢ sinh (x * I ^ 2) = -sinh x
x y : ℂ
⊢ sinh (x * I * I) = -sinh x
ring_nf
no goals
x y : ℂ
⊢ sinh (x * I ^ 2) = -sinh x
simp