A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
⊢ ↑ℜ ((↑z.re + ↑z.im * I) • a) = z.re • ↑ℜ a - z.im • ↑ℑ a
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
⊢ ↑ℜ (z • a) = z.re • ↑ℜ a - z.im • ↑ℑ a
conv_lhs =>
  rw [← re_add_im z]
no goals
A : Type u_1
inst✝³ : AddCommGroup A
inst✝² : Module ℂ A
inst✝¹ : StarAddMonoid A
inst✝ : StarModule ℂ A
z : ℂ
a : A
⊢ ↑ℜ ((↑z.re + ↑z.im * I) • a) = z.re • ↑ℜ a - z.im • ↑ℑ a
simp [-re_add_im, add_smul, ← smul_smul, sub_eq_add_neg]