no goals
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f g : ℂ → E
c : ℂ
R : ℝ
hR : 0 ≤ R
h : EqOn f g (sphere c R)
θ : ℝ
x✝ : θ ∈ [[0, 2 * π]]
⊢ deriv (circleMap c R) θ • (fun z => f z) (circleMap c R θ) =
    deriv (circleMap c R) θ • (fun z => g z) (circleMap c R θ)
simp only [h (circleMap_mem_sphere _ hR _)]