unfold circleParam jacobian
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ jacobian R circleParam = 1
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ (fun x =>
      let dg := ∂ (θ:=x), (cos θ, sin θ);
      let dg' := semiAdjoint R dg;
      sqrt (det R (dg' ∘ dg))) =
    1