Theorem: realCircleMap_eq_circleMap (Ray/Hartogs/FubiniBall.lean)

State before:
c : ℂ
x : ℝ × ℝ
⊢ realCircleMap c x = Complex.equivRealProd (circleMap c x.1 x.2)
Tactic:
simp only [realCircleMap, circleMap, Complex.equivRealProd_apply, Complex.add_re, Complex.mul_re,
  Complex.ofReal_re, Complex.exp_ofReal_mul_I_re, Complex.ofReal_im, Complex.exp_ofReal_mul_I_im,
  zero_mul, sub_zero, Complex.add_im, Complex.mul_im, add_zero]
State after:
no goals