sorry_proof
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
r : R
hr : r ≠ 0
x₁✝ : R
a✝¹ : 0 ≤ x₁✝
a✝ : x₁✝ < 2 * RealScalar.pi
⊢ (r * (circleParam x₁✝).1) ^ 2 + (r * (circleParam x₁✝).2) ^ 2 - r ^ 2 = 0
no goals