ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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<VAR>h : dist p₁ p₂ = dist p₁ p₃<GOAL>|(∡ p₂ 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>p p₁ p₂ : P<VAR>hp₁ : p₁ ≠ p<VAR>hp₂ : p₂ ≠ p<GOAL>(∡ p₁ p p₂).cos = Real.cos (∠ 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<VAR>hp₁ : p₁ ≠ p<VAR>hp₂ : p₂ ≠ p<GOAL>∡ p₁ p p₂ = ↑(∠ p₁ p p₂) ∨ ∡ p₁ p 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<VAR>hp₁ : p₁ ≠ p<VAR>hp₂ : p₂ ≠ p<GOAL>∠ p₁ p p₂ = |(∡ p₁ p p₂).toReal|
<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<VAR>h : (∡ p₁ p p₂).sign = 0<GOAL>p₁ = p ∨ p₂ = p ∨ ∠ p₁ p p₂ = 0 ∨ ∠ 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₅ p₆ : P<VAR>h : ∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆<VAR>hs : (∡ p₁ p₂ p₃).sign = (∡ p₄ p₅ p₆).sign<GOAL>∡ p₁ p₂ 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₅ p₆ : P<VAR>hp₁ : p₁ ≠ p₂<VAR>hp₃ : p₃ ≠ p₂<VAR>hp₄ : p₄ ≠ p₅<VAR>hp₆ : p₆ ≠ p₅<VAR>hs : (∡ p₁ p₂ p₃).sign = (∡ p₄ p₅ p₆).sign<GOAL>∠ p₁ p₂ p₃ = ∠ p₄ p₅ p₆ ↔ ∡ p₁ p₂ 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<VAR>h : (∡ p₁ p₂ p₃).sign = 1<GOAL>∡ p₁ p₂ 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<VAR>h : (∡ p₁ p₂ p₃).sign = -1<GOAL>∡ p₁ p₂ 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<VAR>hp₁ : p₁ ≠ p<VAR>hp₂ : p₂ ≠ p<GOAL>∡ p₁ p p₂ = 0 ↔ ∠ p₁ p p₂ = 0
<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<GOAL>∡ p₁ p₂ 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<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>∠ p₁ p₂ p₃ = π / 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>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>∠ p₃ p₂ p₁ = π / 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>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(-π / 2)<GOAL>∠ p₁ p₂ p₃ = π / 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>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(-π / 2)<GOAL>∠ p₃ p₂ p₁ = π / 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>p₁ p₂ p₃ : P<GOAL>-(∡ p₁ p₂ p₃).sign = (∡ p₂ p₁ p₃).sign
<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<GOAL>-(∡ p₁ p₂ p₃).sign = (∡ p₃ p₂ p₁).sign
<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<GOAL>-(∡ p₁ p₂ p₃).sign = (∡ p₁ p₃ p₂).sign
<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<GOAL>(∡ p₂ p₃ p₁).sign = (∡ p₁ p₂ p₃).sign
<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<GOAL>∡ p₁ p₂ p₃ = ↑π ↔ Sbtw ℝ 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<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>∡ 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<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>∡ 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<VAR>h : Wbtw ℝ p₁ p₂ p₃<GOAL>∡ p₂ p₁ p₃ = 0
<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<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>∡ p₂ p₁ p₃ = 0
<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<VAR>h : Wbtw ℝ p₁ p₂ p₃<GOAL>∡ p₃ p₁ p₂ = 0
<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<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>∡ p₃ p₁ p₂ = 0
<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<VAR>h : Wbtw ℝ p₁ p₂ p₃<GOAL>∡ p₂ p₃ p₁ = 0
<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<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>∡ p₂ p₃ p₁ = 0
<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<VAR>h : Wbtw ℝ p₁ p₂ p₃<GOAL>∡ p₁ p₃ p₂ = 0
<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<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>∡ p₁ p₃ p₂ = 0
<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<GOAL>∡ p₁ p₂ p₃ = 0 ↔ Wbtw ℝ p₂ p₁ p₃ ∨ Wbtw ℝ 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 : Wbtw ℝ p₂ p₁ p₁'<VAR>hp₁p₂ : p₁ ≠ p₂<GOAL>∡ p₁ p₂ 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 : Sbtw ℝ p₂ p₁ p₁'<GOAL>∡ p₁ p₂ 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 : Wbtw ℝ p₂ p₃ p₃'<VAR>hp₃p₂ : p₃ ≠ p₂<GOAL>∡ p₁ p₂ 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 : Sbtw ℝ p₂ p₃ p₃'<GOAL>∡ p₁ p₂ 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<GOAL>∡ (midpoint ℝ p₁ p₂) p₂ 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<GOAL>∡ (midpoint ℝ p₂ p₁) p₂ 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<GOAL>∡ p₁ p₂ (midpoint ℝ p₃ 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<GOAL>∡ p₁ p₂ (midpoint ℝ p₂ 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 : Sbtw ℝ p₁ p₂ p₁'<VAR>hp₃p₂ : p₃ ≠ p₂<GOAL>∡ p₁ p₂ 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 : Sbtw ℝ p₃ p₂ p₃'<VAR>hp₁p₂ : p₁ ≠ p₂<GOAL>∡ p₁ p₂ 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₃' : P<VAR>h₁ : Sbtw ℝ p₁ p₂ p₁'<VAR>h₃ : Sbtw ℝ p₃ p₂ p₃'<GOAL>∡ p₁ p₂ 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 : Collinear ℝ {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 : Collinear ℝ {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<VAR>h : p₁ ≠ p₂<GOAL>dist p₁ p = dist p₂ p ↔ ∃ r, r • (EuclideanGeometry.o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ 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>p₅ : P<VAR>hp₁p₂ : p₁ ≠ p₂<VAR>hp₃p₄ : p₃ ≠ p₄<VAR>hc : Collinear ℝ {p₁, p₂, p₃, p₄}<VAR>hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)<GOAL>(∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign
<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<VAR>p₄ : P<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>(∡ p₁ p₄ p₂).sign = (∡ p₂ p₄ p₃).sign
<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<VAR>p₄ : P<VAR>h : Wbtw ℝ p₁ p₂ p₃<VAR>hne : p₁ ≠ p₂<GOAL>(∡ p₁ p₄ p₂).sign = (∡ p₁ p₄ p₃).sign
<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<VAR>p₄ : P<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>(∡ p₁ p₄ p₂).sign = (∡ p₁ p₄ p₃).sign
<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<VAR>p₄ : P<VAR>h : Wbtw ℝ p₁ p₂ p₃<VAR>hne : p₂ ≠ p₃<GOAL>(∡ p₂ p₄ p₃).sign = (∡ p₁ p₄ p₃).sign
<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<VAR>p₄ : P<VAR>h : Sbtw ℝ p₁ p₂ p₃<GOAL>(∡ p₂ p₄ p₃).sign = (∡ p₁ p₄ p₃).sign
<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 : AffineSubspace ℝ P<VAR>p₁ p₂ p₃ p₄ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃p₄ : s.SSameSide p₃ p₄<GOAL>(∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
<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 : AffineSubspace ℝ P<VAR>p₁ p₂ p₃ p₄ : P<VAR>hp₁ : p₁ ∈ s<VAR>hp₂ : p₂ ∈ s<VAR>hp₃p₄ : s.SOppSide p₃ p₄<GOAL>(∡ p₁ p₄ p₂).sign = -(∡ p₁ p₃ p₂).sign
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsRefl α r<GOAL>Reflexive r
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>h : Reflexive r<VAR>x y : α<VAR>hr : x ≠ y → r x y<GOAL>r x y
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>h : Reflexive r<VAR>x y : α<GOAL>x ≠ y → r x y ↔ r x y
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>IsRefl α r<VAR>x y : α<GOAL>x ≠ y → r x y ↔ r x y
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>H : Symmetric r<VAR>x y : α<GOAL>r x y ↔ r y x
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>h : Symmetric r<GOAL>flip r = r
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Symmetric r → Function.swap r = r
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>flip r = r ↔ Symmetric r
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Function.swap r = r ↔ Symmetric r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : β → β → Prop<VAR>h : Reflexive r<VAR>f : α → β<GOAL>Reflexive (r on f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : β → β → Prop<VAR>h : Symmetric r<VAR>f : α → β<GOAL>Symmetric (r on f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : β → β → Prop<VAR>h : Transitive r<VAR>f : α → β<GOAL>Transitive (r on f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : β → β → Prop<VAR>h : Equivalence r<VAR>f : α → β<GOAL>Equivalence (r on f)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<GOAL>(Relation.Comp r fun x x_1 => x = x_1) = r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<GOAL>Relation.Comp (fun x x_1 => x = x_1) r = r
<VAR>α : Type u_1<VAR>r : Prop → α → Prop<GOAL>Relation.Comp (fun x x_1 => x ↔ x_1) r = r
<VAR>α : Type u_1<VAR>r : α → Prop → Prop<GOAL>(Relation.Comp r fun x x_1 => x ↔ x_1) = r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r : α → β → Prop<VAR>p : β → γ → Prop<VAR>q : γ → δ → Prop<GOAL>Relation.Comp (Relation.Comp r p) q = Relation.Comp r (Relation.Comp p q)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → β → Prop<VAR>p : β → γ → Prop<GOAL>flip (Relation.Comp r p) = Relation.Comp (flip p) (flip r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>rα : α → α → Prop<VAR>rβ : β → β → Prop<VAR>f : α → β<VAR>fib : Relation.Fibration rα rβ f<VAR>a : α<VAR>ha : Acc rα a<GOAL>Acc rβ (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>rβ : β → β → Prop<VAR>f : α → β<VAR>dc : ∀ {a : α} {b : β}, rβ b (f a) → ∃ c, f c = b<VAR>a : α<VAR>ha : Acc (InvImage rβ f) a<GOAL>Acc rβ (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>r : α → β → Prop<VAR>f : α → γ<VAR>g : β → δ<VAR>c : γ<VAR>d : δ<GOAL>Relation.Map r f g c d ↔ ∃ a b, r a b ∧ f a = c ∧ g b = d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>ζ : Type u_6<VAR>r : α → β → Prop<VAR>f₁ : α → γ<VAR>g₁ : β → δ<VAR>f₂ : γ → ε<VAR>g₂ : δ → ζ<GOAL>Relation.Map (Relation.Map r f₁ g₁) f₂ g₂ = Relation.Map r (f₂ ∘ f₁) (g₂ ∘ g₁)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → γ<VAR>g : β → δ<VAR>hf : Function.Injective f<VAR>hg : Function.Injective g<VAR>r : α → β → Prop<VAR>a : α<VAR>b : β<GOAL>Relation.Map r f g (f a) (g b) ↔ r a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<GOAL>Relation.Map r id id = r
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a : α<GOAL>∀ (a_1 : α), Relation.ReflTransGen r a a_1 ↔ a_1 = a ∨ ∃ b, Relation.ReflTransGen r a b ∧ r b a_1
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a : α<GOAL>∀ (a_1 : α), Relation.ReflGen r a a_1 ↔ a_1 = a ∨ r a a_1
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a : α<GOAL>∀ (a_1 : α), Relation.TransGen r a a_1 ↔ r a a_1 ∨ ∃ b, Relation.TransGen r a b ∧ r b a_1
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<GOAL>Relation.ReflGen r a b → Relation.ReflTransGen r a b
<VAR>α : Type u_1<VAR>r p : α → α → Prop<VAR>hp : ∀ (a b : α), r a b → p a b<VAR>a b : α<GOAL>Relation.ReflGen r a b → Relation.ReflGen p a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b c : α<VAR>hab : Relation.ReflTransGen r a b<VAR>hbc : Relation.ReflTransGen r b c<GOAL>Relation.ReflTransGen r a c
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<VAR>hab : r a b<GOAL>Relation.ReflTransGen r a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b c : α<VAR>hab : r a b<VAR>hbc : Relation.ReflTransGen r b c<GOAL>Relation.ReflTransGen r a c
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>h : Symmetric r<GOAL>Symmetric (Relation.ReflTransGen r)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<GOAL>Relation.ReflTransGen r a b → b = a ∨ ∃ c, Relation.ReflTransGen r a c ∧ r c b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>b : α<VAR>P : (a : α) → Relation.ReflTransGen r a b → Prop<VAR>a : α<VAR>h : Relation.ReflTransGen r a b<VAR>refl : P b ⋯<VAR>head : ∀ {a c : α} (h' : r a c) (h : Relation.ReflTransGen r c b), P c h → P a ⋯<GOAL>P a h
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>P : {a b : α} → Relation.ReflTransGen r a b → Prop<VAR>a b : α<VAR>h : Relation.ReflTransGen r a b<VAR>ih₁ : ∀ (a : α), P ⋯<VAR>ih₂ : ∀ {a b : α} (h : r a b), P ⋯<VAR>ih₃ : ∀ {a b c : α} (h₁ : Relation.ReflTransGen r a b) (h₂ : Relation.ReflTransGen r b c), P h₁ → P h₂ → P ⋯<GOAL>P h
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<VAR>h : Relation.ReflTransGen r a b<GOAL>a = b ∨ ∃ c, r a c ∧ Relation.ReflTransGen r c b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<GOAL>Relation.ReflTransGen r a b ↔ a = b ∨ ∃ c, r a c ∧ Relation.ReflTransGen r c b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b c : α<VAR>U : Relator.RightUnique r<VAR>ab : Relation.ReflTransGen r a b<VAR>ac : Relation.ReflTransGen r a c<GOAL>Relation.ReflTransGen r b c ∨ Relation.ReflTransGen r c b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b : α<VAR>h : Relation.TransGen r a b<GOAL>Relation.ReflTransGen r a b
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b c : α<VAR>hab : Relation.TransGen r a b<VAR>hbc : Relation.ReflTransGen r b c<GOAL>Relation.TransGen r a c
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b c : α<VAR>hab : Relation.TransGen r a b<VAR>hbc : Relation.TransGen r b c<GOAL>Relation.TransGen r a c
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b c : α<VAR>hab : r a b<VAR>hbc : Relation.ReflTransGen r b c<GOAL>Relation.TransGen r a c
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b c : α<VAR>hab : Relation.ReflTransGen r a b<VAR>hbc : r b c<GOAL>Relation.TransGen r a c
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b c : α<VAR>hab : r a b<VAR>hbc : Relation.TransGen r b c<GOAL>Relation.TransGen r a c
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>b : α<VAR>P : (a : α) → Relation.TransGen r a b → Prop<VAR>a : α<VAR>h : Relation.TransGen r a b<VAR>base : ∀ {a : α} (h : r a b), P a ⋯<VAR>ih : ∀ {a c : α} (h' : r a c) (h : Relation.TransGen r c b), P c h → P a ⋯<GOAL>P a h
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>P : {a b : α} → Relation.TransGen r a b → Prop<VAR>a b : α<VAR>h : Relation.TransGen r a b<VAR>base : ∀ {a b : α} (h : r a b), P ⋯<VAR>ih : ∀ {a b c : α} (h₁ : Relation.TransGen r a b) (h₂ : Relation.TransGen r b c), P h₁ → P h₂ → P ⋯<GOAL>P h
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a b c : α<VAR>hab : Relation.ReflTransGen r a b<VAR>hbc : Relation.TransGen r b c<GOAL>Relation.TransGen r a c
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a c : α<GOAL>Relation.TransGen r a c ↔ ∃ b, Relation.ReflTransGen r a b ∧ r b c
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a c : α<GOAL>Relation.TransGen r a c ↔ ∃ b, r a b ∧ Relation.ReflTransGen r b c
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a : α<VAR>h : Acc r a<GOAL>Acc (Relation.TransGen r) a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a : α<GOAL>Acc (Relation.TransGen r) a ↔ Acc r a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>h : WellFounded r<GOAL>WellFounded (Relation.TransGen r)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>hr : Reflexive r<GOAL>Relation.ReflGen r = r
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Reflexive (Relation.ReflGen r)
<VAR>α : Type u_1<VAR>r r' : α → α → Prop<VAR>hr' : Reflexive r'<VAR>h : ∀ (x y : α), r x y → r' x y<VAR>x y : α<VAR>hxy : Relation.ReflGen r x y<GOAL>r' x y
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>trans : Transitive r<GOAL>Relation.TransGen r = r
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Transitive (Relation.TransGen r)
<VAR>α : Type u_1<VAR>r : α → α → Prop<GOAL>Relation.TransGen (Relation.TransGen r) = Relation.TransGen r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>p : β → β → Prop<VAR>a b : α<VAR>f : α → β<VAR>h : ∀ (a b : α), r a b → p (f a) (f b)<VAR>hab : Relation.TransGen r a b<GOAL>Relation.TransGen p (f a) (f b)