no goals
x y : ℂ
⊢ sin (↑(starRingEnd ℂ) x) = ↑(starRingEnd ℂ) (sin x)
rw [← mul_left_inj' I_ne_zero, ← sinh_mul_I, ← conj_neg_I, ← RingHom.map_mul, ← RingHom.map_mul,
  sinh_conj, mul_neg, sinh_neg, sinh_mul_I, mul_neg]