mathlib3

f399d3a3 - feat(analysis/special_functions/complex/arg): relation to `real.angle.to_real` (#16205)

feat(analysis/special_functions/complex/arg): relation to `real.angle.to_real` (#16205) Add two lemmas about the fact that `real.angle.to_real` is the inverse of coercing the result of `complex.arg` to `real.angle`. Thus, give the existing lemma `arg_coe_angle_eq_iff` a much shorter proof.