feat(data/complex/basic): Adding im_eq_sub_conj (#5750)

Adds `im_eq_sub_conj`, which I couldn't find in the library.

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

Author: jamesa9283

src/data/complex/basic.lean

@@ -363,8 +363,15 @@ instance char_zero_complex : char_zero ℂ :=
 char_zero_of_inj_zero $ λ n h,
 by rwa [← of_real_nat_cast, of_real_eq_zero, nat.cast_eq_zero] at h
 
+/-- A complex number `z` plus its conjugate `conj z` is `2` times its real part. -/
 theorem re_eq_add_conj (z : ℂ) : (z.re : ℂ) = (z + conj z) / 2 :=
-by rw [add_conj]; simp; rw [mul_div_cancel_left (z.re:ℂ) two_ne_zero']
+by simp only [add_conj, of_real_mul, of_real_one, of_real_bit0, 
+     mul_div_cancel_left (z.re:ℂ) two_ne_zero']
+
+/-- A complex number `z` minus its conjugate `conj z` is `2i` times its imaginary part. -/
+theorem im_eq_sub_conj (z : ℂ) : (z.im : ℂ) = (z - conj(z))/(2 * I) :=
+by simp only [sub_conj, of_real_mul, of_real_one, of_real_bit0, mul_right_comm, 
+     mul_div_cancel_left _ (mul_ne_zero two_ne_zero' I_ne_zero : 2 * I ≠ 0)]
 
 /-! ### Absolute value -/