Theorem: realCircleMap.fderiv (Ray/Hartogs/FubiniBall.lean)

State before:
c : ℂ
x : ℝ × ℝ
⊢ HasFDerivAt (fun x => realCircleMap c x) (rcmDeriv x) x
Tactic:
simp_rw [realCircleMap]
State after:
c : ℂ
x : ℝ × ℝ
⊢ HasFDerivAt (fun x => (c.re + x.1 * x.2.cos, c.im + x.1 * x.2.sin)) (rcmDeriv x) x

State before:
c : ℂ
x : ℝ × ℝ
⊢ HasFDerivAt (fun x => (c.re + x.1 * x.2.cos, c.im + x.1 * x.2.sin)) (rcmDeriv x) x
Tactic:
apply_rules [hasFDerivAt_const, hasFDerivAt_fst, hasFDerivAt_snd, HasFDerivAt.cos,
  HasFDerivAt.sin, HasFDerivAt.add, HasFDerivAt.mul, HasFDerivAt.prod]
State after:
no goals