feat: add lemmas on Complex.arg (x * y) and Complex.log (x * y) (#8346)

This adds lemmas as in the title (plus one for `arg (x * r)` with real `r`):
```lean
lemma arg_mul_eq_add_arg_iff {x y : ℂ} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) :
    (x * y).arg = x.arg + y.arg ↔ arg x + arg y ∈ Set.Ioc (-π) π

lemma arg_mul {x y : ℂ} (hx₀ : x ≠ 0) (hx₁ : -π / 2 < x.arg) (hx₂ : x.arg ≤ π / 2)
    (hy₀ : y ≠ 0) (hy₁ : -π / 2 < y.arg) (hy₂ : y.arg ≤ π / 2) :
    (x * y).arg = x.arg + y.arg

lemma log_mul_eq_add_log_iff {x y : ℂ} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) :
    log (x * y) = log x + log y ↔ arg x + arg y ∈ Set.Ioc (-π) π

lemma log_mul {x y : ℂ} (hx₀ : x ≠ 0) (hx₁ : -π / 2 < x.arg) (hx₂ : x.arg ≤ π / 2)
    (hy₀ : y ≠ 0) (hy₁ : -π / 2 < y.arg) (hy₂ : y.arg ≤ π / 2) :
    (x * y).log = x.log + y.log
```
See [here](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/log.20.28x*y.29.20.3D.20log.20x.20.2B.20log.20y.20for.20complex.20numbers/near/401233495) on Zulip.

Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean

@@ -188,6 +188,9 @@ theorem arg_real_mul (x : ℂ) {r : ℝ} (hr : 0 < r) : arg (r * x) = arg x := b
       arg_mul_cos_add_sin_mul_I (mul_pos hr (abs.pos hx)) x.arg_mem_Ioc]
 #align complex.arg_real_mul Complex.arg_real_mul
 
+theorem arg_mul_real {r : ℝ} (hr : 0 < r) (x : ℂ) : arg (x * r) = arg x :=
+  mul_comm x r ▸ arg_real_mul x hr
+
 theorem arg_eq_arg_iff {x y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) :
     arg x = arg y ↔ (abs y / abs x : ℂ) * x = y := by
   simp only [ext_abs_arg_iff, map_mul, map_div₀, abs_ofReal, abs_abs,
@@ -511,6 +514,13 @@ theorem arg_coe_angle_eq_iff {x y : ℂ} : (arg x : Real.Angle) = arg y ↔ arg
   simp_rw [← Real.Angle.toReal_inj, arg_coe_angle_toReal_eq_arg]
 #align complex.arg_coe_angle_eq_iff Complex.arg_coe_angle_eq_iff
 
+lemma arg_mul_eq_add_arg_iff {x y : ℂ} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) :
+    (x * y).arg = x.arg + y.arg ↔ arg x + arg y ∈ Set.Ioc (-π) π := by
+  rw [← arg_coe_angle_toReal_eq_arg, arg_mul_coe_angle hx₀ hy₀, ← Real.Angle.coe_add,
+      Real.Angle.toReal_coe_eq_self_iff_mem_Ioc]
+
+alias ⟨_, arg_mul⟩ := arg_mul_eq_add_arg_iff
+
 section Continuity
 
 variable {x z : ℂ}

Mathlib/Analysis/SpecialFunctions/Complex/Log.lean

@@ -86,6 +86,14 @@ theorem log_mul_ofReal (r : ℝ) (hr : 0 < r) (x : ℂ) (hx : x ≠ 0) :
     log (x * r) = Real.log r + log x := by rw [mul_comm, log_ofReal_mul hr hx, add_comm]
 #align complex.log_mul_of_real Complex.log_mul_ofReal
 
+lemma log_mul_eq_add_log_iff {x y : ℂ} (hx₀ : x ≠ 0) (hy₀ : y ≠ 0) :
+    log (x * y) = log x + log y ↔ arg x + arg y ∈ Set.Ioc (-π) π := by
+  refine ext_iff.trans <| Iff.trans ?_ <| arg_mul_eq_add_arg_iff hx₀ hy₀
+  simp_rw [add_re, add_im, log_re, log_im, AbsoluteValue.map_mul,
+    Real.log_mul (abs.ne_zero hx₀) (abs.ne_zero hy₀), true_and]
+
+alias ⟨_, log_mul⟩ := log_mul_eq_add_log_iff
+
 @[simp]
 theorem log_zero : log 0 = 0 := by simp [log]
 #align complex.log_zero Complex.log_zero