Theorem: circle_parametric_inverse_polar (test/prob_ad/circle_discont_2d.lean)

State before:
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)
Tactic:
simp[ParametricInverseAt]
State after:
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

State before:
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
Tactic:
intros
State after:
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

State before:
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
Tactic:
sorry_proof
State after:
no goals