noncomputable def DegreeTheory.det2 (a b : Fin 2 → ℝ) : ℝ

def DegreeTheory.OnUnitCircle (f : ℝ → Fin 2 → ℝ) : Prop

noncomputable def DegreeTheory.angularVelocity (f : ℝ → Fin 2 → ℝ) (t : ℝ) : ℝ

def DegreeTheory.IsAngleFunction (f : ℝ → Fin 2 → ℝ) (θ : ℝ → ℝ) : Prop

theorem DegreeTheory.exists_angle_of_unit_circle (a b : ℝ) (h : a ^ 2 + b ^ 2 = 1) : ∃ (θ₀ : ℝ), a = Real.cos θ₀ ∧ b = Real.sin θ₀

theorem DegreeTheory.smooth_angular_velocity (f : ℝ → Fin 2 → ℝ) (hf : ContDiff ℝ ⊤ f) : ContDiff ℝ ⊤ (angularVelocity f)

theorem DegreeTheory.contDiff_infty_integral (ω : ℝ → ℝ) (c : ℝ) (hω : ContDiff ℝ ⊤ ω) : ContDiff ℝ ⊤ fun (t : ℝ) => c + ∫ (τ : ℝ) in 0..t, ω τ

theorem DegreeTheory.ode_uniqueness (f : ℝ → Fin 2 → ℝ) (θ : ℝ → ℝ) (hf : ContDiff ℝ ⊤ f) (hcirc : OnUnitCircle f) (hθ : ContDiff ℝ ⊤ θ) (hderiv : ∀ (t : ℝ), HasDerivAt θ (angularVelocity f t) t) (hinit0 : f 0 0 = Real.cos (θ 0)) (hinit1 : f 0 1 = Real.sin (θ 0)) (t : ℝ) : f t 0 = Real.cos (θ t) ∧ f t 1 = Real.sin (θ t)

theorem DegreeTheory.angle_function_exists (f : ℝ → Fin 2 → ℝ) (hf : ContDiff ℝ ⊤ f) (hcirc : OnUnitCircle f) : ∃ (θ : ℝ → ℝ), IsAngleFunction f θ

theorem DegreeTheory.angle_function_unique (f : ℝ → Fin 2 → ℝ) (θ₁ θ₂ : ℝ → ℝ) (h1 : IsAngleFunction f θ₁) (h2 : IsAngleFunction f θ₂) : ∃ (k : ℤ), ∀ (t : ℝ), θ₂ t - θ₁ t = 2 * Real.pi * ↑k

theorem DegreeTheory.angle_function_exists_unique (f : ℝ → Fin 2 → ℝ) (hf : ContDiff ℝ ⊤ f) (hcirc : OnUnitCircle f) : (∃ (θ : ℝ → ℝ), IsAngleFunction f θ) ∧ ∀ (θ₁ θ₂ : ℝ → ℝ), IsAngleFunction f θ₁ → IsAngleFunction f θ₂ → ∃ (k : ℤ), ∀ (t : ℝ), θ₂ t - θ₁ t = 2 * Real.pi * ↑k

noncomputable def DegreeTheory.degreeReal (f : ℝ → Fin 2 → ℝ) (T : ℝ) : ℝ

theorem DegreeTheory.degree_is_integer (f : ℝ → Fin 2 → ℝ) (hf : ContDiff ℝ ⊤ f) (hcirc : OnUnitCircle f) (T : ℝ) (hper : ∀ (t : ℝ), f (t + T) = f t) : ∃ (k : ℤ), degreeReal f T = ↑k

theorem DegreeTheory.degree_eq_zero_of_not_surjective (f : ℝ → Fin 2 → ℝ) (T : ℝ) (hT : T > 0) (hf : ContDiff ℝ ⊤ f) (hcirc : OnUnitCircle f) (hper : ∀ (t : ℝ), f (t + T) = f t) (q : Fin 2 → ℝ) (hq : q 0 ^ 2 + q 1 ^ 2 = 1) (hmiss : ∀ (t : ℝ), f t ≠ q) : degreeReal f T = 0

theorem DegreeTheory.surjective_of_degree_ne_zero (f : ℝ → Fin 2 → ℝ) (T : ℝ) (hT : T > 0) (hf : ContDiff ℝ ⊤ f) (hcirc : OnUnitCircle f) (hper : ∀ (t : ℝ), f (t + T) = f t) (hdeg : degreeReal f T ≠ 0) (q : Fin 2 → ℝ) : q 0 ^ 2 + q 1 ^ 2 = 1 → ∃ (t : ℝ), f t = q

theorem DegreeTheory.level_crossing_identity (θ : ℝ → ℝ) (T : ℝ) (hT : T > 0) (hθ_smooth : ContDiff ℝ ⊤ θ) (α : ℝ) (preimages : Finset ℝ) (hpre_bounds : ∀ t ∈ preimages, 0 ≤ t ∧ t < T) (hpre_val : ∀ t ∈ preimages, ∃ (k : ℤ), θ t - α = 2 * Real.pi * ↑k) (hcomplete : ∀ (t : ℝ), 0 ≤ t → t < T → (∃ (k : ℤ), θ t - α = 2 * Real.pi * ↑k) → t ∈ preimages) (hregular : ∀ t ∈ preimages, deriv θ t ≠ 0) (hperiodic : ∃ (k : ℤ), θ T - θ 0 = 2 * Real.pi * ↑k) : (θ T - θ 0) / (2 * Real.pi) = ∑ t ∈ preimages, (deriv θ t).sign

theorem DegreeTheory.degree_as_signed_count (f : ℝ → Fin 2 → ℝ) (T : ℝ) (hT : T > 0) (hf : ContDiff ℝ ⊤ f) (hcirc : OnUnitCircle f) (hper : ∀ (t : ℝ), f (t + T) = f t) (p : Fin 2 → ℝ) (hp : p 0 ^ 2 + p 1 ^ 2 = 1) (preimages : Finset ℝ) (hpre : ∀ t ∈ preimages, 0 ≤ t ∧ t < T ∧ f t = p) (hcomplete : ∀ (t : ℝ), 0 ≤ t → t < T → f t = p → t ∈ preimages) (hregular : ∀ t ∈ preimages, deriv f t ≠ 0) : degreeReal f T = ∑ t ∈ preimages, (det2 p (deriv f t)).sign