simp[ParametricInverseAt]
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
r : R
hr : r ≠ 0
⊢ ParametricInverseAt (fun x => x.1 ^ 2 + x.2 ^ 2 - r ^ 2 - 0) 0 (fun x θ s => s • circleParam θ) (fun x x => r)
    fun x => Ico 0 (2 * RealScalar.pi)
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
r : R
hr : r ≠ 0
⊢ ∀ (x₁ : R), 0 ≤ x₁ → x₁ < 2 * RealScalar.pi → (r * (circleParam x₁).1) ^ 2 + (r * (circleParam x₁).2) ^ 2 - r ^ 2 = 0