ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>o.oangle y ((o.rotation (o.oangle x y)) x) = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>θ : Real.Angle<GOAL>o.oangle ((o.rotation θ) x) ((o.rotation θ) y) = o.oangle x y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>hx : x ≠ 0<VAR>θ : Real.Angle<GOAL>(o.rotation θ) x = x ↔ θ = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>hx : x ≠ 0<VAR>θ : Real.Angle<GOAL>x = (o.rotation θ) x ↔ θ = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>θ : Real.Angle<GOAL>(o.rotation θ) x = x ↔ x = 0 ∨ θ = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>θ : Real.Angle<GOAL>x = (o.rotation θ) x ↔ x = 0 ∨ θ = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>(o.rotation (o.oangle x y)) x = y ↔ ‖x‖ = ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>θ : Real.Angle<GOAL>o.oangle x y = θ ↔ y = (‖y‖ / ‖x‖) • (o.rotation θ) x
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<VAR>θ : Real.Angle<GOAL>o.oangle x y = θ ↔ ∃ r, 0 < r ∧ y = r • (o.rotation θ) x
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>θ : Real.Angle<GOAL>o.oangle x y = θ ↔ x ≠ 0 ∧ y ≠ 0 ∧ y = (‖y‖ / ‖x‖) • (o.rotation θ) x ∨ θ = 0 ∧ (x = 0 ∨ y = 0)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>θ : Real.Angle<GOAL>o.oangle x y = θ ↔ (x ≠ 0 ∧ y ≠ 0 ∧ ∃ r, 0 < r ∧ y = r • (o.rotation θ) x) ∨ θ = 0 ∧ (x = 0 ∨ y = 0)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>f : V ≃ₗᵢ[ℝ] V<VAR>hd : 0 < LinearMap.det ↑f.toLinearEquiv<GOAL>∃ θ, f = o.rotation θ
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedAddCommGroup V'<VAR>InnerProductSpace ℝ V<VAR>InnerProductSpace ℝ V'<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Fact (FiniteDimensional.finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ : Real.Angle<VAR>f : V ≃ₗᵢ[ℝ] V'<VAR>x : V'<GOAL>(((Orientation.map (Fin 2) f.toLinearEquiv) o).rotation θ) x = f ((o.rotation θ) (f.symm x))
<VAR>θ : Real.Angle<VAR>z : ℂ<GOAL>(Complex.orientation.rotation θ) z = ↑θ.expMapCircle * z
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ : Real.Angle<VAR>f : V ≃ₗᵢ[ℝ] ℂ<VAR>hf : (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation<VAR>x : V<GOAL>f ((o.rotation θ) x) = ↑θ.expMapCircle * f x
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ : Real.Angle<GOAL>(-o).rotation θ = o.rotation (-θ)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<GOAL>⟪(o.rotation ↑(π / 2)) x, x⟫_ℝ = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<GOAL>⟪x, (o.rotation ↑(π / 2)) x⟫_ℝ = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>r : ℝ<GOAL>⟪r • (o.rotation ↑(π / 2)) x, x⟫_ℝ = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>r : ℝ<GOAL>⟪x, r • (o.rotation ↑(π / 2)) x⟫_ℝ = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>r : ℝ<GOAL>⟪(o.rotation ↑(π / 2)) x, r • x⟫_ℝ = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>r : ℝ<GOAL>⟪r • x, (o.rotation ↑(π / 2)) x⟫_ℝ = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>r₁ r₂ : ℝ<GOAL>⟪r₁ • (o.rotation ↑(π / 2)) x, r₂ • x⟫_ℝ = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x : V<VAR>r₁ r₂ : ℝ<GOAL>⟪r₂ • x, r₁ • (o.rotation ↑(π / 2)) x⟫_ℝ = 0
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<GOAL>⟪x, y⟫_ℝ = 0 ↔ x = 0 ∨ ∃ r, r • (o.rotation ↑(π / 2)) x = y
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y z : V<VAR>hxyne : x ≠ y<VAR>hxzne : x ≠ z<VAR>hxy : ‖x‖ = ‖y‖<VAR>hxz : ‖x‖ = ‖z‖<GOAL>o.oangle y z = 2 • o.oangle (y - x) (z - x)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y z : V<VAR>hxyne : x ≠ y<VAR>hxzne : x ≠ z<VAR>r : ℝ<VAR>hx : ‖x‖ = r<VAR>hy : ‖y‖ = r<VAR>hz : ‖z‖ = r<GOAL>o.oangle y z = 2 • o.oangle (y - x) (z - x)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x₁ x₂ y z : V<VAR>hx₁yne : x₁ ≠ y<VAR>hx₁zne : x₁ ≠ z<VAR>hx₂yne : x₂ ≠ y<VAR>hx₂zne : x₂ ≠ z<VAR>r : ℝ<VAR>hx₁ : ‖x₁‖ = r<VAR>hx₂ : ‖x₂‖ = r<VAR>hy : ‖y‖ = r<VAR>hz : ‖z‖ = r<GOAL>2 • o.oangle (y - x₁) (z - x₁) = 2 • o.oangle (y - x₂) (z - x₂)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>s : EuclideanGeometry.Sphere P<VAR>p₁ p₂ p₃ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∈ s<VAR>hp₂p₁ : p₂ ≠ p₁<VAR>hp₂p₃ : p₂ ≠ p₃<GOAL>∡ p₁ s.center p₃ = 2 • ∡ p₁ p₂ p₃
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>s : EuclideanGeometry.Sphere P<VAR>p₁ p₂ p₃ p₄ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∈ s<VAR>hp₄ : p₄ ∈ s<VAR>hp₂p₁ : p₂ ≠ p₁<VAR>hp₂p₄ : p₂ ≠ p₄<VAR>hp₃p₁ : p₃ ≠ p₁<VAR>hp₃p₄ : p₃ ≠ p₄<GOAL>2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ p₄ : P<VAR>h : EuclideanGeometry.Cospherical {p₁, p₂, p₃, p₄}<VAR>hp₂p₁ : p₂ ≠ p₁<VAR>hp₂p₄ : p₂ ≠ p₄<VAR>hp₃p₁ : p₃ ≠ p₁<VAR>hp₃p₄ : p₃ ≠ p₄<GOAL>2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>s : EuclideanGeometry.Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>h : p₁ ≠ p₂<GOAL>∡ p₁ s.center p₂ = ↑π - 2 • ∡ s.center p₂ p₁
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>s : EuclideanGeometry.Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>h : p₁ ≠ p₂<GOAL>∡ p₁ s.center p₂ = ↑π - 2 • ∡ p₂ p₁ s.center
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>s : EuclideanGeometry.Sphere P<VAR>p₁ p₂ p₃ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∈ s<VAR>hp₂p₁ : p₂ ≠ p₁<VAR>hp₂p₃ : p₂ ≠ p₃<VAR>hp₁p₃ : p₁ ≠ p₃<GOAL>2 • ∡ p₃ p₁ s.center + 2 • ∡ p₁ p₂ p₃ = ↑π
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>s : EuclideanGeometry.Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<GOAL>|(∡ s.center p₂ p₁).toReal| < π / 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>s : EuclideanGeometry.Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<GOAL>|(∡ p₂ p₁ s.center).toReal| < π / 2
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>s : EuclideanGeometry.Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>h : p₁ ≠ p₂<GOAL>((∡ p₂ p₁ s.center).tan / 2) • (EuclideanGeometry.o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>s : EuclideanGeometry.Sphere P<VAR>p₁ p₂ p₃ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∈ s<VAR>hp₁p₂ : p₁ ≠ p₂<VAR>hp₁p₃ : p₁ ≠ p₃<VAR>hp₂p₃ : p₂ ≠ p₃<GOAL>((∡ p₁ p₂ p₃).tan⁻¹ / 2) • (EuclideanGeometry.o.rotation ↑(π / 2)) (p₃ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₃ = s.center
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>s : EuclideanGeometry.Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>h : p₁ ≠ p₂<GOAL>dist p₁ p₂ / (∡ p₂ p₁ s.center).cos / 2 = s.radius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>s : EuclideanGeometry.Sphere P<VAR>p₁ p₂ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>h : p₁ ≠ p₂<GOAL>dist p₁ p₂ / (∡ p₂ p₁ s.center).cos = 2 * s.radius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>s : EuclideanGeometry.Sphere P<VAR>p₁ p₂ p₃ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∈ s<VAR>hp₁p₂ : p₁ ≠ p₂<VAR>hp₁p₃ : p₁ ≠ p₃<VAR>hp₂p₃ : p₂ ≠ p₃<GOAL>dist p₁ p₃ / |(∡ p₁ p₂ p₃).sin| / 2 = s.radius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>s : EuclideanGeometry.Sphere P<VAR>p₁ p₂ p₃ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃ : p₃ ∈ s<VAR>hp₁p₂ : p₁ ≠ p₂<VAR>hp₁p₃ : p₁ ≠ p₃<VAR>hp₂p₃ : p₂ ≠ p₃<GOAL>dist p₁ p₃ / |(∡ p₁ p₂ p₃).sin| = 2 * s.radius
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>t : Affine.Triangle ℝ P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<GOAL>((∡ (t.points i₁) (t.points i₂) (t.points i₃)).tan⁻¹ / 2) • (EuclideanGeometry.o.rotation ↑(π / 2)) (t.points i₃ -ᵥ t.points i₁) +ᵥ midpoint ℝ (t.points i₁) (t.points i₃) = Affine.Simplex.circumcenter t
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>t : Affine.Triangle ℝ P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<GOAL>dist (t.points i₁) (t.points i₃) / |(∡ (t.points i₁) (t.points i₂) (t.points i₃)).sin| / 2 = Affine.Simplex.circumradius t
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>t : Affine.Triangle ℝ P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<GOAL>dist (t.points i₁) (t.points i₃) / |(∡ (t.points i₁) (t.points i₂) (t.points i₃)).sin| = 2 * Affine.Simplex.circumradius t
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>t : Affine.Triangle ℝ P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<GOAL>Affine.Simplex.circumsphere t = { center := ((∡ (t.points i₁) (t.points i₂) (t.points i₃)).tan⁻¹ / 2) • (EuclideanGeometry.o.rotation ↑(π / 2)) (t.points i₃ -ᵥ t.points i₁) +ᵥ midpoint ℝ (t.points i₁) (t.points i₃), radius := dist (t.points i₁) (t.points i₃) / |(∡ (t.points i₁) (t.points i₂) (t.points i₃)).sin| / 2 }
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>t₁ t₂ : Affine.Triangle ℝ P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h₁ : t₁.points i₁ = t₂.points i₁<VAR>h₃ : t₁.points i₃ = t₂.points i₃<VAR>h₂ : 2 • ∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃) = 2 • ∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)<GOAL>Affine.Simplex.circumsphere t₁ = Affine.Simplex.circumsphere t₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>t : Affine.Triangle ℝ P<VAR>p : P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h : 2 • ∡ (t.points i₁) p (t.points i₃) = 2 • ∡ (t.points i₁) (t.points i₂) (t.points i₃)<GOAL>p ∈ Affine.Simplex.circumsphere t
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ p₄ : P<VAR>h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄<VAR>hn : ¬Collinear ℝ {p₁, p₂, p₄}<GOAL>EuclideanGeometry.Cospherical {p₁, p₂, p₃, p₄}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ p₄ : P<VAR>h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄<VAR>hn : ¬Collinear ℝ {p₁, p₂, p₄}<GOAL>EuclideanGeometry.Concyclic {p₁, p₂, p₃, p₄}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ p₄ : P<VAR>h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄<GOAL>EuclideanGeometry.Cospherical {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>hd2 : Fact (FiniteDimensional.finrank ℝ V = 2)<VAR>Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ p₄ : P<VAR>h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄<GOAL>EuclideanGeometry.Concyclic {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>s : σ<GOAL>M.evalFrom s [] = s
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>s : σ<VAR>a : α<GOAL>M.evalFrom s [a] = M.step s a
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<GOAL>M.eval [] = M.start
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>a : α<GOAL>M.eval [a] = M.step M.start a
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>x : List α<VAR>a : α<GOAL>M.eval (x ++ [a]) = M.step (M.eval x) a
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>start : σ<VAR>x y : List α<GOAL>M.evalFrom start (x ++ y) = M.evalFrom (M.evalFrom start x) y
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>Fintype σ<VAR>x : List α<VAR>s t : σ<VAR>hlen : Fintype.card σ ≤ x.length<VAR>hx : M.evalFrom s x = t<GOAL>∃ q a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ M.evalFrom s a = q ∧ M.evalFrom q b = q ∧ M.evalFrom q c = t
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>Fintype σ<VAR>x : List α<VAR>hx : x ∈ M.accepts<VAR>hlen : Fintype.card σ ≤ x.length<GOAL>∃ a b c, x = a ++ b ++ c ∧ a.length + b.length ≤ Fintype.card σ ∧ b ≠ [] ∧ {a} * {b}∗ * {c} ≤ M.accepts
<VAR>α : Type u<VAR>σ : Type v<VAR>α' : Type u_1<VAR>f : α' → α<VAR>M : DFA α σ<GOAL>(DFA.comap f M).accept = M.accept
<VAR>α : Type u<VAR>σ : Type v<VAR>α' : Type u_1<VAR>f : α' → α<VAR>M : DFA α σ<VAR>s : σ<VAR>a : α'<GOAL>(DFA.comap f M).step s a = M.step s (f a)
<VAR>α : Type u<VAR>σ : Type v<VAR>α' : Type u_1<VAR>f : α' → α<VAR>M : DFA α σ<GOAL>(DFA.comap f M).start = M.start
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<GOAL>DFA.comap id M = M
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>α' : Type u_1<VAR>f : α' → α<VAR>s : σ<VAR>x : List α'<GOAL>(DFA.comap f M).evalFrom s x = M.evalFrom s (List.map f x)
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>α' : Type u_1<VAR>f : α' → α<VAR>x : List α'<GOAL>(DFA.comap f M).eval x = M.eval (List.map f x)
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>α' : Type u_1<VAR>f : α' → α<GOAL>(DFA.comap f M).accepts = List.map f ⁻¹' M.accepts
<VAR>α : Type u<VAR>σ : Type v<VAR>σ' : Type u_2<VAR>g : σ ≃ σ'<VAR>M : DFA α σ<GOAL>((DFA.reindex g) M).accept = ⇑g.symm ⁻¹' M.accept
<VAR>α : Type u<VAR>σ : Type v<VAR>σ' : Type u_2<VAR>g : σ ≃ σ'<VAR>M : DFA α σ<VAR>s : σ'<VAR>a : α<GOAL>((DFA.reindex g) M).step s a = g (M.step (g.symm s) a)
<VAR>α : Type u<VAR>σ : Type v<VAR>σ' : Type u_2<VAR>g : σ ≃ σ'<VAR>M : DFA α σ<GOAL>((DFA.reindex g) M).start = g M.start
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<GOAL>(DFA.reindex (Equiv.refl σ)) M = M
<VAR>α : Type u<VAR>σ : Type v<VAR>σ' : Type u_2<VAR>g : σ ≃ σ'<GOAL>(DFA.reindex g).symm = DFA.reindex g.symm
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>σ' : Type u_2<VAR>g : σ ≃ σ'<VAR>s : σ'<VAR>x : List α<GOAL>((DFA.reindex g) M).evalFrom s x = g (M.evalFrom (g.symm s) x)
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>σ' : Type u_2<VAR>g : σ ≃ σ'<VAR>x : List α<GOAL>((DFA.reindex g) M).eval x = g (M.eval x)
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>σ' : Type u_2<VAR>g : σ ≃ σ'<GOAL>((DFA.reindex g) M).accepts = M.accepts
<VAR>α : Type u<VAR>σ : Type v<VAR>M : DFA α σ<VAR>α' : Type u_1<VAR>σ' : Type u_2<VAR>f : α' → α<VAR>g : σ ≃ σ'<GOAL>DFA.comap f ((DFA.reindex g) M) = (DFA.reindex g) (DFA.comap f M)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<GOAL>‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ InnerProductGeometry.angle x y = π / 2
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : InnerProductGeometry.angle x y = π / 2<GOAL>‖x + y‖ * ‖x + y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<GOAL>‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ InnerProductGeometry.angle x y = π / 2
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : InnerProductGeometry.angle x y = π / 2<GOAL>‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>InnerProductGeometry.angle x (x + y) = Real.arccos (‖x‖ / ‖x + y‖)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y ≠ 0<GOAL>InnerProductGeometry.angle x (x + y) = Real.arcsin (‖y‖ / ‖x + y‖)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0<GOAL>InnerProductGeometry.angle x (x + y) = Real.arctan (‖y‖ / ‖x‖)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x = 0 ∨ y ≠ 0<GOAL>0 < InnerProductGeometry.angle x (x + y)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>InnerProductGeometry.angle x (x + y) ≤ π / 2
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0<GOAL>InnerProductGeometry.angle x (x + y) < π / 2
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>Real.cos (InnerProductGeometry.angle x (x + y)) = ‖x‖ / ‖x + y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y ≠ 0<GOAL>Real.sin (InnerProductGeometry.angle x (x + y)) = ‖y‖ / ‖x + y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>Real.tan (InnerProductGeometry.angle x (x + y)) = ‖y‖ / ‖x‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>Real.cos (InnerProductGeometry.angle x (x + y)) * ‖x + y‖ = ‖x‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>Real.sin (InnerProductGeometry.angle x (x + y)) * ‖x + y‖ = ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y = 0<GOAL>Real.tan (InnerProductGeometry.angle x (x + y)) * ‖x‖ = ‖y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y = 0<GOAL>‖x‖ / Real.cos (InnerProductGeometry.angle x (x + y)) = ‖x + y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x = 0 ∨ y ≠ 0<GOAL>‖y‖ / Real.sin (InnerProductGeometry.angle x (x + y)) = ‖x + y‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x = 0 ∨ y ≠ 0<GOAL>‖y‖ / Real.tan (InnerProductGeometry.angle x (x + y)) = ‖x‖
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>InnerProductGeometry.angle x (x - y) = Real.arccos (‖x‖ / ‖x - y‖)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y ≠ 0<GOAL>InnerProductGeometry.angle x (x - y) = Real.arcsin (‖y‖ / ‖x - y‖)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0<GOAL>InnerProductGeometry.angle x (x - y) = Real.arctan (‖y‖ / ‖x‖)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x = 0 ∨ y ≠ 0<GOAL>0 < InnerProductGeometry.angle x (x - y)
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>InnerProductGeometry.angle x (x - y) ≤ π / 2